しばらく静かにしていました！執筆時間のほとんどをLogic for Programmersに注ぎ込んでいて、頭の中はすっかり本の形になっています。正直、Sphinxのビルド後LaTeXカスタマイズについて2000語も愚痴った文章なんて読みたくないでしょう。でも、この一週間は歴史の沼にハマってしまい、見つけたことをどうしても共有したくなりました。

きっかけはAlgebraic [Data] Types are not Scary, Actuallyという記事でした。この記事ではAlgDT¹についてより詳しく解説されていますが、簡単におさらいすると次のとおりです：

• 直積型は(Int, Bool)やDog(name: str, owner: Person, age: Intのようなものです。各フィールドに対応する値を持ちます。現代の言語のほとんどは直積型を備えており、たいてい「struct」や「record」「value object」などと呼ばれています。

• 直和型は「タグ付き共用体」で、Int + NothingやResult + ErrorType、Address + Number + Emailのようなものです。いくつかの選択肢の中から一つを選ぶ型です。「タグ」があることで、重なる選択肢が消えることはありません。Bool + Boolは4つの値を取り得ます。俗な言い方をすれば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で用語を検索し、最も古いものから順にすべての論文を読む²

たいていはこの二つを組み合わせるのが一番うまくいきます。そうやってたどり着いたのが、ジョン・マッカーシー（LISPの発明者）による1961年発表の“A Basis for a Mathematical Theory of Computation”でした。私の知る限り、これがあらゆる形でのAlgDTに関する最初の論考です。

マッカーシーの論文

まず、この論文では（計算機科学の意味での）「型」や「代数」という言葉はまったく使われておらず、そもそも計算機科学を扱ったものでもありません。しかし「与えられた基本空間から新しいデータ空間を定義する方法」について論じており、その新しいデータ空間の一つが「要素がT（真）とF（偽）のみからなる真理値のΠ」すなわちブール値です。ただ、彼はALGOL-60委員会のメンバーだったので型の概念には確実に精通しており、ここで意図的に「型」という言葉を避けたのだろうと推測しています。

論文全体は、プログラムの関数とその性質についての単純な数学的モデルを扱っています。2.6節で彼は、既存のデータ空間から新しいデータ空間を生成する二つの方法を定義しています：

1. 二つの集合AとBのデカルト積A × Bは、a ∈ Aかつb ∈ Bであるすべての順序対(a · 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と1対1対応し、他方がBと1対1対応する、互いに交わらない二つの集合の和集合である。AとBが有限なら、AとBが交わっていても [強調は筆者] n(A ⊕ B) = n(A) + n(B)である。A ⊕ Bの要素は、由来する集合を添字として付けたAまたはBの要素として、すなわちa_Aまたはb_Bと書くことができる

私の知る限り、「direct union（直和）」という言葉はマッカーシーの造語ですが、これは非交和（disjoint union）と正確に対応します。マッカーシーは後にこの二つを「direct sumとCartesian product」と呼んでいます。彼はそれらを「sum型やproduct型」と名付けたわけではありませんが、対応する非交和やデカルト積という集合演算にちなんで名付けられたと考えるのは十分あり得るでしょう。それらの名前の歴史まで深掘りするつもりはありませんが、おそらく算術の和や積からの類推で名付けられたのだろうと思います。

直和とデカルト積を定義した直後³、マッカーシーはデータ空間間の同型を定義します：

集合A × (B × C) and (A × B) × Cを同じものとはみなさないが、それらの間には標準的な1対1写像が存在する……これらの集合が標準的に同型であるという事実を表すために(A × B) × C ≅ A × (B × C)と書くことにする

彼はさらに、先ほど私が素敵だと感じた分配則A × (B ⊕ C) ≅ A × B ⊕ A × Cを含む、数多くの同型を示しています。「代数的データ型」のこうした性質は、当時はまだそう呼ばれていなかったものの、最初からすべて知られていたのです。

そこから広まったのだろうか？

この件を調べているときに、“Some Observations Concerning Large Programming Efforts”（1964年）という奇妙な記事を見つけました。著者はアジャイル宣言のほぼ50年前にアジャイル宣言のような内容を提示していたのです！誰にも引用されず、著者は他に何も発表していません。

言いたいのは、誰もあなたの考えを聞いてくれなければ、最初に思いついたかどうかは関係ないということです。

というわけで、代数的データ型の発展をさらに追ってみましょう。1964年、マッカーシーはDefinition of new data types in ALGOL xを発表しました⁴。この中で彼は、次期ALGOLに「cartesian」と「union」という二つの新しい型を追加することを提案しています。注目すべきは、ここで初めて和と積の両方に文字列タグが付く「タグ付き」代数的データ型が登場することです。ALGOL 68は後にその両方を実装しますが、言語史の中では奇妙な行き止まりとなり、現代のプログラミング言語にはほとんど影響を与えませんでした。

ここから歴史はややこしくなります。次の展開を探す中で、マッカーシーを引用している影響力の大きい二つの論文を見つけました。トニー・ホーアのNotes on Data Structuring（1970年）と、ロッド・バーストールのProving properties of programs by structural induction（1968年）です。これらは命令型言語と関数型言語の分岐に対応しているので、別々の節で扱うことにします。

ホーアの論文

ホーアは和型と積型のアイデアを独自に思いついたようです。“A contribution to the development of ALGOL”（1966年）では、「class」でタグ付けされたレコードと、互いに素なclassを一つのスーパータイプにまとめるunionキーワードを提案しています。ただし、レコードやunionの代数的性質については述べていません。「Notes on Data Structuring」の頃には、彼の用語法はマッカーシーのそれに近づきます：

我々が関心を持つ型とは、数学者にとってすでになじみ深いものである。すなわち、デカルト積、識別された和集合（Discriminated Unions）、集合、関数、列、そして再帰的構造である。

彼の言う「cartesian products」も「discriminated unions」もどちらもタグ付きで、今日の代数的データ型の使い方と一致しています。彼は主にデータの格納に関心があるため、代数的性質は列挙していませんが、これらの型をいかに効率的に格納するかという議論の中で濃度には触れています。

この論文は、和型がコンパイル時にエラーを検出する手段として論じられた最初の例かもしれません：

もしプログラマが、識別された和集合の値を、元々由来していない型に戻そうとすれば、それは無意味な結果を招きかねない重大なプログラミングエラーである。このエラーは、そのような変換が明示的にも暗黙的にも呼び出されるたびにタグフィールドをテストする実行時チェックによってのみ検出できる。そのようなチェックは時間がかかり、失敗したときには非常に厄介である。したがって我々は、実行中のプログラムでこのエラーが決して起こらないことを保証する記法を求める。その保証は、実行時に処理される値についての知識なしに、テキストを検査するだけで与えられる。もし利用可能なら、そのような保証は自動コンパイラによって与えられうる。

これは私が見つけられた限り、誰かが和型を「discriminated union」と呼んだ最初の例でもあります⁵。その後バーバラ・リスコフがCLUのoneofという和型を説明するのに「discriminated union」を使い、ニクラウス・ヴィルトはPascalがなぜ和型を持たないのかを説明するのに「discriminated union」を使っています。このことから、命令型の世界はホーアの講義から和型について初めて学び、ホーア自身は（完全にではないにせよ）マッカーシーの影響を受けていたのではないかと推測しています⁶。

この時点を境に、和型は命令型プログラミングから姿を消します。20世紀後半の命令型言語はPascalとCの影響が支配的でした。Pascalが和型を持たなかったのは、ヴィルトがタグなし共用体よりも柔軟性に欠けると考えたためです。Cが和型を持たないのは、IBMのPL/Iの型システムを採用したためかもしれません。1964年に最初にリリースされたPL/Iは、積型（彼らはstructsと呼んでいました）は持っていましたが、共用体はタグなしのものだけでした。近年の命令型言語はむしろ関数型プログラミングの世界から和型を取り入れており、話は再び“Proving properties of programs by structural induction”に戻ります。

バーストールの論文

バーストールについて調べるのは信じられないほど骨が折れます。彼の追悼記事には膨大な数の論文や影響力のある教え子たちが列挙されており、関数型プログラミングの初期の発展において彼が巨大な役割を果たしたことは明らかです。しかし、それらの論文のごくわずかしかオンラインで入手できないため、簡単に調べられる範囲には大きな空白があります。これは彼の歴史上の役割を解明しようとする、私なりの精一杯の試みです。

この論文は、リストや木のような再帰的な型の性質を証明することについて書かれています。彼はリストを次のように定義しています：

各構築操作が新しい型を導入し、それらの型の選言もまた型であるべきだと提案する（大まかにLandin 1964に従って）

a cons has an atom and a list, a nil has no components, a list is a cons or a nil.

バーストールは、この記法をP・J・ランディンの“The Mechanical Evaluation of Expressions”（1964年）から得たと言っています。ランディンの使い方は、どうも和型とは言い難いように思えます――値が重なった場合に型を識別する仕組みを持っていたかどうかはっきりしません。むしろ、バーストールが「従っている」のはランディンの再帰的定義の書き方なのではないかと私には思えます。ただ、数回読んだだけでは判断が難しく、私が間違っている可能性も十分にあります。

とはいえ、バーストールは和型を持っており、それは彼の木の定義に見て取れます。木は「nodeかtipかniltree」ですが、tipはitemを「持つ」のであり、item「そのものである」わけではありません。そして後には次のような疑似コードが出てきます：

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

バーストールはまた、自身のアイデアは「ジョン・マッカーシーの研究に基づいている」と述べ、彼の数学的理論の論文を引用しています。バーストールがマッカーシーのdirect unionの概念に触発された可能性も十分にあります。

2025年時点でこの論文は500回以上引用されています。バーストールは後にさらに大きな貢献をすることになりますが、それは1980年のことなので、まずはMLについて触れなければなりません。

ミルナーの論文

これまでに代数的データ型の定義や「Cartesian product」という一般的な用法は見てきましたが、用語としての「sum type」や「product type」はまだ出てきていません。私の知る限り、それはロビン・ミルナーのMLに由来し、“A Theory of Type Polymorphism in Programming”（1977年）で広まったものです：

MLの完全に決定された型（すなわち単相型）は、基本型の集合（int、boolなど）から、二項の中置演算子であるx（デカルト積）、+（非交和）、->（関数型）と、単項の後置演算子であるlistによって構築される。

この論文について注目すべき点がいくつかあります。第一に、もちろん「disjoint sum」を使って型を構築することを説明し、+記号を使っていることです。第二に、ホーアやマッカーシーとは対照的に、「disjoint sum」を正当化も定義もしていないことです。この時点では、ミルナーの読者にとっては常識になっていたのかもしれません。最後に、この論文は和と積がすでに少なくとも2年前にはMLで実装されていたと主張しています。

最古のMLの完全な仕様は残っていませんが、MLが設計された対象であるLCF proverの公開されたソースコードは残っています。これは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))
     )  ;;

