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

前回に続いて、エラー処理のある言語を型検査できる型システムを実装する話。今回は部分型全般やBottom型に対するチェックを行うヘルパ関数について。

導入するヘルパ関数は四つ：

• ある型がある型の部分型かどうかを調べるis_subtype
• 部分型関係を考慮に入れて二つの型が同一だと見做せるかを調べるeq_upto_subtype
• 二つの型の上位型を算出するjoin
• ある型がBottomを構成要素として持っているか調べるcontains_bottom

is_subtype

is_subtypeは第一引数t1が第二引数t2の部分型かどうかを調べる。逆はしないので注意。

let rec is_subtype t1 t2 = match t1, t2 with
  | _, _ when t1 = t2 -> true
  | TBottom, _ -> true

最初の二つのケースは簡単。もしt1とt2が同一であればt1はt2の部分型だし、t1がBottom型なら同じくt1はt2の部分型だ（Bottom型はすべての型の部分型なので）。

TArrowの場合：

  | TArrow(targ1,tret1), TArrow(targ2,tret2) ->
    is_subtype targ2 targ1 && is_subtype tret1 tret2

関数というのは部分型に関しては、引数に関して反変なのでis_subtype targ2 targ1、返り値に関しては共変なのでis_subtype tret1 tret2と再帰的に部分型関係を調べる呼び出しの引数の順序が違っている。

実際にはSTLCの関数は引数が明示的に注釈されている必要があり、プログラマによる注釈にはbottom型は出てこれないので引数targに関しては部分型を調べる必要はなくtarg1 = targ2と直接比較してもいいのだが・・・。あるいは引数部分にbottomが出てきたらエラーを投げるようにしてもいいかもしれない。

TRecordの場合：

  | TRecord lts1, TRecord lts2 ->
    List.map fst lts1 = List.map fst lts2 && 
    List.for_all2 is_subtype (List.map snd lts1) (List.map snd lts2)

レコードのすべてのフィールドに関して、そもそもラベルが一致しているかを確認し、そして各フィールドの型一つ一つに関して部分型であることを確認する。

それ以外：

  | _ -> false

他のケースに関しては単にfalseを返していい（一番最初に「まったく同じ型かどうか」というケースが来ているので）。

eq_upto_subtype

eq_upto_subtypeはis_subtypeと非常に似ている：

let rec eq_upto_subtype t1 t2 = match t1, t2 with
  | _, _ when t1 = t2 -> true
  | TBottom, _ | _, TBottom -> true
  | TArrow(targ1,tret1), TArrow(targ2,tret2) ->
    eq_upto_subtype targ2 targ1 && eq_upto_subtype tret1 tret2
  | TRecord lts1, TRecord lts2 ->
    List.for_all2 eq_upto_subtype (List.map snd lts1) (List.map snd lts2)
  | _ -> false

is_subtypeとの違いとしてはt1, t2のどちらがTBottomでもtrueになっている件と、再帰的呼び出しが当然ながらis_subtypeではなくeq_upto_subtypeであること。

実は元々この関数はlet rec eq_upto_subtype t1 t2 = is_subtype t1 t2 || is_subtype t2 t1と実装していたのだが、前回の記事でも書いた通りレコード型によってはt1 = {x:int->bottom, y:bool->bool}, t2 = {x:int->int, y:bool->bottom}のようなお互いに部分型ではないのに同一視できるような二つの型があり得てしまうので、それを踏まえて修正。

join

joinは「上位型」（部分型の反対の概念）を算出するための関数。部分型関係がない場合はエラー。

is_subtypeで片方が部分型なのがわかったら、もう片方を返す：

let rec join t1 t2 = match t1, t2 with
| _, _ when is_subtype t1 t2 -> t2
| _, _ when is_subtype t2 t1 -> t1

関数型の場合は、引数の型は（STLCなので）完全な合致をする場合、返り値のjoin結果を持つTArrow型を返す：

| TArrow(targ1,tret1), TArrow(targ2,tret2) ->
  if targ1 = targ2
    then TArrow(targ1, join tret1 tret2)
    else failwith "type mismatch in function params"

レコードのケースが一番ややこしい。フィールドのラベルが一致することを確認して、個別のフィールドに関して上位型を計算していって、最終的にすべてを合わせたTRecord型を返す：

| TRecord lts1, TRecord lts2 ->
  let labels = List.map fst lts1 in
  if labels = List.map fst lts2
    then TRecord (List.combine labels  (List.map2 join (List.map snd lts1) (List.map snd lts2)))
    else failwith "label mismatch in record"

上記のケース以外では部分型・上位型関係はないとみなしてエラー：

| _ -> failwith "unable to join types"

contains_bottom

型がTBottomを保持しているか確認するcontains_bottom：

let rec contains_bottom = function
| TBottom -> true
| TArrow(_,t) -> contains_bottom t 
| TRecord lts -> List.exists contains_bottom (List.map snd lts)
| _ -> false

TRefやTVariantがTBoolを保持できないのをいいことに検査すらしない。本当だったらやっぱりassert falseぐらいしてもいいかもしれないが・・・。

次回

次回からはtypeof関数の各ケースがこれらヘルパ関数を使ってどのように変更されていくかを見ていく。