跳轉到

1973 ML 型別推導誕生：Milner 與演算法 W 的魔法#

案發現場#

1970 年代初，愛丁堡大學的 Robin Milner 正在開發 LCF（Logic for Computable Functions）——一個交互式定理證明器。LCF 面臨一個兩難：使用者輸入的數學式子必須經過型別檢查，確保「證明步驟」不會產生偽證（例如把 \(1+1\) 誤當成 \(true+false\) ）。但型別檢查要求使用者到處寫型別註記，這在交互式環境中令人窒息。

未解之謎是：能不能讓語言自動推導出所有運算式的型別，使用者一個型別都不用寫，卻仍然擁有完整的靜態型別安全？

當時學界的悲觀論調是：如果缺少型別註記，型別系統就無法判定（type inference 是不可判定的）。1969 年 J. Roger Hindley 在邏輯文獻中其實已證明：對於簡單型別 λ 演算的組合子版本，主型別（principal type）推導是可判定的。但沒有人把它用在真正的程式語言上。Milner 在 1973 年為 ML 實作了推導演算法，並在 1978 年的論文中形式化為演算法 W，加上參數多型（parametric polymorphism），成就了程式語言史上最優雅的型別系統。

偵查過程#

Milner 的核心靈感來自兩個來源：Hindley 的邏輯推導演算法，與 Curry-Howard 對應——型別就是命題，程式就是證明。他的推導分三步：

第一步：基本推導規則。 型別環境 \(\Gamma\) 下，推導是語法導向的：

\[ \frac{\Gamma(x) = \tau}{\Gamma \vdash x : \tau} \quad \frac{\Gamma \vdash e_1 : \tau' \to \tau \quad \Gamma \vdash e_2 : \tau'}{\Gamma \vdash e_1\ e_2 : \tau} \]

應用規則中出現了「約束」： \(e_1\) 的參數型別 \(\tau'\) 必須與 \(e_2\) 的型別相等。演算法用替換（substitution，記為 \(\sigma = \{\alpha \mapsto int\}\) ）來解這些約束。

第二步：逐步推導 id : α → α。 考慮 fun x -> x（ML 語法）：

  1. 為 \(x\) 生成新鮮型別變數 \(\alpha_1\) ，環境為 \(\{x : \alpha_1\}\) 。
  2. 函數體 \(x\) 推導出型別 \(\alpha_1\) 。
  3. 函數整體型別為 \(\alpha_1 \to \alpha_1\) 。
  4. 函數定義結束時，對 \(\alpha_1\) 進行泛化（generalization）： \(\alpha_1\) 是區域變數、未被外部約束，故升格為全稱量詞變數，得到：
\[ \forall \alpha.\ \alpha \to \alpha \]

這就是 id 函數的主型別——它對所有型別一體適用。當呼叫 id 5 時，實例化為 \(\alpha \mapsto int\) ，得到 \(int \to int\) 。

第三步：演算法 W。 完整演算法由三個操作構成：

  • Var：查環境，泛化後回傳。
  • App：推導函數與參數，合一 \(fn : \alpha \to \beta\) 與 \(arg : \tau\) ，回傳 \(\beta\) 。
  • Abs：為參數生成新鮮變數，推導函數體，回傳箭頭型別。

演算法 W 的性質是完備且健全（sound and complete）：若存在主型別，W 必能找到；W 找到的型別必是最一般的。

第四步：代數資料型別。 ML 還引入了可定義的遞迴資料型別：

datatype tree = Leaf | Node of tree * int * tree

型別推導與代數資料型別結合，使 ML 能在「零註記」下處理任意複雜的資料結構。這個組合直接成為 OCaml、Standard ML、F#、Haskell 的核心。

結案報告#

ML 型別推導的遺產：

  • 語言系譜：Standard ML（1983）、OCaml、F# 直承 ML 血統；Haskell（1990-Haskell.md）採用 Hindley-Milner 為基礎；Rust 的型別推導與所有權系統、Swift 的型別推導，都是這條血脈的後裔。
  • 理論影響：Curry-Howard 對應從此成為程式語言理論的核心，型別系統研究（子型別、型別類、依值型別）皆以 ML 為起點。
  • 工業實踐：現代語言（TypeScript、Scala、Kotlin、Go 的部分推導）都提供某種程度的型別推導。「靜態型別但不用寫型別」已成為主流體驗。
  • 工具鏈：IDE 的型別顯示、重構工具、形式化驗證（Coq、Agda）都建立在 Milner 的基礎上。

Milner 於 1991 年獲得圖靈獎。ML 證明：型別安全與程式簡潔不必二選一——只要推導演算法夠聰明。

證據與工具#

OCaml 示範——零註記的型別推導：

let id x = x                    (* id : 'a -> 'a *)
let compose f g x = f (g x)     (* compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b *)

type tree = Leaf | Node of tree * int * tree

let rec sum = function
  | Leaf -> 0
  | Node (l, v, r) -> sum l + v + sum r   (* sum : tree -> int *)

let _ = id 5          (* int *)
let _ = id "hello"    (* string *)

用 Python 模擬 Hindley-Milner 演算法 W：

import itertools

class TyVar:
    _ids = itertools.count()
    def __init__(self): self.id = next(TyVar._ids)
    def __repr__(self): return f"t{self.id}"

class TyArrow:
    def __init__(self, a, b): self.a, self.b = a, b
    def __repr__(self): return f"({self.a} -> {self.b})"

def occurs(v, t):
    if isinstance(t, TyVar): return v is t
    if isinstance(t, TyArrow): return occurs(v, t.a) or occurs(v, t.b)
    return False

def subst(t, s):
    if isinstance(t, TyVar): return s.get(t, t)
    if isinstance(t, TyArrow):
        return TyArrow(subst(t.a, s), subst(t.b, s))
    return t

def unify(a, b, s):
    a, b = subst(a, s), subst(b, s)
    if isinstance(a, TyVar) and not occurs(a, b): s[a] = b
    elif isinstance(b, TyVar) and not occurs(b, a): s[b] = a
    elif isinstance(a, TyArrow) and isinstance(b, TyArrow):
        unify(a.a, b.a, s); unify(a.b, b.b, s)
    elif a != b: raise TypeError(f"cannot unify {a} with {b}")

def infer(env, e, s):
    if isinstance(e, str):                          # 變數
        return subst(env[e], s)
    if isinstance(e, tuple) and e[0] == "abs":      # fun x -> body
        v = TyVar(); env = dict(env); env[e[1]] = v
        body = infer(env, e[2], s)
        return TyArrow(subst(v, s), body)
    if isinstance(e, tuple) and e[0] == "app":      # f x
        tf = infer(env, e[1], s); tx = infer(env, e[2], s)
        res = TyVar()
        unify(tf, TyArrow(tx, res), s)
        return res

# 推導 id = fun x -> x
s = {}
t = infer({}, ("abs", "x", "x"), s)
print(t)   # (t0 -> t0)，即 ∀α. α -> α