アンダースタンディング コンピュテーション ―単純な機械から不可能なプログラムまで

9.2

 静的意味論

305

9.2.2

　利点と制限

構築してきた型システムを使うことで、基本的なエラーが回避できます。これら静的意味論にした

がって、プログラムの「おもちゃ」バージョンを実行することで、元のプログラムの各ポイントにおけ

る値の型がどうなるかがわかります。そして、それらの型が実行時にその動的意味論がやろうとする

ことに正しくマッチしているか、チェックすることができます。このプログラムの「おもちゃ」バージョ

ンの解釈は単純なので、複雑なことをせずに簡単にチェックできるという利点がありますが、プログラ

ムを評価したときに起こることの一部の情報しか得られないという制限があります。たとえば、永久に

実行するプログラムをチェックしてみましょう。

>>

statement =

Sequence.new(

Assign.new(:x, Number.new(0)),

While.new(

Boolean.new(true),

Assign.new(:x, Add.new(Variable.new(:x), Number.new(1)))

)

)

=> «x = 0; while (true) { x = x + 1 }»

>>

statement.type({ x: Type::NUMBER })

=> #<Type void>

>>

statement.evaluate({})

SystemStackError: stack level too deep

これは明らかに愚かなプログラムですが、型エラーは