kiyoka.2013_09_10 RSSPLAIN

Related pages: !kiyoka.blog.list !kiyoka.blog.2013_09
35555555555555555555555555555555555545555555545555455555555555555555455555555555
3

[Nendo] 副作用の無いコードの静的解析について(1)

5

 

5

だいぶ前に、Nendoに型検査を入れて副作用の無いコードを静的解析で保証したいという話題を書いた。

5
 ( kiyoka.2011_10_07[Nendo][Ruby] コードブロックに副作用が混在するかを検出できるかどうか )
5

あれから時間が経ったけど、諦めずに考えているのであった。もう2年も経ったのか…

5

 

5

最近TAPL(第8章、第9章)を読んで、理論的なところを知ると、いろいろ気づいたので自分用のメモとして書いておく。

5
 4274069117  型システム入門 -プログラミング言語と型の理論-: Benjamin C. Pierce
5

 

5

欲しい機能

5

Nendoにどんな機能を追加したいかというと、

5
(pure S式)
5

と書くと、コンパイル時に静的解析して「S式の中に副作用が無いことを保証してくれる」機能だ。

5

 

5

例えば、次のコードは静的解析で実行前にエラーとなる。

5
(pure
5
 (define a 0)
5
 (set! a 1))
5

 

5

次。func1からの関数呼び出しがどれだけ深かろうが静的に検査して欲しい。

5
(pure
5
 (func1))
5

 

5

また、次のコードは副作用が無いと判断し、エラー無しで通って欲しい。

5
(pure
5
 (define lst '(1 2 3))
5
 (define result
5
   (map
5
    (lambda (x)
5
      (+ x 1))
5
    lst)))
5

 

5

ただ、そう簡単にはいかないのが世の中というもの。

5

 

5

問題点

5

 

4
アノテーションの記述量が膨大になる
5

 

5

静的解析するためには、事前に型情報のようなものが必要となる。

5

型情報といっても、副作用が無いと考えられる関数全てに「pure」の注釈を付けるだけなので、StringやIntegerなどの型情報は不要だ。

5

最低限、pureな全ての関数には必要。

5

 

5

これはなかなか膨大な作業で、関数を定義するたびに注釈を付ける必要がある。

5

なんとか半自動でやる方法は無いものかなぁ。

5

 

4
構文にも型情報が必要
5

 

5

if や cond 、let let* などの規定の構文(syntax)にも型情報が必要。

5

これは関数とは別に特別扱いで処理する必要がある。

5

 

4
Rubyのメソッドディスパッチの問題
5

 

5

Nendoは、残念なことに次のような記述を許してしまっている。

5
(str.chomp)
5

 

5

strという変数がRubyのString型であると判別できないと、chompというメソッドがString#chompだとはわからない。

5

これは、Nendoが動的型付け言語なのでstrがRubyのどの型なのか簡単にはわからないため。

5

静的解析できるようにするためには、strの型をアノテーションしてやらないいけないが、こいつはプログラマに余分な手間をかけさせてしまう。

5

お手軽にやりたいので、アノテーション無しにしたいところ。

5

 

5

解決策は、(str.chomp)のような 「. (ドット)によるメソッドコンビネーションは使えない」とすることかな。

5

その場合は、pureなchomp関数を定義する必要がある。

5
(chomp str)
5

 

5

自分が過去に書いたコードでも、str.sizeは多様している気がするので、そこは書き直す必要がある。

5

 

5

その他(備忘録)

5

 

4
デバッグ出力は特別扱い
5
#?=S式
5

という形式のデバッグ出力は、標準エラー出力にデバッグ表示するという副作用があるのだが、気軽にデバッグ出力を入れたいので型検査結果として「副作用なし」としたい。

5

 

5

おわりに

5

 

5

NendoはSchemeのサブセットであり、最初から静的型付けの言語とは反対の性質を持っているので、後付けでどこまでできるかという問題になりそうだ。

5

まあ、実際にはやってみないと何が出るかわからんというところですな。

5

ただ、JavaScript界隈では先駆者が多く存在し、JSX、Dartは型はoptionalで、指定が無ければ型推論で補うようになっているなど、参考にできるものはたくさんありそう。

5

TAPLを読むだけでなく、先行技術も調査しないといけないなぁ。

5

 

5

...comment disabled...