ここに「sum」型と「product」型があります！ただし、これらはタグ付きではありません。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”はマッカーシーの論文もホーアやバーストールの論文も引用していないため、ミルナーが彼らに影響を受けたのか、それとも独自にAlgDTを開発したのかははっきりしません。かすかな手がかりとして、続編の論文“A Metalanguage for Interactive Proof in LCF”（1978年）では、彼は三人全員に謝辞を述べています：

我々の研究の理論的基盤の大部分を提供してくれたデイナ・スコットに、スタンフォードでこのプロジェクトの前身を励ましてくれたジョン・マッカーシーに、このプロジェクトに多大な貢献をしてくれたリチャード・ウェイホークに、MLにおける抽象型の概念について助けてくれたトニー・ホーアとジェリー・シュワルツに、実験を通じて最終的な設計段階で助けてくれたエイヴラ・コーンに、そして啓発的な議論をしてくれたロッド・バーストールとエディンバラの多くの同僚に感謝する。

さて、あと三つの言語を残すのみです。

Hope、VAX ML、そしてMiranda

この頃、バーストールは圏論をソフトウェア仕様に応用しており、やがてHOPEの開発へとつながります。“HOPE: An experimental applicative language”（1980年）は、関数型プログラミングへのタグ付き和の最初の導入となりましたが、タグ付き積はまだ含まれていませんでした：

