Hindley-Milnerの型推論

アルゴリズムについてのメモ

  • 構文: 変数参照(ref)、関数適用(apply)、lambda、let, letrec
    • 整数や文字列などは特別なref扱いで
    • 型宣言はない
  • 型: 多相型と具体型、単一型(アトム)と組合せ型(関数とかタプルとか)
    • 推論型: 構文上の問題から仮に割り当て、チェック時には仮に多相型のようにユニファイしていくことで固定化する具体型。ユニファイでは多相型のように処理するが、処理後は具体型として参照する内部型。仮引数や再帰関数など。
  • 型環境: [(識別子, 型)]
    • 構文ツリーでのlambdaやletごとに親子構造をとる継承式辞書
    • built-inの名前の型をトップに入れておく
  • 型チェック: (構文木、型環境) -> 型 or 型エラー
    • (構文ノードの種類ごとに再帰的に処理、結果としてそのノードの型を取り出す)
    • 変数参照: 型環境から取り出す
    • 関数適用: 使っている関数の型と、引数と戻り値の型からなる関数型をユニファイ、戻り値の型を返す
    • 関数(lambda): 子の型環境をつくり、そこに仮引数識別子をキーに、値をそれぞれ新たな推論型にして入れる。その型環境を使って本体の型チェックをして、それを最初の仮引数型と戻り方からなる関数型を作り、それを返す
    • let: 子の型環境をつくり、引数識別子と、値を型チェックして入れる。その型環境を使って本体を型チェックしてその型を返す
    • letrec: letと同じく型環境を新たに作るが、まず変数識別子には推論型を入れて、その型環境を使って変数値の型チェックをする。その結果の(関数)型から最初の変数推論型をユニファイする(推論型の具体型が固定される)。その後、本体を型チェックしてその型を返す。
  • ユニファイ: (型1、型2) -> 型エラー
    • 二つの型を同じ型とみなす。多相型の場合、具体型に落としていく。その過程でミスマッチを見つけると型エラーにする。

メモ

  • 関数では仮引数を推論型として扱い、内部をチェックしいくときに、具体的な型へと落ちていく。落ちなければそのまま多相型になる。
  • ユニファイでは、型の構造比較を再帰的に行う。多相型はその時点で具体化される。複数回ユニファイされた多相型で別なものへの具体化が行われようとすると、型エラー。
  • 推論型はユニファイ時の具体化の結果を後々利用する処理上の型。式の型ではない。
  • 単体型は、無引数の関数型にすると、関数型だけ処理すればよくなる
  • エラーはユニファイ単位ごとに出すことになるが、構文単位で出さないと場所がわかりにくくなりそう。
  • 構文に型宣言を入れるとしたら、そこでユニファイを行うことになる。
    • 推論型のところはそのまま具体型にすることになる


リソース