副作用の無いコードの静的解析について(1)
だいぶ前に、[Nendo]に型検査を入れて副作用の無いコードを静的解析で保証したいという話題を書いた。 ( 2011-10-07Nendo*Ruby コードブロックに副作用が混在するかを検出できるかどうか ) あれから時間が経ったけど、諦めずに考えているのであった。もう２年も経ったのか…
最近TAPL(第８章、第９章)を読んで、理論的なところを知ると、いろいろ気づいたので自分用のメモとして書いておく。
欲しい機能
[Nendo]にどんな機能を追加したいかというと、
(pure S式)
と書くと、コンパイル時に静的解析して「S式の中に副作用が無いことを保証してくれる」機能だ。
例えば、次のコードは静的解析で実行前にエラーとなる。
(pure
(define a 0)
(set! a 1))
次。func1からの関数呼び出しがどれだけ深かろうが静的に検査して欲しい。
(pure
(func1))
また、次のコードは副作用が無いと判断し、エラー無しで通って欲しい。
(pure
(define lst '(1 2 3))
(define result
(map
(lambda (x)
(+ x 1))
lst)))
ただ、そう簡単にはいかないのが世の中というもの。
問題点
- アノテーションの記述量が膨大になる
静的解析するためには、事前に型情報のようなものが必要となる。 型情報といっても、副作用が無いと考えられる関数全てに「pure」の注釈を付けるだけなので、StringやIntegerなどの型情報は不要だ。 最低限、pureな全ての関数には必要。
これはなかなか膨大な作業で、関数を定義するたびに注釈を付ける必要がある。 なんとか半自動でやる方法は無いものかなぁ。
- 構文にも型情報が必要
if や cond 、let let* などの規定の構文(syntax)にも型情報が必要。 これは関数とは別に特別扱いで処理する必要がある。
- Rubyのメソッドディスパッチの問題
Nendoは、残念なことに次のような記述を許してしまっている。
(str.chomp)
strという変数がRubyのString型であると判別できないと、chompというメソッドがString#chompだとはわからない。 これは、Nendoが動的型付け言語なのでstrがRubyのどの型なのか簡単にはわからないため。 静的解析できるようにするためには、strの型をアノテーションしてやらないいけないが、こいつはプログラマに余分な手間をかけさせてしまう。 お手軽にやりたいので、アノテーション無しにしたいところ。
解決策は、(str.chomp)のような 「. (ドット)によるメソッドコンビネーションは使えない」とすることかな。 その場合は、pureなchomp関数を定義する必要がある。
(chomp str)
自分が過去に書いたコードでも、str.sizeは多様している気がするので、そこは書き直す必要がある。
その他(備忘録)
- デバッグ出力は特別扱い
#?=S式という形式のデバッグ出力は、標準エラー出力にデバッグ表示するという副作用があるのだが、気軽にデバッグ出力を入れたいので型検査結果として「副作用なし」としたい。
おわりに
[Nendo]はSchemeのサブセットであり、最初から静的型付けの言語とは反対の性質を持っているので、後付けでどこまでできるかという問題になりそうだ。 まあ、実際にはやってみないと何が出るかわからんというところですな。 ただ、JavaScript界隈では先駆者が多く存在し、JSX、Dartは型はoptionalで、指定が無ければ型推論で補うようになっているなど、参考にできるものはたくさんありそう。 TAPLを読むだけでなく、先行技術も調査しないといけないなぁ。