代数的データ型

代数的データ型 (algebraic data type、ADT) は、既にある型を「かつ」(直積) と「or」(直和) で組み合わせて作る型。

直積と直和

新しい型を作る方法は、突き詰めると2つしかない。

• 直積 (product): $A$ の値 かつ $B$ の値を持つ型。座標は「x座標 かつ y座標」なので直積
• 直和 (sum): $A$ の値 or $B$ の値を持ち、どちらなのかが分かる型。図形は「円 or 長方形」なので直和

直積はどの言語にもある (classのフィールドがそれ)。 直和は長らく関数型言語にしかなく、OOP言語には無かった。 継承やnullableやフラグで似せることはできても、場合の集合をコンパイラが知らないので、代わりにはならない。

直積型

型 $A$ と $B$ の直積 $A \times B$ は、$A$ の値と $B$ の値の組の型。 型の値を作る関数を構成子 (constructor) と呼ぶ。 直積の構成子は両方の値を受け取って組を返し (例では Point)、使うときは射影 (projection) で片方ずつ取り出す。

data Point = Point { x :: Double, y :: Double }

struct Point { x: f64, y: f64 }

record Point(double x, double y) {}

フィールドに名前が付いているかどうかは本質ではなく、タプルと同じ型。 要素が0個の直積がunit型で、値は1つだけ。

直和型

型 $A$ と $B$ の直和 $A + B$ は、$A$ の値か $B$ の値のどちらか一方で、どちらなのかが値自身に記録されている型。 構成子は場合ごとに1つずつあり (例では Circle と Rect)、各構成子に型が付く。

data Shape
  = Circle { radius :: Double }
  | Rect { width :: Double, height :: Double }

enum Shape {
    Circle { radius: f64 },
    Rect { width: f64, height: f64 },
}

sealed interface Shape permits Circle, Rect {}
record Circle(double radius) implements Shape {}
record Rect(double width, double height) implements Shape {}

Shape は Circle と Rect の直和で、各場合が直積になっている (sum of products)。 実用上のADTはだいたいこの形。

場合が0個の直和が空型で、値を1つも持たない。 各場合が値を持たない直和が、いわゆるenum。

前提知識

• 集合の記法 ($\times$、$+$、$|A|$)

代数的データ型のコンセプト

直積と直和だけで型を組み立てると、次の2つが型の構成法から機械的に出てくる。

代数的データ型の値はパターンマッチで使う

直和型の値を使うには、どの場合かで分岐する (パターンマッチ)。 型が場合の集合を知っているので、コンパイラは分岐がすべての場合を尽くしているか (網羅性) を検査できる。 これが代数的データ型を使う最大の理由。

代数的データ型は数えられる

型を「その型の値の集合」と見て値の個数を数えると、直積型の個数は掛け算、直和型の個数は足し算になる。 場合の数の積の法則と和の法則そのもの。 型の間の等式を普通の代数と同じ規則で扱えて、listのように自分自身を含む型 (再帰型) は方程式の解として読める。 「代数的」と呼ぶのはこのため。

Option と Result

身近なものが実は直和になっている。

• nullableは直和。$A$ の値 or null、のどちらか一方で、どちらなのかは値を見れば分かる。nullを値が1つだけのunit型と見て $1$ と書けば $A + 1$
• 「結果を返す or エラー (例外) を投げる」も直和。$A$ の値 or $E$ の値のどちらか一方。$A + E$

これを直和型として書いたものが、最もよく使う2つの直和型。

• Option: 「値がある or 値がない」。nullableの直和型版
• Result: 「成功して値がある or 失敗してエラーがある」。例外の直和型版

どちらも「値がない」「失敗した」場合を型に書くことで、呼び出し側に分岐を強制する。 nullや例外との違いは、checkをコンパイラが肩代わりすること。

パターンマッチ

直和型の値はパターンマッチで使う。

area :: Shape -> Double
area (Circle r) = pi * r * r
area (Rect w h) = w * h

fn area(shape: &Shape) -> f64 {
    match shape {
        Shape::Circle { radius } => std::f64::consts::PI * radius * radius,
        Shape::Rect { width, height } => width * height,
    }
}

static double area(Shape shape) {
    return switch (shape) {
        case Circle(double r) -> Math.PI * r * r;
        case Rect(double w, double h) -> w * h;
    };
}

分岐は式で、コンパイラはすべての場合を尽くしているか (網羅性、exhaustiveness) を検査する。 これが直和型を使う最大の理由で、場合を1つ足すと、分岐漏れのある箇所がすべてコンパイル時にエラーになる。 Shape に Triangle を足すと、area を含む Shape のパターンマッチがすべてエラーになって、直すべき箇所を漏れなく教えてくれる。

enum Shape {
    Circle { radius: f64 },
    Rect { width: f64, height: f64 },
    Triangle { base: f64, height: f64 },
}

fn area(shape: &Shape) -> f64 {
    // error[E0004]: non-exhaustive patterns: `&Shape::Triangle { .. }` not covered
    match shape {
        Shape::Circle { radius } => std::f64::consts::PI * radius * radius,
        Shape::Rect { width, height } => width * height,
    }
}

継承で同じことを書くと、Triangle が area を実装し忘れたことは (abstract methodなら) エラーになるが、型の外に書かれた分岐 (型を調べるifの連鎖) の漏れは検出できない。

