代数的データ型とパターンマッチの網羅性検査

型を「代数」として数える

代数的データ型（algebraic data type、ADT）の「代数的」は比喩ではありません。型を、その型が取りうる値の個数（基数）と同一視すると、型の構成が文字どおり掛け算と足し算で表せるからです。値が1個しかない型（ユニット型 ()）を 1、Bool を 2 と数えるところから始めます。

この見方が効くのは、複合型の安全性を「数」で見通せるからです。フィールドを束ねた組（タプルやレコード）は直積型、複数の選択肢のどれか1つを取る型（Enumや代数的バリアント）は直和型になります。この2つの掛け合わせがADTであり、型システムが静的に値の形を保証する土台になっています。

直積型：フィールドの掛け算

直積型（product type）は、複数の値を同時に持つ型です。(Bool, Bool) という組は、左右それぞれが2通りなので、全体で 2 × 2 = 4 通りの値を取ります。基数が掛け算になるのが「積」と呼ばれる理由です。

struct Point { x: bool, y: bool } // 値の総数は 2 × 2 = 4

ユニット型 () が積の単位元（基数 1）になることも数で確認できます。(A, ()) は A と同じ個数の値しか持たず、n × 1 = n が成立します。直積は「AND」、つまりすべてのフィールドを同時に確定させて初めて1つの値になるという構造を表します。

直和型：選択肢の足し算

直和型（sum type）は、いくつかの選択肢のうちちょうど1つを取る型です。各バリアントは互いに排他的で、基数は足し算になります。

enum Shape {
    Circle(f64),        // 半径ひとつ
    Rect(f64, f64),     // 幅と高さ
}

Shape の値は「Circle であり、かつ中身は実数1つ」または「Rect であり、かつ中身は実数2つ」のどちらかです。タグ（どのバリアントか）と中身がセットになっているため、タグ付き共用体（tagged union）とも呼ばれます。C言語の素の union がタグを持たず危険なのと対照的に、ADTの直和は必ずタグを伴うので、中身を取り出す前に「いまどのバリアントか」を必ず確かめる必要が生じます。これがパターンマッチを呼び込みます。

パターンマッチ：型を分解して値を取り出す

パターンマッチは、直和型のタグで分岐しつつ、直積型の中身を同時に束縛する操作です。match 式は上から順にパターンを照合し、最初に一致した節（arm）の本体を実行します。

fn area(s: Shape) -> f64 {
    match s {
        Shape::Circle(r) => 3.14 * r * r,
        Shape::Rect(w, h) => w * h,
    }
}

ここで本質的なのは、コンパイラが「Shape のすべての値が、いずれかのパターンで確実に処理されるか」を静的に検証する点です。これが網羅性検査（exhaustiveness checking）です。新たに Triangle を Shape に追加すると、この match は型エラーになり、修正漏れがコンパイル時に発覚します。型を「数」として捉えた直和の構造が、この保証を可能にしています。

網羅性検査の原理：抽象値を差し引く

網羅性検査は「足し算の逆算」として理解できます。検査器が扱うのは具体値ではなく、未指定部分をワイルドカード _ で表した抽象値の集合です。出発点は「その型の全値」を表す _ ただ1つ。各パターンが覆う部分をここから差し引き、最後に空集合になれば網羅、残れば残った抽象値こそが反例（漏れている値）です。

差し引きの核は、コンストラクタごとの特殊化（specialization）という操作です。ある列の先頭がコンストラクタ C のとき、C(...) か _ で始まる行だけを残し、C の引数を新たな列として展開します。これを全コンストラクタについて行い、どの分岐でも漏れが無いことを再帰的に確かめます。Maranget による定式化では、この再帰が「有用性」（usefulness）という1つの述語に集約されます。

到達可能性：決して当たらない節を見つける

網羅性が「漏れ」を見るのに対し、到達可能性検査（reachability、冗長性検査）は「無駄」を見ます。ある節のパターンが、それ以前の節すべてによって完全に覆われていれば、その節には永遠に値が到達しません。これも有用性で判定できます。i 番目の節のパターンが、先行する 1 から i-1 番目までの行列に対して有用でないとき、その節は到達不能（冗長）です。

match n {
    x if x > 0 => "正",
    _          => "それ以外",
    1          => "いち",   // 到達不能: 上の _ が全値を覆う
}

網羅性は「ワイルドカード行が有用か」、到達可能性は「各節が先行行に対し有用か」。問いの向きが違うだけで、同じ計算機構を使います。

ガード節と網羅性の限界

検査が原理的に苦手とする場面もあります。代表がガード節（if 条件付きパターン）です。

ガードの中身は任意の式なので、コンパイラはその真偽を一般には決定できません。そこでガード付き節は「マッチするとは限らない」と保守的に見なされ、網羅性の根拠には数えられません。x if x > 0 と x if x <= 0 で論理的には全域を覆っていても、コンパイラはそれを証明できず、別途ワイルドカード節を要求します。安全側に倒すこの設計は、健全性（漏れを見逃さない）を保つための意図的な割り切りです。

再帰的ADTと型の代数方程式

ADTは自己参照でき、これがリストや木を生みます。リスト型は「空、または（先頭要素，残りのリスト）」という直和と直積の組で定義され、型を数の式として書くと L = 1 + A × L という方程式になります。形式的に解けば等比級数 L = 1 + A + A² + ... が現れ、「任意長の列」という直感と一致します。型を代数として扱う見方が、データ構造の本質まで貫いていることが分かります。

data List a = Nil | Cons a (List a)   -- L = 1 + a × L

まとめ：数えられる型が安全を生む

代数的データ型は、直積（AND・掛け算）と直和（OR・足し算）で値の形を厳密に定義する仕組みでした。値が数えられるからこそ、コンパイラは「全値が処理されたか」を有用性という1つの述語で判定でき、網羅性と到達可能性をコンパイル時に保証できます。型を制約ではなく代数として読み直すと、なぜ直和とパターンマッチが堅牢なコードを生むのかが腑に落ちます。この基盤はジェネリクスによる多相と組み合わさり、さらに型推論の文脈ではHindley-Milner型推論が直和・直積の型を自動で導きます。より深い数理的背景は型理論の基礎が、直積を論理積、直和を論理和と対応づけて見せてくれます。