這裡安靜了一陣子！我幾乎把所有寫作時間都花在 Logic for Programmers 上，整個腦袋都變成書的形狀了。相信我，你絕對不會想看我那篇長達兩千字、抱怨 Sphinx 建置後 LaTeX 客製化的長篇牢騷。不過過去一週我掉進了一個歷史的兔子洞，忍不住想把找到的東西分享出來。

一切是從 Algebraic [Data] Types are not Scary, Actually 這篇文章開始的。該文更詳細地介紹了 AlgDT¹，不過先快速回顧一下：

• 乘積型別像是 (Int, Bool) 或 Dog(name: str, owner: Person, age: Int 這樣的東西。它們為每一個欄位都擁有一個值。幾乎所有現代語言都有乘積型別，通常會叫做「結構（structs）」或「紀錄（records）」或「值物件（value object）」之類的名稱。

• 和型別就是「標記聯集（tagged unions）」，像是 Int + Nothing、Result + ErrorType 或 Address + Number + Email。它們代表在幾個選項中擇一。「標記」的意思是我們不會把重疊的選項合併掉。Bool + Bool 有四種可能的值，口語來說就是 Left True、Right True、Left False、Right False。和型別在現代程式語言中相對少見，除了函數式程式語言以及像 Rust 這樣的少數語言之外。

這些名稱是怎麼來的？常見的解釋是來自它們的基數（也就是可能值的數量）：如果 #T 是型別 T 的基數，那麼 #(S + T) == #S + #T 且 #(S, T) == #S * #T。如果你不太確定，可以拿 Bool + Weekday 和 (Bool, Weekday) 試試看。

但也可能是名稱來自於型別的和與積表現得就像數字的和與積一樣！我想這算是滿廣為人知的，但在 AlgDT 的入門介紹中卻很少出現。舉例來說：數字的加法具有結合律，也就是 a + (b + c) == (a + b) + c。這告訴我們 Int + (String + Null) 與 (Int + String) + Null 是同構（≅）的：我們可以在這兩種型別之間轉換值，而不會遺失任何有用的資訊。

一個更有趣的例子是，AlgDT 遵循分配律 a*(b + c) == a*b + a*c。如果我們有一個型別為 Account(name: str, contact: (Email + Phone)) 的值，就可以把它轉換成型別為 EmailAccount(name, email) + PhoneAccount(name, number) 的值。還滿巧妙的吧！

所以我開始好奇：究竟是 AlgDT 的哪一項性質讓「和」與「乘積」型別得名，又有哪些性質是後來才被發現的？隨著我繼續深入研究，這篇部落格文章就逐漸膨脹成了一篇代數資料型別的早期歷史。

尋找起源

通常要追溯術語的起源是件苦差事，但這算是廣義的學術廢話，所以所有相關的東西都可以在某篇論文裡找到。我喜歡用的兩種研究技巧是：

1. 找一篇確定有使用這些術語的論文，看它引用了什麼，再去讀那些論文，如此反覆
2. 到 ACM Digital Library 搜尋某個術語，然後從最舊的論文開始一篇篇讀下去²

通常我覺得兩種方法搭配起來效果最好。最後我一路追到了 John McCarthy（LISP 的發明者）於 1961 年發表的「A Basis for a Mathematical Theory of Computation」。就我所能找到的範圍來看，這是以任何形式討論 AlgDT 的最早文獻。

McCarthy 的論文

首先，這篇論文完全沒有使用「型別」（以資訊科學的意義而言）或「代數」這些詞，甚至嚴格來說也沒有談資訊科學。但它確實討論了「透過給定的基礎空間來定義新資料空間的方法」，而其中一種新的資料空間是「Π 由真值所構成，其僅有的元素為 T（代表真）與 F（代表假）」，也就是所謂的布林值。但他顯然對型別並不陌生，畢竟他是 ALGOL-60 委員會的成員，所以我猜他是刻意避開了「型別」這個詞。

整篇論文都在談程式函式及其性質的一個簡單數學模型。在第 2.6 節中，他定義了兩種從現有資料空間產生新資料空間的方式：

1. 兩個集合 A 與 B 的笛卡兒積 A × B，是所有有序對 (a · b) 所成的集合，其中 a ∈ A 且 b ∈ B。若 A 與 B 為有限集合，且 n(A) 與 n(B) 分別表示 A 與 B 的成員數量，則 n(A × B) = n(A) · n(B)。

毫不意外地，乘積型別的名稱來自笛卡兒積。紀錄 Dog(name: str, owner: Person, age: Int) 就是笛卡兒積 Str × Person × Int 的標記版本。在這裡我們也看到，用我們的術語來說，#(A, B) == #A * #B。

1. 集合 A 與 B 的直接聯集 A ⊕ B，是兩個互不相交的集合的聯集，其中一個與 A 呈一對一對應，另一個與 B 呈一對一對應。若 A 與 B 為有限集合，則 n(A ⊕ B) = n(A) + n(B) 即使 A 與 B 相交亦然 [強調為原文所有]。A ⊕ B 的元素可以寫成來自 A 或 B 的元素，並以下標標示其來源集合，即 a_A 或 b_B

就我所知，「直接聯集（direct union）」是 McCarthy 首創的詞，但它完全對應到不交聯集（disjoint union）。McCarthy 後來將這兩者稱為「直接和與笛卡兒積」。他並沒有將它們命名為「和與乘積型別」，但我認為它們的名稱來自對應的不交聯集與笛卡兒積這兩種集合運算是相當可信的。至於那些名稱的歷史我就不深究了，但我猜它們是類比算術中的和與積而命名的。

在定義了直接和與笛卡兒積後不久³，McCarthy 定義了資料空間之間的同構：

我們不會將集合 A × (B × C) 和 (A × B) × C 視為相同，但它們之間存在一個典範的一對一對應……我們將寫作 (A × B) × C ≅ A × (B × C) 來表達這些集合是典範同構的。

他接著展示了許多同構關係，包括我覺得非常巧妙的分配律 A × (B ⊕ C) ≅ A × B ⊕ A × C。即使當時還沒被稱為那個名字，「代數資料型別」的所有這些性質從一開始就已經被知道了。

是從那裡傳開的嗎？

在研究過程中，我找到一篇奇特的文章〈Some Observations Concerning Large Programming Efforts〉（1964 年）。作者幾乎在敏捷宣言問世的五十年前就提出了敏捷宣言的內容！卻從來沒有人引用過它，作者也沒有再發表過任何其他作品。

我想說的是，就算你是第一個想到某個點子的人，如果沒有人聽到你有這個點子，那也無濟於事。

所以，讓我們繼續追溯代數型別的發展。1964 年 McCarthy 發表了 Definition of new data types in ALGOL x⁴。他在文中提議在下一版的 ALGOL 中加入兩種新類型：「cartesian」與「union」。值得注意的是，這是我們第一次看到「標記的」代數型別，也就是和與乘積都帶有字串標籤。ALGOL-68 後來實作了這兩者，但在語言史上卻是一個奇特的死胡同；它對現代程式語言幾乎沒有產生什麼影響。

接下來的歷史就變得混亂了。在尋找後續發展時，我找到了兩篇引用 McCarthy 的重要論文：Tony Hoare 的 Notes on Data Structuring（1970 年）與 Rod Burstall 的 Proving properties of programs by structural induction（1968 年）。這兩篇分別對應到指令式語言與函數式語言的分歧，所以我會分開討論。

Hoare 的論文

Hoare 似乎是獨立想出了和與乘積型別的概念。在〈A contribution to the development of ALGOL〉（1966 年）中，他提出以「類別（classes）」來標記紀錄，並用 union 關鍵字將不相交的類別結合成一個超型別。不過他並沒有給出任何關於紀錄或聯集的代數性質。到了〈Notes on Data Structuring〉時，他的用語已經轉為與 McCarthy 一致：

我們感興趣的型別是數學家們早已熟悉的那些；也就是笛卡兒積、判別聯集、集合、函式、序列與遞迴結構。

他的「笛卡兒積」與「判別聯集」都是帶標記的，符合我們今天使用代數型別的方式。由於他主要關心的是資料儲存，他並沒有列出任何代數性質，但確實在討論如何最有效率地儲存這些型別時提到了它們的基數。

這篇論文也可能是第一次將和型別視為在編譯時期偵測錯誤的手段：

如果程式設計師試圖將一個判別聯集的值轉換回它原本並非源自的型別，這是一個嚴重的程式錯誤，可能導致無意義的結果。這個錯誤只能透過執行時期檢查來偵測，也就是每當此類轉換被明確或隱含地呼叫時，就測試其標籤欄位。這樣的檢查很耗時，而當它失敗時又極為不便。因此我們尋求一種表示法技巧，能保證這個錯誤在執行的程式中永遠不會發生；而這個保證僅需透過檢視程式文本就能給出，無需任何關於執行時期值的知識。如果有的話，這樣的保證可以由自動編譯器來提供。

就我所能找到的範圍，這也是任何人第一次將和型別稱為「判別聯集（discriminated union）」⁵。Barbara Liskov 接著用「判別聯集」來描述 CLU 的 oneof 和型別，而 Niklaus Wirth 則用「判別聯集」來解釋 Pascal 為何沒有和型別。基於這個原因，我懷疑指令式語言的世界是透過 Hoare 的這場演講才首次認識和型別，而 Hoare 本身則受到 McCarthy 的影響（但並非完全由其啟發）⁶。

在此之後，和型別就從指令式程式設計中消失了。20 世紀後期的指令式語言主要受到 Pascal 與 C 的影響。Pascal 沒有和型別，是因為 Wirth 認為它們不如無標記聯集來得彈性。C 很可能沒有和型別，則是因為它沿用了 IBM PL/I 的型別系統。PL/I 於 1964 年首次發表，擁有乘積型別（他們稱之為 structs），但只有無標記聯集。較新的指令式語言反而是從函數式程式設計的世界重新獲得和型別，這就又把我們帶回了 「Proving properties of programs by structural induction」。

Burstall 的論文

Burstall 是個讓人非常難以研究的對象。他的訃聞列出了數量驚人的論文與具影響力的學生，顯然他在函數式程式設計的早期發展中扮演了舉足輕重的角色。但那些論文中非常少數能在線上找到，所以我能輕易研究的範圍有很大的缺口。以下是我盡力拼湊出他那部分歷史的成果。

這篇論文談的是證明遞迴型別（如串列與樹）的性質。他是這樣定義串列的：

我建議每個建構子運算都引入一個新類別，而這些型別的析取也應該是型別（大致依循 Landin 1964）

一個 cons 擁有一個原子與一個串列，一個 nil 沒有任何組成，一個 list 是一個 cons 或一個 nil。

Burstall 說他的表示法來自 P. J. Landin 的〈The Mechanical Evaluation of Expressions〉（1964 年）。Landin 的用法似乎還不完全是和型別——目前還不清楚他是否有機制能在型別值重疊時加以區分。相反地，在我看來，Burstall 只是「依循」了 Landin 撰寫遞迴定義的方式。雖然我反覆讀了幾次，還是很難確定，也很可能是我搞錯了。

不過 Burstall 確實有和型別，這可以從他對樹的定義看出來。一棵樹是「一個節點（node）或一個葉尖（tip）或一棵空樹（niltree）」，但一個 tip 是「擁有一個項目（item）」，而不是就是一個項目。而後來，他寫了這樣的虛擬碼：

cases t:
    niltree(): nil()
    tip(i): i::nil()
    node(t1, i1, i2): concat(flatten(t1), flatten(t2))

Burstall 也說他的想法「基於 John McCarthy 的工作」，並引用了他的數學理論論文。Burstall 受到 McCarthy 的直接聯集概念啟發，也並非不可能。

截至 2025 年，這篇論文已被引用超過 500 次。Burstall 後來還會做出更大的貢獻，但那是 1980 年的事了，所以我們得先談談 ML。

Milner 的論文

到目前為止，我們已經看過代數資料型別的定義以及「笛卡兒積」的常見用法，但還沒看到「和型別」與「乘積型別」這些術語。就我所能找到的範圍，這些名稱來自 Robin Milner 的 ML，如他在〈A Theory of Type Polymorphism in Programming〉（1977 年）中所宣傳的：

ML 中完全確定的型別（即單型（monotypes））是由一組基本型別（int、bool 等）透過二元中綴運算子 x（笛卡兒積）、+（不交和）與 ->（函式型別），以及一元後綴運算子 list 所建構而成。

關於這篇論文，有幾點值得注意。首先，當然是它描述了以「不交和」來建構型別，並使用了 + 這個符號。其次，與 Hoare 和 McCarthy 不同，它既沒有為「不交和」提供理據，也沒有定義它。到了這個時候，對 Milner 的讀者而言，這或許已經是常識了。最後，該論文聲稱和與積在 ML 中至少已經實作兩年了。

我們沒有最早期 ML 版本的完整規格，但我們有 ML 所為之設計的 LCF 證明器已釋出的原始碼。這是在 files.ml 中的片段：

let instintype insttylist ty = inst ty whererec inst ty =
    fst(revassoc ty insttylist)
    ?(failwith phylumoftype ty
   ??``consttype vartype`` ty
   ??``funtype`` mkfuntype((inst # inst)(destfuntype ty))
   ??``sumtype`` mksumtype((inst # inst)(destsumtype ty))
   ??``prodtype`` mkprodtype((inst # inst)(destprodtype ty))
     )  ;;

看吧：就是「和」與「乘積」型別！不過這些還不是帶標記的。Li-yao Xia 在文章 Where does the name “algebraic data type” come from? 中指出「早期版本並沒有資料型別（見第一版 Edinburgh LCF）」，我理解他的意思是指帶標記的代數型別；ML 有 abstype 關鍵字來為建構出的型別命名。你可以把 EmailOrAddress 定義為 Str + Str，但無法將左邊的 Str 稱為「email」。

〈A Theory of Type Polymorphism〉並沒有引用 McCarthy 的論文，也沒有引用 Hoare 或 Burstall 的論文，所以不清楚 Milner 是受到他們的影響，還是獨立發展出 AlgDT。一些初步的證據來自後續論文〈A Metalanguage for Interactive Proof in LCF〉（1978 年），他在其中感謝了三人的貢獻：

我們感謝 Dana Scott 為我們的工作提供了很大一部分理論基礎：感謝 John McCarthy 鼓勵了本計畫在史丹佛的前身：感謝 Richard Weyhrauch 對該計畫的巨大貢獻：感謝 Tony Hoare 與 Jerry Schwarz 在 ML 抽象型別概念上的協助：感謝 Avra Cohn 在最後設計階段透過她的實驗所提供的幫助：感謝 Rod Burstall 與愛丁堡的許多同事帶來啟發性的討論。

好了，還剩下三個語言要談。

Hope、VAX ML 與 Miranda

大約在這個時候，Burstall 正在將範疇論應用於軟體規格，最終促成了 HOPE 的誕生。〈HOPE: An experimental applicative language〉（1980 年）標誌著標記聯集首次被引入函數式程式設計，但沒有引入標記乘積：

要定義一個「數字樹」型別，我們可以這樣寫

data numtree == empty ++ tip(num) ++ node(numtree#numtree)

（符號 # 表示型別的笛卡兒積。）

除此之外，這篇論文還引入了幾個重要的概念。第一個是編譯器可以針對和型別中所有不相交的選項進行窮盡性檢查：

每種資料型別都將擁有一組互不相交的子型別，每個子型別都有不同的建構子函式；例如，串列是由 cons 或 nil 所構成。針對這些建構子進行個案分析應該很容易，且編譯器也很容易檢查該分析是否窮盡。這可以避免像是忘記加入對空串列測試的錯誤。

除此之外，該論文還提出，透過模式匹配可以大幅簡化對和型別的使用。這並非語言中結構化模式匹配的首次出現（Prolog 才是最早的），但卻是模式匹配在函數式程式設計中的首次出現。

大約與 HOPE 同一時期，Burstall 的徒孫 Luca Cardelli⁷ 正在將 ML 移植到 VAX 與 Unix，並在過程中加入了紀錄與變體型別。就我所能找到的範圍，這是標記的和與標記的乘積首次同時出現在函數式程式語言中。

所有這些想法後來都被納入了 Standard ML，奠定了人們今天所認為的代數型別核心特性：標記、基於編譯器的窮盡性檢查，以及模式匹配。

最後，再次引用 Xia 的文章，〈Miranda: A non-strict functional language with polymorphic types〉（1985 年）是第一篇實際使用「Algebraic Data Type」這個術語的論文。我強烈建議閱讀 Xia 的文章以獲得更多資訊。

一個非常不穩固的總結

• McCarthy 在他的論文中首次提出了代數資料型別的概念與性質，儘管他並沒有那樣稱呼它。
• 這至少對 Tony Hoare 與 Rod Burstall 產生了一些影響，他們各自寫出了具影響力的論文。
• AlgDT 在 ALGOL-68、CLU 與 ML 中被實作。Milner 是否知道 McCarthy 的理論目前還不清楚，但我傾向認為他知道的可能性比較大。
• Pascal 與 C 使得和型別無法在指令式程式設計中站穩腳步。
• Burstall 與 Luca Cardelli 補齊了 AlgDT 的主要特性，使其成為型別化函數式程式設計的基石。

這已經是我在有限時間與資源下所能做到的最好成果了。如果你發現任何錯誤，請告訴我！

如果你喜歡這篇文章，歡迎加入我的電子報！我每週都會在那裡發表新的文章。

我為企業提供形式化方法的培訓，讓軟體開發更快、更便宜、更安全。歡迎在這裡了解更多。