Haskellの代数的データ型とGADTs

# Haskellの代数的データ型とGADTs

Haskellの`data`キーワードで宣言される代数的データ型(*Algebraic data types*)とGADT(一般化された代数的データ型)についてです。まずは直和と直積、GADTと関連する幽霊型について解説していきます。

## 注意

- この記事を書くのに使われているGHCのバージョンは8.8.3です。
 
- 誤りなどあれば、指摘していただけると幸いです。

- この記事では、集合論とHaskellを対応させて考察する部分があります。それらは、読み飛ばしてもらってもかまいません。

- この記事では集合の`{}`を数式ブロックで使っているのですが、うまく表示されません。良い解決法があれば、教えてください。

## 代数的データ型 (Algebraic Data Type)

Haskellでの`data`キーワードでは、値と型を定義できます。

```haskell
data A = A
```

値`A`は型`A`を持ちます。

ここまでは普通のデータ型です。しかし、直積型と直和型によって、より高度なポリモーフィズムを実現する**代数的データ型**を扱えます。

### 直積型 (Product Type)

直積型の値は、1つの値が複数の型の値を持ちます。

```haskell
data Frac = Frac Int Int
```

値コンストラクタ`Frac`は`Int -> Int -> Frac`という型を持ちます。一般化すると、

```haskell
data TypeName = TypeConstructor Type1 Type2 ...
```

となります。

ここからの話は読み飛ばしてもかまいません。

集合論的には、`Int`を集合$ Int $と考え、値をそれぞれの要素と考えると、
$$
Int_1 \times Int_2
$$
と表せます。これはデカルト積または直積集合と呼ばれ、集合$A$と集合$B$に対してできる直積集合$A\times B$は、
$$
A \times B = \{ (a, b) | a \in A かつ b \in B \}
$$
と表せます。例えば、$A = \{1,2,3 \}$、$B=\{4,5,6\}$とすると、直積集合$A \times B$は
$$
\{(a, b)|a \in A かつ b \in B\} \\
= \{(1, 4), (1, 5), (1, 6), (2, 4), (2, 5), (2, 6), (3,4), (3, 5), (3, 6) \}
$$
となります。Haskellの型はこの集合$A \times B$は「出来うる組み合わせによる値の集合」を表しています。といっても、Haskellでは全ての組み合わせは考えません。**Haskellの型を代数の集合に、Haskellの値をその要素に対応させる**とよく分かります。

|                            | 集合論                          | Haskell             |
| -------------------------- | ------------------------------- | ------------------- |
| `Int`型                    | 集合$Int$                       | `Int`型             |
| 値(`10`など)               | $10 \in Int$                    | `10 :: Int`         |
| 直積型(`Frac Int Int`など) | $Int_1 \times Int_2$            | `data Frac Int Int` |
| 直積型の値(`Frac 3 4`など) | $(3, 4) \in Int_1 \times Int_2$ | `Frac 3 4 :: Frac Int Int` |

集合論の直和では型コンストラクタが消えますが、$Frac(Int_1, Int_2) = Int_1 \times Int_2$とすれば同じことです。

### 直和型 (Sum Type)

直和型は、値が複数ある型です。

```haskell
data Bool = False | True
```

型`Bool`の値は`False`か`True`である、ということです。どちらの値でも、型は`Bool`になります。

一般化すると、

```haskell
data Type = Value1 | Value2 | ...
```

ここからの話は読み飛ばしてもかまいません。

集合の直和については、ブリタニカ曰く

> 集合 *A* と *B* との和集合というときに，*A* ，*B*⊆*X* の場合の合併をさす場合もあるが，*A* と *B* を重なりを考えずに並べたものをいう場合もある。これを合併集合と区別するために直和ということもある。転じて，部分集合の合併についても，*A*∩*B*＝φ の場合に限って直和ということもある。

とのこと。ブリタニカを参考にするならば、「直和」は和集合ですから、
$$
A = \{1,2,3\}\\
B = \{6,7,8\}\\
A \amalg B = \{1,2,3,6,7,8\}
$$
となります。

Haskellと対応させて考えるときに、Haskellの直和型では**異なる型の値が複数できる**ことを考えてみましょう。これは、代数的に言い換えると**異なる集合の要素を複数含む**ということです。例えば、次のような直和型を考えます。

```haskell
data BaseOpe = Add | Sub | Mul | Div
data AdvOpe = Exp | Sqrt

data Ope = Base BaseOpe | Adv AdvOpe
```

集合に対応させると、
$$
\begin{eqnarray}
BaseOpe &=& \{Add, Sub, Mul, Div\}\\
AdvOpe &=& \{Exp, Sqrt\}\\
BaseOpe \amalg AdvOpe &=& \{Add, Sub, Mul, Div, Exp, Sqrt\}
\end{eqnarray}
$$
$BaseOpe \amalg AdvOpe$が`Ope`と対応しています。直積型と違い、集合同士が(リストのように)連結される感覚です。$BaseOpe \amalg AdvOpe$には$BaseOpe$と$AdvOpe$の要素がどちらも含まれています。同じように、`Ope`の値には(型コンストラクタはありますが)`BaseOpe`と`AdvOpe`のどちらもなることができます。

