簡単な型システムを実装していく７ STLC+Bool+Nat+Let+Record+Variant

型システムにバリアント型とケースに対するパターンマッチを追加する。

こういうやつ：

type t =
  Name of string
| Id of int

let to_str = function
  Name s -> s
| Id n -> string_of_int n

代数的データ型における直和型であり、前回の直積型と合わせるとぐっと関数型プログラミングっぽさが出てきてテンションが上がる。

gist.github.com

型

バリアント型を追加：

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

バリアントはName of string | Id of intのように「コンストラクタと型のリスト」となっているので、TVariantはコンストラクタを表す文字列と型のリストを持つ。

式

式としてはコンストラクタによってバリアント型の値を作成するETagとバリアント型に対するパターンマッチのECaseを追加：

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

ETagはコンストラクタと式だけではなく、どの型に属するかを明示的に注釈する必要がある。これはOCamlのバリアントとは違っていて、OCamlだとコンストラクタがモジュール内でユニークであるという制約があるのでこの型注釈が省けるらしい。

ECaseは式expに対してのパターンマッチで、リストに含まれているいずれかのコンストラクタに合致する場合、コンストラクタが保持していたデータを変数に束縛した上で本体の式を評価する、というロジックになっている。ECase of パターンマッチ対象 * (コンストラクタ名 * (変数 * 本体の式)) listという構造だ。

ちなみに関数型プログラミング言語によく見られるような、レコード、リテラル、ネストしたデータ型などに対するパターンマッチはサポートしていない。パターンマッチはそれ自体がかなり深掘りしがいのあるトピックなので、機会があったら別に調べていろいろ実装したい。

typeof関数

typeof関数にETagとECaseのケースを追加する。

まずはETag：

let rec typeof env = function
...
| ETag(l,e,t) -> (match t with
    | TVariant lts -> 
      let t' = List.assoc l lts in
      if typeof env e = t' then t
      else failwith "field does not have expected type"
    | _ -> failwith "annotation is not a variant type")

コンストラクタに渡される「引数」である式eがバリアント型の対応するコンストラクタの引数の型と合致しているかを確認してから、全体の式をバリアント型として返す。

パターンマッチECaseの型検査：

| ECase(e, cases) -> (match typeof env e with
    | TVariant lts ->
      let labels = List.map fst cases in
      let is_label_in_type l = List.mem_assoc l lts in
      if not (List.for_all is_label_in_type labels) then failwith "label mismatch between case and type";
      let typeof_case_exp (l,(var,exp)) = typeof ((var,List.assoc l lts)::env) exp in
      let ts = List.map typeof_case_exp cases in
      if not (List.for_all (fun t -> t = List.hd ts) ts) then failwith "type mismatch in arms of case";
      List.hd ts
    | _ -> failwith "variant type expected")

ややこしいので部分的に見ていく。

まず外側から：

 (match typeof env e with
    | TVariant lts -> ...
    | _ -> failwith "variant type expected")

バリアント型じゃない式に対するECaseパターンマッチはエラーになる。

次にTVariant ltsに関連する最初の3行：

    | TVariant lts ->
      let labels = List.map fst cases in
      let is_label_in_type l = List.mem_assoc l lts in
      if not (List.for_all is_label_in_type labels) then failwith "label mismatch between case and type";
      ...

もしECasesのパターンに使われているラベルの一つでも型のコンストラクタの集合に含まれていないならエラー。この実装だと網羅性検査はしないようになっている。網羅性検査をするなら逆にバリアント型のラベルがすべてECaseのパターンに含まれているか「も」調べる必要がある。

次の3行：

    | TVariant lts ->
      ...
      let typeof_case_exp (l,(var,exp)) = typeof ((var,List.assoc l lts)::env) exp in
      let ts = List.map typeof_case_exp cases in
      if not (List.for_all (fun t -> t = List.hd ts) ts) then failwith "type mismatch in arms of case";
      ...

各ケースの型を再帰的typeofで調べて（環境を拡張する必要があるのでややこしい）、すべてのケースで同じ型になっていることを確認する。型が一つでも違っていたらエラー。

最後に返す型：

    | TVariant lts ->
      ...
      List.hd ts

前述のチェックでエラーにならない場合はパターンマッチのすべてのケースが同じ型なのでtsの先頭の型をとる。（ケースのリストが空だったら実行時エラーだが構文上あり得ない）

このECaseに対する処理が「簡単な型システムを実装していく」シリーズここまでで一番長いコードだった。それにしても実際に読み書きしてみれば当たり前のことしかしていない、ということがわかったのは嬉しい。（ただし記事を書くために見返していてバグを見つけて慌てて修正したのは内緒だ）

次回

次回は再帰を可能とするための不動点オペレータFixを追加する。