1973-ML誕生#

案件摘要#

1973 年，Robin Milner 在愛丁堡大學帶領團隊開發 LCF（Logic for Computable Functions）定理證明器，而 ML（Meta Language）是它內建的「元語言」。案件的核心約束極為苛刻：定理證明器必須保證「只產生真定理」（soundness），絕不能讓使用者偽造證明。為此 Milner 設計了一種全新的語言：不寫型別卻全程型別安全、擁有史上第一個結構化例外機制。ML 因此誕生，成為整個現代型別化函數式語言家族的祖先。

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

Milner 在 Stanford 與 Edinburgh 期間研究 Dana Scott 的邏輯（LCF 即 Scott 的可計算函數邏輯），想建造互動式定理證明器。
核心問題：證明器若允許使用者任意操作「定理」物件，使用者可以偽造定理（例如直接把假命題標記為定理），整個系統的 soundness 就崩潰。
解法構想：把「定理」放在隔離花園（walled garden）裡——定理只能由公理與推論規則產生，外部語言只能「反射」呼叫這些規則，不能偽造。
但使用者需要寫戰術（tactic）腳本來自動化證明搜尋；當時的語言（Lisp、POP-2）沒有靜態型別，無法在編譯期保證型別安全。
於是需要一種新的元語言：夠快、夠互動，且型別系統能強制「定理」型別不被偽造。

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

線索一：多型型別系統#

ML 的第一個洞見是多型（polymorphism）：一個函數可以用於多種型別。Strachey 1967 年已區分兩種多型：

Parametric polymorphism（參數化多型）：同一份程式碼，行為對所有型別一致，如 length : 'a list -> int。
Ad-hoc polymorphism（特殊多型）：不同型別走不同程式碼，如 + 對整數與浮點數。

ML 選擇 parametric：map 的型別 ('a -> 'b) -> 'a list -> 'b list 對所有 'a、'b 成立，一份程式碼通吃。

線索二：Hindley-Milner 型別推論#

更驚人的是：使用者完全不用寫型別。型別由演算法 W 自動推導（詳見 1978 年那篇論文，此處先看到結果）。程式碼：

(* Standard ML：完全沒有寫任何型別標註 *)
fun map f [] = []
  | map f (x::xs) = f x :: map f xs
(* 系統自動推為 : ('a -> 'b) -> 'a list -> 'b list *)

fun length [] = 0
  | length (x::xs) = 1 + length xs
(* 自動推為 : 'a list -> int *)

線索三：let-多型#

let 綁定的變數可以被「實例化」為不同型別，但 lambda 參數不行：

let val id = fn x => x      (* id : 'a -> 'a，一般化為多型 *)
in (id 1, id true)          (* 一處當 int->int，一處當 bool->bool *)
end                         (* OK：let-polymorphism *)

(fn f => (f 1, f true)) (fn x => x)
(* 錯誤：f 是 lambda 參數，不可一般化，f 只能有一個型別 *)

這個區別保住了 soundness：lambda 參數若允許多型會導致型別系統不自洽。

線索四：例外（exception）的誕生#

ML 是第一個有結構化例外處理的語言。戰術搜尋會失敗，需要一種非局部跳脫且型別安全的機制：

exception NotFound of string;

fun lookup _ [] = raise NotFound "key missing"
  | lookup k ((k', v)::rest) =
      if k = k' then v else lookup k rest;

(* 使用：handle 捕捉例外 *)
val r = lookup "a" [("b", 2)] handle NotFound msg => 0;

例外是「帶值的非局部控制流」，比當時 Lisp 的 CATCH/THROW 更結構化、可推論。

線索五：型別健全性 -- progress + preservation#

型別系統的核心保證由兩個定理構成：

Progress：型別良好的程式不會 stuck——要么是值，要么可以再走一步。
Preservation：若 \(\Gamma \vdash e : \tau\) 且 \(e \to e'\) ，則存在 \(\Gamma'\) 使 \(\Gamma' \vdash e' : \tau\) 。

\[ \Gamma \vdash e : \tau \implies e = v \ \lor\ \exists e'.\ e \to e' \]

型別錯誤（如把整數當函數呼叫）在編譯期就被擋下，程式不會在執行期「卡死」。

線索六：隔離花園 -- 破案時刻#

LCF 的破案關鍵：ML 的型別系統把 thm（定理）做成抽象型別（abstract type），其建構函式只有公理與推論規則。使用者無法在 ML 層偽造一個 thm，因為建構途徑被型別系統封死：

(* thm 是抽象型別：使用者看不到建構子 *)
signature THEOREM =
sig
  type thm
  val ASSUME : term -> thm        (* 公理 *)
  val MP     : thm * thm -> thm   (* Modus Ponens 推論規則 *)
end
(* 沒有 mkThm : term -> thm —— 偽造途徑不存在 *)

這是「用型別系統強制邏輯健全」的經典設計，後來稱為 LCF 風格。

結案 -- 後果與影響#

ML 成為 OCaml、Standard ML、F# 的直系祖先；1990 年代 Standard ML 的定義（Milner, Tofte, Harper, MacQueen）是首個有形式語義的正式語言標準。
Hindley-Milner 型別推論進入 Swift、Kotlin、Rust、C++20 concepts、TypeScript——所有現代語言的「局部型別推論」皆為其後裔。
結構化例外處理（exception）進入幾乎所有現代語言：Java、Python、C++、OCaml。
LCF 風格（用抽象型別保證 soundness）成為定理證明器設計標準：Isabelle、Coq 的核心都遵循同一原則。
Mike Gordon 以 LCF 為基礎發展 HOL 系統；Luca Cardelli 後續在型別理論上有重大貢獻。
Milner 因 LCF、ML 與 CCS（併發理論）獲 1991 年 ACM 圖靈獎。

關鍵人物與文獻#

Gordon, M. J., Milner, R., Morris, L., Newey, M. C., Wadsworth, C. P., A Metalanguage for Interactive Proof in LCF, Proceedings of the ACM Conference on Principles of Programming Languages (POPL), 1978。
Milner, R., A Theory of Type Polymorphism in Programming, Journal of Computer and System Sciences, 17(3), 1978。
Milner, R., Tofte, M., Harper, R., MacQueen, D., The Definition of Standard ML, MIT Press, 1990（修訂版 1997）。
Paulson, L. C., Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press, 1987。
Hindley, R., The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, 146, 1969。
Strachey, C., Fundamental Concepts in Programming Languages, 1967 講義，重刊於 Higher-Order and Symbolic Computation 13(1-2), 2000。