簡単な型システムを実装していく１５ STLC+...+Error (6)

typeof関数のRefとError関連のケースを部分型に対応させる。今回でエラーに関する話は最後。

Ref

以前書いたとおり、安易にRefにBottomを含む型を持たせると型安全性が破壊されてしまう。なのでRefに入る値の型にはBottomがまったくないという厳しめの制約をつける：

| ERef e ->
  let t = typeof env e in
  if contains_bottom t then failwith "type containing bottom passed to ref"
  else TRef t

これで

let f = fun () -> failwith "some error" in
if some_condition
  then f := fun () -> 1
  else f := fun () -> true;
f ()

のようなコードは最初の行で型エラーになる（TRef (TArrow (TUnit, TBottom))を作成しようとするため）。本当はif some_condition ...の部分でエラーを探知する方がいいとは思うのだが、thenとelseの式自体の型を見るだけだと両方ともTUnitで一致しているので難しい。型推論でやるような単一化があればfに代入されているのが違う型だとわかるのだろうが・・・。ここら辺はOCamlでいうところのValue Restrictionと同じ問題意識。

EDerefはパターンマッチでTBottomに対応するだけ：

| EDeref e -> (match typeof env e with
    | TRef t -> t
    | TBottom -> TBottom
    | _ -> failwith "non-ref passed to deref")

EAssign：

| EAssign(e1,e2) -> (match typeof env e1 with
    | TRef t when is_subtype (typeof env e2) t -> TUnit 
    | TRef _ -> failwith "type mismatch between ref and value"
    | TBottom -> ignore @@ typeof env e2; TUnit
    | _ -> failwith "ref type expected")

TRefの中身はTBottomを部分的にでも含むことができないのでtypeof env e1がTRef tのケースは型安全性が守られている。

typeof env e1がTBottomそのものな場合は型安全が守られているか怪しげかもしれない。

例えば以下のOCamlコード：

let x = failwith "some error" in
x := 1; x := true

これが型チェックを通ってしまう。がしかし実行時にはx:=1もx:=trueも実行されないので大丈夫なはず。代入するはずのRef値部分がTBottom型だということはそもそもその代入式に到達する前に例外が投げられている（なのでその代入式までプログラムが到達しない）という意味になる。

Error

エラーに対する型検査を部分型に対応させるのは簡単：

| EError -> TBottom
| ETry(e1, e2) -> join (typeof env e1) (typeof env e2)

ETryのtryとexceptの式の型が一致するかを確認する必要がある。それを部分型を考慮に入れるためにjoinでやっている。

次回

正直な話、部分型が必要な形でエラー処理を導入したことはかなり後悔している。ただBottomを追加しただけ（レコードのフィールドの部分集合などから生じる部分型などは完全に無視）だというのにほぼすべての箇所にかなり複雑な変更が必要になってしまった。

近いうちに再帰型と型コンストラクタを追加した型システムを作りたいと考えているが、エラーと部分型はややこしくしているので除いてしまうのがいいように思う。とりあえず一旦はSTLCから離れて型推論をやっていく。