前回に続いてバリアント型を追加していく話。今回はバリアント型を扱うための式とその式に対する型推論のロジックを見ていく。

式

バリアント型の値を作るETagと、パターンマッチでバリアントに保持されている値を取り出すECaseを追加：

type exp =
...
| ETag of string * exp * ty
| ECase of exp * (string * string * exp) list * ty

第一のポイントとして、どちらも最後にtyを持っていること。レコード型と同じく、あるモジュールの特定の位置で使われるタグは型推論するまでもなく何の型かわかる（すでに定義されているバリアント型の一つを特定できる）ので、型推論に入る前処理として「バリアントのタグが出てくる式には、その式が何の型かを持たせる」ということができ、型推論のロジックが非常に簡単になる。

ETagはタグとなる文字列と、そのタグに渡す式、そしてタグからわかるETag式の型の三要素で構成されている。タグが変数式ではなく文字列なのでA 1のようなコンストラクタ適用は関数適用ではないことに注意（これはOCamlなどとも一緒）。バリアントのコンストラクタをそのまま高階関数に渡すといったことはできない。

ECaseはパターンマッチ式。OCamlでいうところのmatch e with tag1 var1 -> res1 | tag2 var2 -> res2のような式を表す。

最初のexpがmatch e with ...のeにあたる
tag1 var1 -> res1というのがstring * string * expに対応する
... | ...となっているように、string * string * expの部分は|でわけられている箇所ごとに存在するので(string * string * exp) listとなる
最後にtag1, tag2の部分からどのバリアント型に対するパターンマッチかが一意に定まるので、そのバリアント型がtyとなる。

`typeof`

ETagとECaseに対する型推論を見ていく。

ETag

let rec typeof env level = function
...
| ETag(l,e,t) -> (match t with
  | TVariant lts -> unify (List.assoc l lts) (typeof env level e); t
  | _ -> failwith "Variant type expected in Variant Constructor annotation")

まず式に保持されている型に対してパターンマッチ。これがバリアント型でない場合はエラー（ここは前処理でバリアント型が必ず入るはずなのでassert falseでもいいかもしれない）。

正しくバリアントだった場合はTVariant ltsというパターンにマッチし、「タグと型のリスト」ltsが得られるので、List.assoc l ltsでその中からETag式で使われたタグlに対応する型を探す（見つからない場合は実行時エラーだが、そもそもETag(l,e,t)のtの部分はlから自動的に算出している前提なので見つからないことはあり得ないはず）。

コンストラクタに渡しているe式の型をtypeof env level eで推論し、List.assoc l ltsの結果と単一化する（タグに渡すべき式の型と実際に渡している式の型を合致させる）。unifyが成功したならETag式全体の型はtとなる。

ECase

| ECase(e,cases,t) -> (match t with
  | TVariant lts ->
    unify t (typeof env level e);
    if List.exists2 (fun (l1,_) (l2,_,_) -> l1 != l2) lts cases
      then failwith "Labels mismatch between cases and annotation";
    let ts = List.map2 (fun (_,t) (_,s,e) -> typeof ((s,t)::env) level e) lts cases in
    let t = List.hd ts in
    List.iter (unify t) (List.tl ts);
    t
  | _ -> failwith "Variant type expected in Case annotation")

比較的長く複雑なので分解して見ていく。

やはりまず式に保持されている型に対してパターンマッチしてバリアント型であることを確認（assert falseでいいはずなのも同様）：

| ECase(e,cases,t) -> (match t with
  | TVariant lts ->
  ...
  | _ -> failwith "Variant type expected in Case annotation")

eがt型であるはずなので単一化：

    unify t (typeof env level e);

次にパターンマッチで使われるタグが型のタグと一致しているかを確認：

    if List.exists2 (fun (l1,_) (l2,_,_) -> l1 != l2) lts cases
      then failwith "Labels mismatch between cases and annotation";

ラベルが一致しなければエラー。

実装で楽をするためにパターンマッチのケースは網羅的かつバリアント型の定義と同じ順番でタグが出ないといけないようになっている（ここは前処理で順番をソートしたりしてもいいかもしれない）。現在はパターンマッチが非常に簡単なのでこれでも問題ないはずだが、タプルに対するマッチと組み合わせたりガードを使えるようになるとこのやり方では破綻する。

次の部分は少しややこしい：

    let ts = List.map2 (fun (_,t) (_,s,e) -> typeof ((s,t)::env) level e) lts cases in

何をしたいかというとmatch e with tag1 var1 -> exp1 | tag2 var2 -> exp2 ...となっている場合のexp1やexp2の型を求めようとしている。例えばexp1の型を求めるにはtag1 var1に対応する型type1をltsから取ってきてtypeof (var1, type1)::env level exp1とする（ltsとcasesのタグの順番が同一なことも利用している）。

これをltsとcasesのすべてに対してList.map2でおこなっていていて、その結果であるtsはパターンマッチ全ケースの結果の型のリストとなる

まずtsの先頭要素をとり、それ以外の要素すべてと順次単一化する：

    let t = List.hd ts in
    List.iter (unify t) (List.tl ts);

その上で単一化された型tを返している。この「tsの要素すべてが単一化されたt」がECase式全体の型となる。

次回

次は再帰関数のための不動点コンビネータを表すFix式の型推論。

Arantium Maestum

プログラミング、囲碁、読書の話題

Hindley Milner型推論に機能を追加していく７ Variant型の追加（後編）

式

`typeof`

ETag

ECase

次回