今回からHindley Milner型推論の要であるLet多相を実装していく。

これまで見てきた型推論は単相な関数しか扱えなかった。例えばこのようなコードはOCamlでは通る：

utop # let id x = x = x in id 1 && id "hello";;
- : bool = true

しかし単相的な型推論では通らない（そもそも整数型も文字列型もないことには目を瞑るとしても）。何故ならid 1について推論した時点でidの型はint -> intだと推論されて、その次のid "hello"で型が合致しないと判定されるからだ。

OCamlでもこんなコードは通らない：

utop # (fun id -> id 1 && id "hello") (fun x -> x = x);;
Line 1, characters 22-29:
Error: This expression has type string but an expression was expected of type int

あくまでLetを通して定義される変数が束縛される関数についての多相性を認める、ということでlet-bound polymorphism（Let多相）と呼ばれている。詳しくはTaPLの解説を参照してほしい。

これからこのLet多相を実装・効率化していく。

というわけでコード全容：

gist.github.com

今回は型や式、変数生成、そしてtypeof関数についての変更を見ていく。typeofで使われるgeneralizeやinstantiateの詳細、そしてmatch_fun_tyなどへの変更については次回。

型

型を表すty型：

type ty =
| TVar of tvar ref
| TArrow of ty * ty
and tvar =
| Unbound of int
| Link of ty
| Generic of int (* 追加 *)

型変数の中身の種類としてUnboundとLinkがあったところにGeneric of intが加わった。これはいわゆる全称型な型変数で、例えばTVar {contents=Generic 1}はfor all a. aという型を表し、TArrow(TVar {contents=Generic 1}, TVar {contents=Unbound 2})はfor all a. a->bを表す。

式

式の種類には新しくLetを追加：

type exp =
| EVar of string
| EAbs of string * exp
| EApp of exp * exp
| ELet of string * exp * exp (* 追加 *)

ELetの最初のstringは変数名、次のexpは束縛される式、最後のexpはbodyとなる式である。

一例としてlet x = f y in g xはELet('x', EApp(EVar("f"), EVar("y")), EApp(EVar("g"), EVar("x")))となる。

`new_tvar`

let new_tvar =
  let i = ref 0 in
  let f () = incr i; TVar(ref @@ Unbound !i) in
  f

新しい型変数を作成するnew_tvar関数は変更なし。必ずunboundな型変数を返す。新しいgenericな型変数を返すような関数はなし。

詳細は次回に譲るがgenericな型変数はunboundな型変数が特定の条件で汎化するので、新しいidを振られるのではなく元のUnboundのidがそのまま使われる。

ちなみに「Grow Your Own Type System」の実装ではnew_gen_varは実装されていて、パーサの中で利用されている。つまり型注釈として多相な型を書いた場合は「まったく新しいgeneric型変数」が必要になる。そもそも今回実装している型システムには型注釈がないので問題とならない。

`typeof`

型推論・型検査の大元な関数であるtypeofに対しての変更は以下のとおり：

Let式に対するケースをパターンマッチに追加。letで束縛される変数の型は汎化（自由な型変数を全称化）する
変数式を型推論する時、返ってきた型が全称型だった場合は（その後の型推論のため）全称化された型変数に新しい具体的な型変数を振る

というわけで実装をパターンマッチのケースごとに見ていく。

式レベルの変数（型変数ではないことに注意）を表すEVar：

let rec typeof env = function
| EVar s -> instantiate (List.assoc s env)

今までは単にList.assoc s envとしていたのが、その結果をinstantiate関数に適用している。instantiateについては次回の記事で解説するが、「型に含まれている汎化・全称化された型変数に新しく型変数を振って新しい型を作る」という処理になる。後述のLetで束縛される変数には型環境に汎化された型がマッピングされ得るが、その変数がLetのbody内で使われる個別のポイントではその型が全称なままではなく具体的なものとして推論される必要がある。

ラムダ抽象のEAbsと関数適用のEApp：

| EAbs(sparam, fbody) ->
  let tparam = new_tvar () in
  let tret = typeof ((sparam,tparam)::env) fbody in
  TArrow(tparam,tret)
| EApp(func, arg) ->
  let tfunc = typeof env func in
  let targ = typeof env arg in
  match_fun_ty tfunc targ

これらに関してはまったく変更なし。ただしmatch_fun_tyの内部は少し変更が加わっているので次回で解説。

今回追加されたLet式のELet：

| ELet(svar, e, ebody) ->
  let tvar = typeof env e in
  let tgen = generalize (List.map snd env) tvar in
  typeof ((svar,tgen)::env) ebody

単相な型推論だったら let tvar = typeof env e in typeof ((svar,tvar)::env) ebodyとしているところに、let tgen = generalize (List.map snd env) tvar ...という処理を追加しているのがポイント。let x = e1 of e2のe1に対して型推論して、その中にある自由な型変数をgeneralizeで全称化している。その時に「型変数が自由かどうか」はe1の中を見るだけではわからず、その型変数が型環境に捕捉されていないかも調べる必要があるのでgeneralizeの引数として(List.map snd env)を与えている（これらが環境上で束縛されている型のリストになる）。generalizeの内部実装についての話は例によって次回。

次回

次回はgeneralize、instantiateの実装が主体。ついでにmatch_fun_tyなどがどう変更されたかなども見ていく。

Arantium Maestum

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

型推論を実装・改善していく７　Let多相型推論（前編）

型

式

`new_tvar`

`typeof`

次回