### 組み合わせる

直積型と直和型を組み合わせて、

```haskell
data Foo = Bar Int Int | Baz Int Int Int
```

のような型を作ることができます。一般化すると、

```haskell
data Type = ACons AType1 AType2 ...
      | BCons BType1 BType2 ...
      | ...
```

という形式になります。

数式に表すと
$$
(Int_{Bar1} \times Int_{Bar2}) \amalg (Int_{Baz1} \times Int_{Baz2} \times Int_{Baz3})
$$
となります。

### 型コンストラクタとカインド

先の例に出てきた`Bar`と`Baz`は、それぞれ**値コンストラクタ**(*Value constructor*または*Data constructor*)と呼ばれます。これらは値をとり、それぞれ定義元の型の値を返します。

```haskell
Prelude> data Foo = Bar Int | Baz Int Int
Prelude> :t Bar
Bar :: Int -> Foo
Prelude> :t Baz
Baz :: Int -> Int -> Foo
```

それぞれが関数として定義されていることがわかります。この場合はデータ型の宣言に`Int`とあるので`Int`をとるようになっていますが、こうすると

```haskell
Prelude> data Foo a = Bar a
Prelude> :t Bar
Bar :: a -> Foo a
```

値コンストラクタの引数が型変数`a`になっているのが分かります。

しかし、仮に以下のように定義したとして、

```haskell
Prelude> data Alpha   = Alpha Int
Prelude> data Beta  a = Beta Int
Prelude> data Gamma a = Gamma a
```

こうすると、値コンストラクタの型は次のようになります。

```haskell
Prelude> :t Alpha
Alpha :: Int -> Alpha
Prelude> :t Beta
Beta :: Int -> Beta a
Prelude> :t Gamma
Gamma :: a -> Gamma a
```

どれも、何かしらの値を取ってそれぞれの型の値を返す関数です。しかし、型の方はどうでしょう? `Beta`と`Gamma`には`a`がありますが、`Alpha`にはありません。これらの違いは、**カインド**(*Kind*)という概念で説明できます。GHCiでは`:kind`コマンド(`:k`)を使ってカインドを確認できます。

```haskell
Prelude> :k Alpha
Alpha :: *
Prelude> :k Beta
Beta :: * -> *
Prelude> :k Gamma
Gamma :: * -> *
Prelude> :k Maybe
Maybe :: * -> *
```

`*`は型のカインドを意味します。ここに当てはまるのは、`Int`や`Bool`などカインド`*`を持つ型です。カインド`* -> *`を持つ`Maybe`を、`Beta`に与えてみます。

```haskell
Prelude> :k Beta Maybe

<interactive>:1:6: error:
    ? Expecting one more argument to ‘Maybe’
      Expected a type, but ‘Maybe’ has kind ‘* -> *’
    ? In the first argument of ‘Beta’, namely ‘Maybe’
      In the type ‘Beta Maybe’
Prelude> :k Beta Bool
Beta Bool :: *
```

1つ目ではカインドが合わないと怒られました。`Beta`は`*`な型を必要としているのに、`Maybe`のカインドは`* -> *`だったので合致しませんでした。一方、`Bool`は`*`なので`* -> *`の「カインドとしての引数(こんな言葉はないが)」になりえます。[^2]そして、`* -> *`、また`(* -> *) -> *`のような「型を取って型を返すもの」を**型コンストラクタ**(*Type constructor*)と呼びます。`Maybe a`の`a`は**型引数**(*Type parameter*)と呼びます。

### 幽霊型 (Phantom Type)[^3]

ところで、Haskellの`Data.Functor.Const`には奇妙な型が存在します。

```haskell
newtype Const a b = Const { getConst :: a }
```

型宣言の部分には`b`という型変数がありますが、値にはそんな型は存在しません。実際弄ってみると、

```haskell
Prelude Data.Functor.Const> let x = Const 4 :: Const Int Bool
Prelude Data.Functor.Const> getConst x
4
```

確かに`x`の型注釈に表れている`Bool`は`x`に関係していないようです。このような、値として表れない型を幽霊型と呼びます。幽霊型は、主に型レベルで値に情報をつけたいとき(例えば、同じデータ型で種類を区別したい、など)です。

簡単な例として、消費税込みの値段への変換を実装してみます。まず、品物の値段は次のような型になります。

```haskell
newtype Price = Price { getPrice :: Float }
    deriving (Show)

price :: Float -> Price
price = Price
```

そして、税の計算はこのような関数で表せます。

```haskell
withTax :: Price -> Price
withTax =  Price . (* 1.1) . getPrice

withoutTax :: Price -> Price
withoutTax = Price . (/ 1.1) . getPrice
```

