Arantium Maestum

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

Hindley Milner型推論に機能を追加していく3 Int型の追加

前回のBoolに続いてInt型とそれに関連する式であるIntリテラル、AddとIsZeroを実装する。

Int型の追加:

type ty =
...
| TInt

Intリテラル、Add、IsZeroを追加:

type exp =
...
| EInt of int
| EAdd of exp * exp
| EIsZero of exp

AddはInt型の式二つをとって足した結果のInt型な値を返す。

IsZeroはあるInt型の式の値が0かどうかをBool型の値として返す。

typeof

追加した三つの式のパターンを「型推論・型検査を行う大元の関数」typeofに追加していく。

まずはEInt:

let rec typeof env level = function
...
| EInt _ -> TInt

Intリテラルは当然Int型になる。

Add:

| EAdd(e1,e2) ->
  unify (typeof env level e1) TInt;
  unify (typeof env level e2) TInt;
  TInt

まず引数となる二つの式の型をInt型と単一化する。このステップは「式の型をIntとみなすことで矛盾が生じないかの検査」と「矛盾が生じない場合、それに合わせた型変数などの情報の更新」の二つのことを同時におこなっている。

もし単一化が成功したなら式全体の型としてTIntを返す。

IsZero:

| EIsZero e ->
  unify (typeof env level e) TInt;
  TBool

Addと似た理屈で、引数をTIntと単一化した上でTBoolを返す。

他の関数

他の関数はパターンマッチのTUnitTBoolとまったく同じ箇所にTIntも追加するだけ。

次回

次はタプルの実装。型検査だけの時はタプルは飛ばして直接レコードの実装に行ったのだが、型推論もある場合少し複雑なのでワンクッションでタプルをまず見ていく。

今回のコード

長くなってきたのでリンクのみ:

Hindley Milner Type Inference with Unit, Bool, Int · GitHub