TL;DR
- Hindley-Milner 型推論は、確定している型から制約を作り、単一化で解く。そのままでは部分型を推論できないので、TypeScript は採用していない。
- 採用している言語でも拡張の度合いは違い、Flix > F# > OCaml > Elm, Gleam の順に元の形から離れている。
内容
型推論の基本
型推論は、すでに確定している型の情報を集め、それをもとに残りの型を確定する。基本的には、型の制約を生成し、その制約を解く。このアルゴリズムの違いで、言語ごとの個性が生まれる。
型推論の手法には、制約ベース型推論、双方向型検査、局所型推論、HM 型推論などがある。発表では HM 型推論を扱った。
HM 型推論
Hindley-Milner（HM）型推論は、ML 系の言語で多く採用されている。確定している型から制約を作り、それを単一化で解く。
Algorithm W は HM の実装の一つで、ML 系の型推論の基礎である。安全で保守的な実装が特徴である。手順は次のとおり。
- 式に型変数（未確定の型）を割り当てる。
- 式の構造を再帰的にたどりながら、制約を作る。
- 単一化する。
単一化
単一化は 2 つの項を等しくする操作で、型を項とした方程式を解いている。型推論以外でも使われる。HM は等しい関係にある型しか解決できないが、拡張はできる。
HM と部分型
等しい関係にない型、たとえば部分型のように包含関係にある型は、そのままでは推論できない。HM がそのままでは部分型を推論できないので、TypeScript は HM を採用していない。
HM を採用している言語
Flix、F#、OCaml、Elm、Gleam が HM を採用している。拡張の度合いは Flix > F# > OCaml > Elm, Gleam の順である。
- Flix: HM を土台にしているが、型クラスなどをサポートするのでほとんど別物で、制約ベース型推論に近い。
- F#: CLR やオブジェクト指向と組み合わせるので、制約の解決も含んでいる。
- OCaml: 古典的な ML に近いが、最近はモジュール型やオブジェクト型、多相メソッドもある。
- Elm、Gleam: HM に忠実に実装している。ただし、Elm は多相型をサポートしており、let 多相（let による一般化）で実装している。