しかし、これでは`withTax`を2回適用したり、税抜きの品物を1.1で割ったりなどという誤った使い方が出来てしまいます。そこで、型に「税も含めた値段か」という情報を追加します。

```haskell
newtype Price a = Price { getPrice :: Float }
    deriving (Show)

price :: Float -> Price Unincluded
price = Price

data Included
data Unincluded

withTax :: Price Unincluded -> Price Included
withTax =  Price . (* 1.1) . getPrice

withoutTax :: Price Included -> Price Unincluded
withoutTax = Price . (/ 1.1) . getPrice
```

`Price`に幽霊型`a`を追加して、値を持たない`Included`型と`Unincluded`型を追加しました。これで、税抜きの品物に`withoutTax`を適用しようとすると、

```haskell
*Main> withoutTax $ price 100

<interactive>:16:14: error:
    ? Couldn't match type ‘Unincluded’ with ‘Included’
      Expected type: Price Included
        Actual type: Price Unincluded
    ? In the second argument of ‘($)’, namely ‘price 100’
      In the expression: withoutTax $ price 100
      In an equation for ‘it’: it = withoutTax $ price 100
```

しっかり弾いてくれます。

## GADTs (一般化された代数的データ型)

GADTsは、先ほどの代数的データ型をより拡張性の高いものにするために付けられた拡張です。`{-# LANGUAGE GADTs #-}`をファイルの先頭に追加して、使えるようになります。

GADTsの特徴的な構文の例として、`Maybe a`型をGADTsの構文で記述してみましょう。

```haskell
data Maybe a where
    Nothing :: Maybe a
    Just    :: a -> Maybe a
```

値コンストラクタをそれぞれ関数として型注釈をつけられます。単純な例を示します。`Zero`と`Succ`のみで自然数を構成し、これを計算します。

```haskell
data Expr a = Zero | Succ (Expr a) | IsZero a

eval :: Expr a -> a
eval Zero       = 0
eval (Succ n)   = 1 + eval n
eval (IsZero n) = 0 == eval n -- nが最終的に`Expr Int`になる保証がない
```

実直に実装すると上のようになりますが、値コンストラクタの`a`の部分に`Int`を指定できないので、`eval`をうまく書けません。

GADTsを導入して、値コンストラクタに`Int`を指定して評価可能なことを明示します。

```haskell
{-# LANGUAGE GADTs #-}

data Expr a where
    Zero :: Expr Int
    Succ :: Expr Int -> Expr Int
    IsZero :: Expr Int -> Expr Bool

eval :: Expr a -> a
eval Zero       = 0
eval (Succ n)   = eval n + 1
eval (IsZero n) = eval n == 0
```

```haskell
*Main> eval $ Succ Zero
1
*Main> eval $ IsZero Zero
True
*Main> eval $ Succ $ Succ $ Succ $ Succ Zero
4
```

`Expr Int`として正しく評価されています。

## まとめ

- 代数的データ型は直積型、直和型とそれらの組み合わせからなる
  - 直積型は1つの型の値が複数の値を持つ
  - 直和型は1つの型が複数の値を持つ
- 型コンストラクタは「型を受け取って型を返す」
- カインドは「型の種類」
- 幽霊型は「値には表れない型」
- GADTsは「値コンストラクタを関数として書ける拡張」

## 参考文献

- [コトバンク - 直和](https://kotobank.jp/word/%E7%9B%B4%E5%92%8C-98360)
- [Wikipedia - 直和](https://ja.wikipedia.org/wiki/%E7%9B%B4%E5%92%8C)
- [Seymour Lipschutz 著 マグロウヒル大学演習 離散数学 コンピュータサイエンスの基礎数学](https://www.amazon.co.jp/%E9%9B%A2%E6%95%A3%E6%95%B0%E5%AD%A6%E2%80%95%E3%82%B3%E3%83%B3%E3%83%94%E3%83%A5%E3%83%BC%E3%82%BF%E3%82%B5%E3%82%A4%E3%82%A8%E3%83%B3%E3%82%B9%E3%81%AE%E5%9F%BA%E7%A4%8E%E6%95%B0%E5%AD%A6-%E3%83%9E%E3%82%B0%E3%83%AD%E3%82%A6%E3%83%92%E3%83%AB%E5%A4%A7%E5%AD%A6%E6%BC%94%E7%BF%92-Seymour-Lipschutz/dp/4274130053)
- [GADT - shatsumat/wiwinlh-jp Wiki](https://github.com/shiatsumat/wiwinwlh-jp/wiki/GADT)

[^1]: 和集合とも紛らわしいですが。圏論の直和については未だよく理解していません…。

[^2]: カインド`* -> *`を「型を取って型を返す関数」と考えます。実は[Type Families](https://wiki.haskell.org/GHC/Type_families)というまさにそんな拡張があるのですが…

[^3]: 実用的な例は、@HirotoShioiさんの[で、出たー！幽霊型だー！(Phantom Type)](https://qiita.com/HirotoShioi/items/3444e215070144b8ca0f)で詳しく解説されています。