型推論を実装・改善していく1 純粋関数型な単相型推論(前編)
型推論がある型システムを実装した上で改善していく。
具体的には
- TaPLのType Reconstruction準拠の単相な型推論を純粋関数型な単一化で実装
- 型変数の作成と単一化を破壊的代入で行うようにする(効率化)
- 型推論をLet多相に拡張
- 型変数を汎化していいかの確認を効率化するための「レベル」の導入
をやっていった上でBoolやNat、RecordやVariantなどを追加していく。
1はTaPL準拠(https://github.com/hsk/simpletapl を参考にさせていただく)、2~4はGrow Your Own Type SystemsというレポジトリのAlgorithm W実装をベースにする。
というわけで今回と次回は純粋関数型な単相型推論の実装:
言語
まずはサポートされる言語のASTや型を見ていく。
例によって先に型:
type ty = | TVar of int | TArrow of ty * ty
かなりミニマルなのがわかると思う。型変数と関数型のみ。整数も真偽もユニットさえなし。実用的な言語ではまったくないが、型推論のロジックを追うにはここからはじめるのが良さそう。一つの注意点として、ref
をまったく使っておらず型変数の内容を破壊的に変更することなどはできない。これは後々の変更ポイントとなる。
式:
type exp = | EVar of string | EAbs of string * exp | EApp of exp * exp
単純型付きラムダ計算の式とほぼ同じ。ただし関数の引数に対する型注釈がないことに注意(型推論するため)。
型推論・型検査のtypeof
関数
let typeof env new_tvar constr e = let (t, new_tvar, constr1) = infer env new_tvar e in let constr = unify (constr @ constr1) in let t = applysubst constr t in (t, new_tvar, constr)
まず戻り値が(t, new_tvar, constr)
になっている。今まではtypeof
で式の型だけを算出していたのだが、ユニークな型変数を振るための情報であるnew_tvar
と、型同士の同値関係などの制約を集めたconstr
も返るようになっている。純粋関数型のコードなので引数と返り値でずらずらとこういった情報を引き回す必要が出てくる。Haskellだったらステートモナドの出番なのだろうが・・・。
typeof
の大まかな流れとしては、まず式e
の型を(外部の型制約や同値関係は無視して)infer
関数で求める。そこから出てきた制約constr1
を外部からきた制約constr
と併せてunify
関数で整合させる。その最終的に整合性のある制約constr
を使ってinfer
から返ってきた型t
をapplysubst
関数で変換して返す。
ちなみにinfer
関数というのはTaPLではrecon
となっている。シリーズ名を「型推論」にしてあるのでinfer
の方がしっくりくるかなと思って統一してある。なんでTaPLではtype reconstructionという用語を使っているのだろう?
次回
次回はinfer
、unify
、applysubst
などの関数の内容を見ていく。