「tree-of-numbers」型を定義するには次のように書ける

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

（記号#は型のデカルト積を表す）

さらに、この論文はいくつかの重要なアイデアを導入しています。一つ目は、コンパイラが和型におけるすべての互いに素な選択肢が処理されているかを網羅的にチェックできるということです：

各データ型は、異なる構築子関数を持つ互いに素なサブタイプの集合を持つことになる。例えば、リストはconsまたはnilで作られる。これらの構築子に関して場合分けを行うのは容易であるべきだし、コンパイラがその分析が網羅的かどうかをチェックするのも容易であるべきだ。これにより、空リストのテストを含め忘れるようなミスを防げる。

さらに、この論文では和型の利用がパターンマッチングによって劇的に簡素化できることも提案されています。これは構造的パターンマッチングが言語に登場した最初の例ではありません（最初はPrologでした）が、関数型プログラミングにおけるパターンマッチングの最初の登場ではあります。

HOPEとほぼ同時期に、バーストールの孫弟子にあたるルカ・カルデリ⁷がMLをVAXとUnixに移植する作業を進めており、その過程でレコード型とバリアント型を追加しました。私の知る限り、これがタグ付きの和とタグ付きの積の両方が関数型プログラミング言語に存在した最初の例です。

これらすべてのアイデアは後にStandard MLに取り入れられ、今日人々が代数的データ型の中核機能とみなしているもの――タグ、コンパイラによる網羅性チェック、そしてパターンマッチング――が成文化されました。

最後に、再びXiaの記事を参照すると、“Miranda: A non-strict functional language with polymorphic types”（1985年）が実際に「Algebraic Data Type」という用語を使った最初の論文です。詳しくはぜひXiaの記事を読むことを強くお勧めします。

非常に危ういまとめ

• マッカーシーが論文で代数的データ型の概念と性質を最初に提案した。ただし本人はそう呼んではいない。
• これは少なくともトニー・ホーアとロッド・バーストールに何らかの影響を与え、彼らはそれぞれ影響力のある論文を書いた。
• AlgDTはALGOL 68、CLU、MLで実装された。ミルナーがマッカーシーの理論を知っていたかどうかは不明だが、おそらく知っていた可能性の方が高いと私は見ている。
• PascalとCによって、和型は命令型プログラミングに足がかりを得ることができなかった。
• バーストールとルカ・カルデリがAlgDTの主要な機能を完成させ、型付き関数型プログラミングの礎として確立した。

これは私が使える時間と資料でできる限りのことです。もし間違いを見つけたら教えてください！

この記事が気に入ったら、ぜひ私のニュースレターに参加してください！毎週新しいエッセイを書いています。

私は企業向けに形式手法のトレーニングを行い、ソフトウェア開発をより速く、安く、安全にしています。詳しくはこちらをご覧ください。