19. 1973 — Robin Milner 的 ML 語言#

案件摘要#

1973 年，Robin Milner 在愛丁堡大學開發 LCF 定理證明器（Logic for Computable Functions）時，發明了 ML（Meta Language）作為其中繼語言。ML 是史上第一門具有型別推論的主流語言：程式設計師不需寫型別註解，編譯器自動推導出最一般的型別。Hindley–Milner 型別系統自此成為函數式程式設計的標準配置。

前因 -- 為什麼會有這個案子#

線索來自理論與實務的交會：

LCF 的需求：Milner 在史丹佛跟隨 Dana Scott 研究 LCF（可計算函數邏輯），回到愛丁堡後要實作定理證明器。證明器中的「策略（tactics）」需要高階函數、遞迴、以及可靠性的保證——證明步驟不能出錯；
型別即保證：Milner 的推理是——若每個策略都有明確的型別，且型別錯誤在編譯期就被抓到，那麼證明的正確性就有了第一道防線；
但手寫型別太累：若要求使用者為每個函數寫型別註解，策略的組合會變得繁瑣。Milner 需要一個「自動推導型別」的演算法；
Hindley 的先聲：Roger Hindley 在 1969 年已經為組合子邏輯提出了一個型別推論演算法；Milner 獨立地為程式語言重新發現了它。

線索與推理 -- 數學式、程式、理論#

1. Hindley–Milner 型別系統#

HM 型別的語法：

\[ \tau ::= \alpha \mid \tau_1 \to \tau_2 \mid \mathbb{Int} \mid \mathbb{Bool} \mid \cdots \qquad \sigma ::= \tau \mid \forall \alpha_1 \cdots \alpha_n.\, \tau \]

其中 \(\tau\) 是單型（monotype）， \(\sigma\) 是型別方案（type scheme）。關鍵限制：全稱量化只允許在 let 邊界上（let-polymorphism），不在 λ 參數上——這使型別推論可判定。

2. let 多型（let-polymorphism）#

(* let 綁定的函數獲得多型 *)
let id x = x
(* id : 'a -> 'a  （多型！） *)

(* id 可以用於不同型別 *)
let _ = id 1          (* int *)
let _ = id "hello"    (* string *)
let _ = id [1;2]      (* int list *)

對比：λ 參數不獲得多型：

(fun id -> (id 1, id "hello")) (fun x = x)
(* 錯誤：id 被推論為 int -> int，第二個呼叫型別不合 *)

數學上：(fun id -> ...) (fun x. x) 中 id 是 λ 參數，只能有單型；而 let id = ... in ... 中 id 每次使用可以「重新實例化」 \(\forall \alpha.\, \alpha \to \alpha\) 。

3. Algorithm W 概述#

Algorithm W（Milner, 1978）是型別推論的核心演算法。輸入環境 \(\Gamma\) 與表達式 \(e\) ，輸出型別 \(\tau\) 與替換（substitution） \(S\) ：

\[ W(\Gamma, e) = (S, \tau) \]

三個基本操作：

實例化（instantiation）：使用型別方案 \(\forall \alpha.\, \tau\) 時，把所有 \(\alpha\) 換成新的型別變數；
統一（unification）： \(S = \text{unify}(\tau_1, \tau_2)\) 找出最一般替換使 \(S\tau_1 = S\tau_2\) ；
泛化（generalization）：let 邊界上，把未被環境約束的型別變數量化。

推導規則概要：

\[ \frac{}{W(\Gamma, x) = (\text{id}, \text{inst}(\Gamma(x)))} \qquad \frac{W(\Gamma, e_1) = (S_1, \tau_1) \quad W(S_1\Gamma, e_2) = (S_2, \tau_2)} {W(\Gamma, e_1\ e_2) = (S_2 \circ S_1,\ S_2(\tau_1)) \text{ 配上 } \text{unify}(S_2\tau_1, \tau_2)} \]

