型推論入門 ― Hindley-Milnerの仕組みと実装の違い

集めた型の情報を元に型を確定する:

基本的な仕組み

制約を得

上記のアルゴリズムの違いで個性が生まれる

型推論の手法

HM 型推論

確定している型から制約を作りそれを単一化で解く

HM 実装の一つ

ML 軽減後の型推論の基礎

安全な型推論と安全かつ保守的な実装が特徴

フロー

式に対して型変数（未確定の型）を割り当てる

式の構造を再起的に辿りながら制約を割り当てる

単一化を行う

単一化

2 の項を等しくするプログラム

型を項とした方程式を解いている

型推論以外でも用いられる

HM は等しい関係性の値しか解決できない

が、拡張は可能

HM と部分型

等しい関係にない型はそのままだと推論できない

e.g. 包含型（部分型 など）

HM はそのままでは部分型を推論できない

だから TypeScript は採用していない

拡張度合い: Flix > F# > OCaml > Elm, Gleam

Flix

HM を土台にしているがほとんど別物

型クラスなどサポートするため

制約ベース型推論に近しい

F#

CLR や OOP 結合のため制約解決を含んでいている

OCaml

古典的な ML に近い

が、最近はモジュール型やオブジェクト型、多相メソッド

Elm, Gleam

忠実に実装

ただし、Elm では多相型がサポートされている

let 一般化によって実装