今年も気づけば4月が終わり、いよいよGWですね。先月、社内のLT会で発表した「5分で分かるADT」を文章にまとめてみました。
「Haskellはね、”1＋2＋3”って直接書けるんですよ」
これは、とあるプログラミング勉強会での印象的な言葉です。1大抵のプログラミングに高度な数学知識は必要ありません。しかし、数学的な視点を持つことで、コードをよりシンプルかつ堅牢に設計できると考えられます。2
実は、私たちが普段何気なく使っている「型」の中にも、算数や数学と同じようなシンプルで美しいルールに従っているものがあります。
本記事では、型の概念の一つ代数的データ型（Algebraic Data Type、以下ADT）3 について、「濃度」という視点から解説します。
ADTとは
ADTを理解するには、まずデータ型の定義からです。データ型とは、その型が取り得る値の集合として見られます。この視点からの例として、Booleanという型はTrue（真）とFalse（偽）の二つの値の集合です。
そして、その集合に含まれる要素の個数を、数学では濃度（cardinality）4と呼びます。型$A$の濃度は$|A|$と書きます。では、主要な言語における基本的な型の濃度を見てみましょう。
| 型 | 濃度 | Haskell | TypeScript | Kotlin |
|---|---|---|---|---|
| Empty（空） | 0 | Void |
never |
Nothing |
| Unit（ユニット） | 1 | () |
void / undefined
|
Unit |
| Boolean | 2 | Bool |
boolean |
Boolean |
| Byte | 256 | Int8 |
number（近似） |
Byte |
なぜADTは「代数的」なのか。それは、型の組み合わせが算数の掛け算や足し算として捉えられるからです。
直積型
複数の型を組み合わせて「A かつ B」を表現する構造を、直積型（product type）と呼びます。構造体やタプル（Tuple）が分かりやすい例です。
| 言語 | 実装例 |
|---|---|
| Haskell | data Config = Config Bool Int8 |
| TypeScript | interface Config { enable: boolean; value: number } |
| Kotlin | data class Config(val enable: Boolean, val value: Byte) |
数学的には、型$A$と型$B$の直積型は$A \times B$と書いて、その濃度は次のようになります。
$$|A \times B| = |A| \times |B|$$
すなわち、掛け算です。
例えば、$A$がBooleanで、$B$がByteの場合、それぞれの濃度は$|A| = 2$、$|B| = 256$であるため、直積型Boolean$\times$Byteの濃度は$2 \times 256 = 512$となります。
これは、Booleanの各値に対してByteの全パターンが組み合わさるためです。全ての値は次のように列挙できます。
| 0 | 1 | ... | 255 | |
|---|---|---|---|---|
| True | True,0 | True,1 | ... | True,255 |
| False | False,0 | False,1 | ... | False,255 |
直和型
直積型と異なり、「A または B」のような、いずれか一方の状態を取る構造を、直和型（sum type）と呼びます。古典的な言語では直接的なサポートは少ないものの、TypeScriptの判別可能なユニオン型（Discriminated Union）やRustの列挙型などが代表例です。
| 言語 | 実装例 |
|---|---|
| Haskell | data Setting = Flag Bool | Num Int8 |
| TypeScript | type Setting = { kind: "flag"; v: boolean } | { kind: "num"; v: number } |
| Kotlin |
sealed class Setting { ... }（冗長のため省略） |
数学的には、型$A$と型$B$の直和型$|A + B|$の濃度は次のようになります。
$$|A + B| = |A| + |B|$$
すなわち、足し算です。
例えば、$A$がBoolean、$B$がByteの場合、それぞれの濃度は$|A| = 2$、$|B| = 256$であるため、直和型Boolean$+$Byteの濃度は$2 + 256 = 258$となります。
これは、「Booleanのいずれかの値」または「Byteのいずれかの値」のどちらか一方のみを保持するためです。
関数型
さらに、関数も代数的に扱うことができます。関数型（functional）プログラミングではなく、関数の型（function type）です（笑）。
関数とは、入力$A$の各要素に対して、出力$B$の要素を対応付ける写像です。関数型$A \to B$の濃度は次のようになります。
$$|A \to B| = |B|^{|A|}$$
すなわち、冪乗です。そのため、関数型は指数型（exponential type）とも呼ばれています。
これは、「入力の各要素に対して、それぞれ独立に出力を選択できる」と考えると直感的に理解できます。すべての入力に対する出力の組み合わせを数え上げると、結果として冪乗の形になります。
例えば、$A$がBoolean、$B$がByteの場合、それぞれの濃度は$|A| = 2$、$|B| = 256$であるため、関数型Boolean$\to$Byteの濃度は$256^2 = 65536$となります。
また、$A$がByte、$B$がBooleanの場合、それぞれの濃度は$|A| = 256$、$|B| = 2$であるため、関数型Byte$\to$Booleanの濃度は$2^{256} \approx 1.16\times10^{77}$となります。
応用編：カリー化の”証明”
多引数関数$(A \times B) \to C$と、カリー化された関数$A \to (B \to C)$が同等であることは、関数の濃度を利用すれば分かりやすく説明できます。
解答
- 多引数関数の濃度 $|(A \times B) \to C| = |C|^{|A \times B|} = |C|^{|A| \times |B|}$
- カリー化関数の濃度 $|A \to (B \to C)| = |B \to C|^{|A|} = (|C|^{|B|})^{|A|}$
ここで、指数法則$(x^y)^z = x^{y \times z}$と交換法則$x \times y = y \times x$を適用すると、両者が等価であることが分かります。
あとがき
いかがでしょうか。ここまで見てきたように、ADTを濃度として捉えることで、プログラムの状態空間を定量的に把握できます。
- 直積型は状態を増やす（組み合わせる）
- 直和型は状態を分ける（排他的に分岐する）
このようにADTを活用し、不正な状態を表現できない5ように設計するという考え方は、より堅牢で読みやすいプログラムを書く助けになるはずです。
ちなみに、本記事の元ネタはおそらく数年前Haskellにハマっていた頃、YouTubeで偶然見かけたChris Taylorさんの講演「The Algebra of Algebraic Data Types」6です。