簡単な型システムを実装していく１１ STLC+...+Error (2)
前回書いたとおり、エラー式の型であるBottom型が部分型として正しく振る舞えるような変更を加えていく必要がある。
Bottom型に関して注意しておくべき最大のポイントは以下の二つ：
- Bottom型はすべての型の部分型である。ということはBottom型の式は他のどんな型が期待されている箇所にあっても型検査を通る。
- Bottom型はプログラマによる型注釈の中では使えない。
というわけでこれから数回にわけて見ていくコード全容：
見ての通り非常に長くなっている。追加したコード量もこれまでのものと比べて圧倒的に多い。
今回はまず「型システムが扱う型」がBottom型とどう関係するかを見ていく。
型
実装する型システムが扱う型の種類や内容に関して、前回と比べて変更はない。ただし、それ以外の部分を実装・改装するにあたって重要なポイントは、Bottom型以外でも再帰的になっている型の中にはBottom型が現れる可能性があるということで、それらを一旦確認しておく。
つまり：
type ty = | TArrow of ty * ty | TBool | TNat | TRecord of (string * ty) list | TVariant of (string * ty) list | TUnit | TRef of ty | TBottom
この中ではTArrow、TRecord、TVariant、TRefの四つに注意する必要が出てくる。これらの中にTBottomが入っている可能性があり、その場合の部分型関係はちゃんと考慮に入れて実装しなければいけない。それ以外の型、例えばTBoolやTNatはTBottomがそれらの部分型である、という点以外では難しいことはない。
TArrow
関数の型を表すTArrowは「引数の型」と「返り値の型」を保持する。このうち「引数の型」には、今回実装している型システムの上ではTBottomは出てくることはない。型推論のないSTLCなので、関数の引数は型が明示的に注釈されている必要があり、そしてTBottomは型注釈には使えない。
なので「返り値の型」だけを心配していればよい。ちなみに部分型のややこしい話題の一つである共変・反変に関して、引数がBottomになりえないので反変にならないというのは少し問題を簡単にしてくれている。
TVariant
バリアントもTArrowの引数型と同じ理屈（つまりバリアントの保持する型はすべてプログラマの注釈から来ている）でTBottomやそれが含まれる型を考慮に入れる必要はない。
TRecord
レコードは少しややこしい。
{x: bottom, ...}といった型はありえない。{x=failwith "some error", y=5}といったコードは{x:bottom, y:int}ではなく式全体の型がbottomになるため。
しかし{x: int -> bottom, ...}などといった型はあり得る。{x: int -> bottom, y: bool -> bool}は{x: int -> int, y: bool -> bool}の部分型となる。
さらにややこしい点としては{x: int -> bottom, y: bool -> bool}と{x: int -> int, y: bool -> bottom}はどちらもお互いの部分型ではないのだが、型検査時に比較した場合「同一である」と見做す必要がある。
TRef
ミュータブルなセルは実はBottomとの相性はかなり悪い。というのも気をつけないと簡単に型安全性を破壊できてしまうからだ。
let myref = ref (fun () -> failwith "some error") in if some_condition then myref := (fun () -> 1) else myref := (fun () -> "hello"); !myref ()
myref := (fun () -> 1)もmyref := (fun () -> "hello")も型としてはunitであるので型チェックは通ってしまう。最後の行で返される値は1か"hello"か、つまりint型かstring型か、ということがsome_conditionの値によって動的に決定されてしまう。
OCamlではこの問題を避けるためにvalue restrictionと言ってrefが多相的な型を取れないようにしてある。今回実装する型システムでも似たように、refの中にはBottomが入っていてはいけないという厳しめの制約をつける。
次回
次回からは実装の中身を見ていく。まずは部分型関係を調べるために追加された各種ヘルパ関数について。
