型

バリアント型を追加：

type ty =
...
| TVariant of (string * ty) list

「タグを表すstringとそのタグに紐づけられる型ty」のリストとして表現されている。

実装を簡単にするために「タグに紐づけられる型は一つ」としている。その一つの型としてタプルを使えるので表現力としてはそこまで問題はないはずだが、例えばOCamlでは

type t1 = A of int * string
type t2 = B of (int * string)

というのは言語上でも内部実装上でも違っている（例えばlet x = (1, "hello") in A xはできないがlet x = (1, "hello") in B xはできる）。この違いは今回の実装では表現できない。

このような実装も考えられる:

type ty =
...
| TVariant of (string * ty list) list

これならtype t1 = A of int * string; type t2 = B of (int * string)を別のものとして表現できる。がしかし型システムの実装上はあまり面白味はない割に手間が増えそう（今回追加するバリアント用の処理に加えてタプルの処理に似たものも一緒にやる必要が生じる）。余裕があったらその実装もやってみて対比させるのも面白いかもしれない。

レコードとの類似性

ちなみに今回のバリアントの中身はレコードのものと完全に一致している：

type ty =
...
| TRecord of (string * ty) list
| TVariant of (string * ty) list

レコードは「フィールドと型」の組のリスト、バリアントは「タグと型」の組のリストだ。実際にプログラミングで使われる際にはレコードとバリアントではかなり様相が違うが、型の中身としては同一。

そしてその結果、型推論に使われる関数でty型に対してパターンマッチするもの（ほとんどがそうだ）はレコードとバリアントのケースでほぼ同一な実装となる：

let rec generalize level ty = match ty with
...
| TRecord lts -> TRecord (List.map (fun (l,t) -> (l, generalize level t)) lts)
| TVariant lts -> TVariant (List.map (fun (l,t) -> (l, generalize level t)) lts)

let instantiate level ty =
  let id_var_hash = Hashtbl.create 10 in
  let rec f ty = match ty with
  ...
  | TRecord lts -> TRecord (List.map (fun (l,t) -> (l, f t)) lts)
  | TVariant lts -> TVariant (List.map (fun (l,t) -> (l, f t)) lts)
  in f ty

let rec unify t1 t2 = match t1, t2 with
...
| TRecord lts1, TRecord lts2 ->
  if List.map fst lts1 != List.map fst lts2 then failwith "Cannot unify records with mismatched labels";
  List.iter2 unify (List.map snd lts1) (List.map snd lts2)
| TVariant lts1, TVariant lts2 ->
  if List.map fst lts1 != List.map fst lts2 then failwith "Cannot unify variants with mismatched labels";
  List.iter2 unify (List.map snd lts1) (List.map snd lts2)
...

let rec occursin id = function
...
| TRecord lts -> List.exists (occursin id) (List.map snd lts)
| TVariant lts -> List.exists (occursin id) (List.map snd lts)

let rec adjustlevel level = function
...
| TRecord lts -> List.iter (adjustlevel level) (List.map snd lts)
| TVariant lts -> List.iter (adjustlevel level) (List.map snd lts)

occursinとadjustlevelに至っては| TRecord lts | TVariant lts -> ...とやってもいいレベルの同一さ。他のものは非常にマイナーな違い（コンストラクタを付け直すところとかエラーメッセージなど）はあるが、やはりほぼ一致。

この同一性は圏論的に直積と直和（coproduct）が双対であることと関連してるんだろうか。してるとは思うのだが、それが何か役に立つ情報なのかはわからない。

次回

次回はバリアント型の値を作るETag式とパターンマッチするECase式、それらに対する型推論のコードを見ていく。

Arantium Maestum

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

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

型

レコードとの類似性

次回