定理（Milner, 1978）：Algorithm W 是完備且健全的——若 \(e\) 有型別， \(W\) 一定能找到最一般的型別（principal type）；且推論出的型別保證型別安全。

4. 一個型別推論小範例#

Haskell/OCaml 中，推論逐步進行：

(* OCaml *)
let compose f g x = f (g x)
(* 推論過程：
   g  : 'a -> 'b     （g x 的型別為 'b，x 為 'a）
   f  : 'b -> 'c     （f (g x) 的型別為 'c）
   compose : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c
   即 compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b  （重命名後） *)

-- Haskell
map :: (a -> b) -> [a] -> [b]
-- 推論：f : a -> b, xs : [a]（因為 map 的第一個參數作用於列表元素）
-- 最一般型別：(a -> b) -> [a] -> [b]

5. 代數資料型別與模式匹配#

ML 引入代數資料型別（Algebraic Data Type, ADT）——這是 Curry–Howard 對應中和型/乘積型的直接體現：

(* OCaml：代數資料型別 = 和型 + 乘積型 *)
type shape =
  | Circle of float            -- 圓（單一乘積：半徑）
  | Rect of float * float      -- 矩形（乘積：寬×高）
  | Triangle of float * float * float  -- 三角（乘積：三邊）

(* 模式匹配 = 和型的消去規則 *)
let area s = match s with
  | Circle r         -> 3.14159 *. r *. r
  | Rect (w, h)      -> w *. h
  | Triangle (a,b,c) -> (* Heron's formula *) ...

模式匹配的完備性檢查（是否涵蓋所有建構子）由編譯器自動執行——這是 Curry–Howard 對應下「消去規則必須完整」的工程實現。

6. 垃圾回收#

ML 是第一門內建垃圾回收（GC）的靜態型別語言。Milner 的推理：定理證明器需要管理大量「證明樹」物件，手動記憶體管理既危險又繁瑣；配合靜態型別與不可變資料結構，GC 可以高效執行。這條線索延續到 OCaml、Java、C#、Haskell——「靜態型別 + GC」成為現代語言的標準配置。

7. ML 的譜系#

ML (1973, Edinburgh)
 ├── Standard ML (1983-1997)：Milner, Tofte, Harper, MacQueen
 │     └── SML/NJ, MLton, Poly/ML
 └── Caml (1987, INRIA)
       └── Caml Light (1990)
             └── OCaml (1996)
                   ├── F# (2005, Microsoft)
                   └── ReasonML, Melange

結案 -- 後果與影響#

Hindley–Milner 型別系統成為標準：OCaml、Haskell、F#、Elm、Rust（早期）、Swift 的型別推論都源自 HM；
型別推論的理論：Milner 的 Algorithm W 開創了「型別推論演算法」的研究，統一（unification）、主型別（principal type）成為標準工具；
代數資料型別與模式匹配：成為所有現代函數式語言的標配，甚至影響 Rust 的 enum/match 與 Swift 的 enum；
定理證明的工程化：LCF 開創了「策略（tactic）」傳統，其後繼者 Isabelle、Coq 都繼承了 LCF 的架構；Milner 因 LCF 與 ML 獲 1991 年圖靈獎；
「靜態型別 + GC + 高階函數」的組合被證明可行且實用，為 Java/C#/Haskell 等現代語言鋪路。

關鍵人物與文獻#

Robin Milner（1934–2010）：英國計算機科學家，愛丁堡/劍橋教授，1991 年圖靈獎得主；後又發明 π 演算（π-calculus, 1992）。
Roger Hindley：邏輯學家，1969 年提出組合子邏輯的型別推論演算法。
Luis Damas：Milner 的學生，1982 年博士論文證明了 HM 系統的健全性（Damas–Milner 定理）。
R. Milner, "A Theory of Type Polymorphism in Programming" (1978, JCSS)。
R. Milner, M. Tofte, R. Harper, The Definition of Standard ML (1990)。
L. Damas & R. Milner, "Principal Type-Schemes for Functional Programs" (1982, POPL)。