跳轉到

1975-Hope 語言與模式匹配#

案件摘要#

1975 年，愛丁堡大學的 Rod Burstall、David MacQueen 與 Donald Sannella 創造了 Hope——程式語言史上第一個同時擁有代數資料型別（algebraic data types）與模式匹配（pattern matching）的語言。Hope 的誕生不是為了寫商業軟體，而是為了一場更深的陰謀：Burstall 與 Darlington 的程式變換研究（transformation program development）需要一門「可代數推理」的語言——資料必須由建構子定義，讓方程式改寫有根基可循。LISP 只有 list 沒有型別，樹狀結構全靠約定俗成；Hope 用 data Tree a = Leaf a | Node (Tree a) (Tree a) 一行宣告，讓「資料是什麼」首次成為語言的一部分。本案追查：代數資料型別背後的初始代數（initial algebra）理論、模式匹配的語義，以及 Hope 如何成為 ML、Miranda、Haskell、Rust、Swift 的共同祖先。

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

  • Burstall-Darlington 的程式變換研究（1975-77，"A Transformation System for Developing Recursive Programs"）需要對程式做「代數運算」：展開、摺疊、定律改寫——但 LISP 程式無法可靠地做這些推理，因為資料沒有型別、結構沒有保證。
  • LISP（1958/1960）只有 list 一種複合資料：樹要用巢狀 list 模擬，car/cdr 取錯一格就是災難，編譯器無從檢查。
  • 1960-70 年代，Burstall 已在程式證明領域深耕（"Proving Properties of Programs by Structural Induction", 1969），需要一門「資料結構直接對應歸納證明」的語言。
  • 愛丁堡學派的 ML（1974，Milner 的 LCF 定理證明器輔助語言）已有型別推論，但資料型別尚未成形。
  • Burstall 想用「建構子」（constructor）表達樹狀資料：每種資料就是幾個建構子的選集，程式的每個分支對應一個建構子——資料與程式互為鏡像。
  • 理論背景：抽象代數的 initial algebra 概念已成熟（Birkhoff 1935），「資料型別 = 初始代數」的等式語義（ADJ 小組，1970s）正在成形——Hope 是這個理論的第一個語言實現。

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

線索一：代數資料型別 = 初始代數#

Hope 的資料宣告：

data tree(a) = leaf(a) ++ node(tree(a), tree(a))

數學上，這定義了一個初始代數（initial algebra）：給定簽名（signature） \(\Sigma\) ，含建構子 \(leaf : A \to Tree(A)\) 與 \(node : Tree(A) \times Tree(A) \to Tree(A)\) ， \(Tree(A)\) 是所有由這兩個建構子有限次生成的項（term）之集合：

\[ Tree(A) = \bigcup_{n \ge 0} T_n, \quad T_0 = A, \quad T_{n+1} = A + T_n \times T_n \]

這正是最小不動點（least fixed point）：

\[ T = \mu F, \quad F(X) = A + X \times X \]

「初始」的意義在萬有性質（universal property）：對任何其他代數 \(B\) （即任何滿足同樣建構子簽名的集合），存在唯一的多態映射（catamorphism，即 fold） \(h : Tree(A) \to B\) ：

\[ h(leaf(a)) = f(a), \qquad h(node(l, r)) = g(h(l), h(r)) \]

這就是為什麼樹的求和、求深、求值都只要一個遞迴函數——初始代數保證了唯一性。datatype 宣告中的 tree 出現在自身定義右側，正是「遞迴資料型別」：型別的定義本身就是不動點方程。

線索二：模式匹配的語義——case analysis#

模式匹配的語義是第一個匹配者生效的子句分析（case analysis）。函數由多個子句定義：

dec sum : tree(num) -> num;
--- sum(leaf(n)) <= n;
--- sum(node(l, r)) <= sum(l) + sum(r);

語義上，這是對建構子的 case split：輸入若是 leaf(n)（即 \(leaf(a)\) 形態），套第一子句；若是 node(l, r)，套第二子句。數學寫法：

\[ sum(t) = \begin{cases} n & \text{if } t = leaf(n) \\ sum(l) + sum(r) & \text{if } t = node(l, r) \end{cases} \]

因為初始代數保證每個項恰好是某個建構子的應用（exhaustiveness），模式匹配可以窮盡所有情況——編譯器甚至能自動檢查子句是否漏掉建構子。這是「由建構子定義資料」的對偶紅利：資料的定義直接編譯成程式分支的完備性檢查。

線索三：Burstall 的結構歸納與程式證明#

Burstall 1969 年的結構歸納（structural induction，Bird 稱之為 inductionless induction 的基礎）：要證明性質 \(P(t)\) 對所有樹成立，只需證明：

\[ \forall a.\, P(leaf(a)) \;\wedge\; \big(\forall l, r.\, P(l) \wedge P(r) \Rightarrow P(node(l, r))\big) \]

