Arantium Maestum

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

型推論を実装・改善していく1 純粋関数型な単相型推論(前編)

型推論がある型システムを実装した上で改善していく。

具体的には

  1. TaPLのType Reconstruction準拠の単相な型推論を純粋関数型な単一化で実装
  2. 型変数の作成と単一化を破壊的代入で行うようにする(効率化)
  3. 型推論をLet多相に拡張
  4. 型変数を汎化していいかの確認を効率化するための「レベル」の導入

をやっていった上でBoolやNat、RecordやVariantなどを追加していく。

1はTaPL準拠(https://github.com/hsk/simpletapl を参考にさせていただく)、2~4はGrow Your Own Type SystemsというレポジトリのAlgorithm W実装をベースにする。

というわけで今回と次回は純粋関数型な単相型推論の実装:

gist.github.com

言語

まずはサポートされる言語の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から返ってきた型tapplysubst関数で変換して返す。

ちなみにinfer関数というのはTaPLではreconとなっている。シリーズ名を「型推論」にしてあるのでinferの方がしっくりくるかなと思って統一してある。なんでTaPLではtype reconstructionという用語を使っているのだろう?

次回

次回はinferunifyapplysubstなどの関数の内容を見ていく。