何にでも合うwildcardの腕を書くと網羅性checkを放棄したことになるので、直和型の分岐には原則として書かない。

型の代数

値の個数

型 $A$ の値の個数を $|A|$ と書く。

直積が積で直和が和なのは、組の作り方が $|A| \cdot |B|$ 通り、どちらか一方の選び方が $|A| + |B|$ 通りだから。 関数が冪なのは、$A$ の各値に $B$ の値を1つずつ割り当てる方法が $|B|^{|A|}$ 通りだから。

$\text{Bool} = 1 + 1$ で個数は2。 $\text{Option}\langle A\rangle = 1 + A$ で個数は $|A| + 1$。 $\text{Result}\langle A, E\rangle = A + E$。 $\text{Bool} \to A = A^2 = A \times A$ で、Boolから引く関数は値の組と同じ。

同型

個数が等しい2つの型の間には、情報を落とさない相互変換 (同型、isomorphism) がある。 型の等式は同型の意味で読む。 高校の代数の等式がそのまま成り立つ。

それぞれに意味がある。

• $A \times 0 \cong 0$: 空型を含む直積は作れない。空型との組の値は存在しない
• $A \times (B + C) \cong (A \times B) + (A \times C)$ (分配則): 「Circle か Rect に色を付けたもの」と「色付き Circle か色付き Rect」は同じ。フィールドを共通の外側に出すか各場合に持たせるかは表現の違いだけ
• $(A + B) \to C \cong (A \to C) \times (B \to C)$: 直和型から引く関数は、場合ごとの関数の組。パターンマッチが各場合に1本ずつ腕を持つのはこれ。冪で書くと $C^{A+B} = C^A \cdot C^B$ (指数法則)
• $(A \times B) \to C \cong A \to (B \to C)$: 2引数の関数は、1つ目の引数を受け取って「2つ目の引数を受け取る関数」を返す1引数の関数と同じ (currying)。冪で書くと $C^{A \times B} = (C^B)^A$

再帰型は方程式の解

listは「空 or 先頭とlistの組」。

data List a = Nil | Cons a (List a)

enum List<A> {
    Nil,
    Cons(A, Box<List<A>>),
}

sealed interface List<A> permits Nil, Cons {}
record Nil<A>() implements List<A> {}
record Cons<A>(A head, List<A> tail) implements List<A> {}

型の等式で書くと $L = 1 + A \times L$ で、$L$ について解くと

listは「要素0個の組 or 1個の組 or 2個の組 or …」と読める。 右辺の $L$ に左辺を代入し続けても同じ無限和になる。

二分木も同様。「空 or 要素と左右の部分木の組」なので、

data Tree a = Leaf | Node (Tree a) a (Tree a)

enum Tree<A> {
    Leaf,
    Node(Box<Tree<A>>, A, Box<Tree<A>>),
}

sealed interface Tree<A> permits Leaf, Node {}
record Leaf<A>() implements Tree<A> {}
record Node<A>(Tree<A> left, A value, Tree<A> right) implements Tree<A> {}

型の等式は $T = 1 + A \times T \times T$ で、$T = 1 + A T^2$ を形式冪級数として解くと $c_n$ がカタラン数になる。

型の微分

$A$ を含む型の値から、$A$ の要素を1つだけ取り除いて、そこを空席 (穴) にしたものを考える。 たとえば組 $(a_1, a_2)$ から $a_2$ を取り除くと $(a_1, \_)$、listの $[a_1, a_2, a_3]$ から $a_2$ を取り除くと、残るのは穴の前の $[a_1]$ と穴の後の $[a_3]$。 残った「穴が1つ空いた構造」の型を、元の型の $A$ についての one-hole context と呼び、$\partial_A$ で書く。 穴に $A$ の値を入れ直すと元の値に戻るので、$\partial_A F \times A$ は「$F$ の値と、その中の1箇所」の組と同じ。

one-hole contextの個数は、普通の微分の規則に従う。

$A \times A$ なら、穴は左か右のどちらか (2通り) で、残るのは $A$ が1つ。 だから $2 \times A$。 listなら $\partial_A L = \partial_A \frac{1}{1-A} = \frac{1}{(1-A)^2} = L \times L$ で、「穴の前のlist」と「穴の後のlist」の組 ($([a_1], [a_3])$) になる。 この one-hole context と穴に入っていた要素の組 ($\partial_A F \times A$) をzipperと呼ぶ。 元の値に「いま注目している1箇所」を付けたもので、不変なデータ構造にcursorを持たせる表現。 listのzipperは「穴の前のlist (逆順)」「注目している要素」「穴の後のlist」の3つ組で、次の操作がすべて定数時間になる。

• 注目している要素を読む、差し替える: 3つ組の真ん中を見る、置き換えるだけ
• cursorを右へ動かす: 注目している要素を前のlistの先頭へ押し込み、後のlistの先頭を新しい注目要素にする。左へは逆
• 元のlistに戻す: 前のlistを逆順にして、注目要素と後のlistをつなぐ

不変なlistの途中の要素を普通に差し替えると先頭からそこまでを作り直すが、zipperならcursorの位置での読み書きが定数時間で済む。 前後2本のlistの間で要素が行き来する様子が名前の由来。 木の微分を取ると、木のzipper (注目している部分木と、根までの経路の各段にある親の要素と兄弟部分木) が同じように機械的に出てくる。