這與模式匹配的子句一一對應：每個子句就是一個歸納步。Burstall-Darlington 的變換系統正是在這個框架上做「展開-摺疊」：sum(leaf(n)) 展開為 n（unfolding），累積的表達式摺回 sum（folding）。有了 ADT 與模式匹配，這些變換每一步都機器可驗證。

線索四：多型 ADT#

Hope 的 data tree(a) 帶型別參數 \(a\) ：tree(num)、tree(bool) 都是合法型別。多型是初始代數構造的參數化—— \(F(X) = A + X \times X\) 對任意 \(A\) 都成立。這讓 Hope 領先了時代：Haskell 的 data、ML 的 datatype、Rust 的 enum 都直接繼承這個設計。

程式示範：Haskell（Hope 的後裔）示範 ADT 與模式匹配#

{-# LANGUAGE LambdaCase #-}

-- Hope 的 tree(a) 直接翻譯成 Haskell 的 data
data Tree a = Leaf a | Node (Tree a) (Tree a) deriving (Show, Eq)

-- 模式匹配：每個子句對應一個建構子（case analysis）
sumTree :: Num a => Tree a -> a
sumTree (Leaf n)     = n
sumTree (Node l r)   = sumTree l + sumTree r

depth :: Tree a -> Int
depth (Leaf _)       = 1
depth (Node l r)     = 1 + max (depth l) (depth r)

-- 初始代數的萬有性質：foldr 保證唯一映射
foldTree :: (a -> b) -> (b -> b -> b) -> Tree a -> b
foldTree f _ (Leaf x)   = f x
foldTree f g (Node l r) = g (foldTree f g l) (foldTree f g r)

sumByFold :: Tree Int -> Int
sumByFold = foldTree id (+)

main :: IO ()
main = do
  let t = Node (Leaf 1) (Node (Leaf 2) (Leaf 3))
  print (sumTree t)    -- 6
  print (depth t)      -- 3
  print (sumByFold t)  -- 6 ：fold 與直接遞迴給出同樣結果（萬有性質）

sumTree 與 sumByFold 結果相同——這正是初始代數萬有性質的可執行證明：任何滿足建構子簽名的映射都唯一。

破案時刻#

Hope 的論文（Burstall-MacQueen-Sannella，"Hope: An Experimental Applicative Language"）首次把 data 宣告與模式匹配並列為語言核心：資料由建構子定義、程式由建構子分支組成、兩者由初始代數的萬有性質鎖死。資料與程式的鏡像就此成為靜態型別函數式語言的標準配備——變形蟲被標本化，這次是資料的形狀。

結案 -- 後果與影響#

  • ADT + pattern matching 進入 Standard ML（Milner 1984 的 datatype）、Miranda（Turner 1985）、Haskell（1990）、F#、Rust 的 enum 與 match、Swift 的 enum 與 switch——成為靜態型別語言的標準配備。
  • Hope 的建構子語法 ::（list cons）直接影響 Haskell 的 : 與語法風格；Hope 的 dec ... <= ... 函數定義演變成 Haskell 的 f x = ... 與守衛。
  • Burstall-Darlington 的變換系統（unfold/fold）成為程式變換與程式合成研究的理論基礎，影響至今的 supercompilation 與 foldr/build 優化。
  • 初始代數語義（catamorphism/fold）成為 Haskell 的 Foldable、recursion-schemes 庫的理論核心。
  • 模式匹配的編譯器完備性檢查成為 Rust/Swift 的安全賣點之一：漏掉的建構子編譯期就報錯。
  • 愛丁堡學派的 Hope-ML 譜系直接催生 Haskell——Hope 是 Haskell 的「失落的祖先」，其名字僅存於歷史，其思想統治了世界。

關鍵人物與文獻#

  • Rod Burstall, David MacQueen & Donald Sannella, "Hope: An Experimental Applicative Language", University of Edinburgh, Dept. of AI, Research Report; 正式發表於 Proceedings of the 1980 ACM Conference on LISP and Functional Programming, 1980, pp. 136–143.
  • Rod Burstall, "Proving Properties of Programs by Structural Induction", The Computer Journal 12(1), 1969, pp. 41–48.
  • Rod Burstall & John Darlington, "A Transformation System for Developing Recursive Programs", Journal of the ACM 24(1), 1977, pp. 44–67.
  • Rod Burstall, David MacQueen & Donald Sannella, "HOPE: An Experimental Applicative Language"（早期版本）, Edinburgh DAI Research Memo 62, 1976.
  • J. A. Goguen, J. W. Thatcher, E. G. Wagner & J. B. Wright（ADJ 小組）, "Initial Algebra Semantics and Continuous Algebras", Journal of the ACM 24(1), 1977, pp. 68–95.
  • Robin Milner, "A Theory of Type Polymorphism in Programming", Journal of Computer and System Sciences 17(3), 1978, pp. 348–375（ML 型別推論，Hope 的同門基礎）.
  • David A. Turner, "Miranda: A Non-Strict Functional Language with Polymorphic Types", Proceedings of IFIP FPCA 1985, LNCS 201, Springer, pp. 1–16.