なぜ型推論が必要なのか

インスタンス関係の実装さえあれば、関数適用の都度、実引数の評価値を検査すればいい。それに、多相なんぞ面倒臭いことを実装する必要もない。なんで必要なのか。

実引数の値を型検査すると、膨大な値をすべて走査しなくてはいけなくなる

型推論器がやること

• なるたけ関数適用をせずに、その式が返し得る型を返す
• 同期的に推論したい
• Tの部分型が期待される箇所に式eが適切かどうかは、eの推論Sが部分型関係 S <: E を満たすかどうかで判断する
  • Numを期待する箇所に0や1ではなくNumそれ自身が置かれた時、NumがNumに推論されると Num <: Num なので型検査に通ってしまう。そこで、Numのような型は、Allに昇格して推論する

型推論アルゴリズム

• Value?
  • if 型? → All
  • otherwise（インスタンス値） → それ自身
• Exp?
  • Sym
    • 自由変数? → 参照式をevalし、infer
    • otherwise → 参照式をinfer
  • Call
    • 関数は「型構築子」? → Call式全体をeval
      • struct, union関数のような例があるから
    • otherwise → 戻り値の型
  • Scope
    • 戻り値がある → 戻り値をinfer
    • ない → ()
  • EFn
    • 仮引数をevalし、本体をinfer、TyFnをつくる
  • ETyFn → All
  • EVec, EDict
    • restやoptionalが存在するなどしたら All
    • 子要素の推論結果からVec, TyVec, Dict, TyDictをつくる

型推論例

[(+ 1 2) 3] -- [Num 3]
_|_ -- _
(=> x:(+ 1 2) x) -- (-> [3] 3)