Haskellの代数的データ型とGADTs
Haskellのdata
キーワードで宣言される代数的データ型(Algebraic data types)とGADT(一般化された代数的データ型)についてです。まずは直和と直積、GADTと関連する幽霊型について解説していきます。
注意
-
この記事を書くのに使われているGHCのバージョンは8.8.3です。
-
誤りなどあれば、指摘していただけると幸いです。
-
この記事では、集合論とHaskellを対応させて考察する部分があります。それらは、読み飛ばしてもらってもかまいません。
-
この記事では集合の
{}
を数式ブロックで使っているのですが、うまく表示されません。良い解決法があれば、教えてください。
代数的データ型 (Algebraic Data Type)
Haskellでのdata
キーワードでは、値と型を定義できます。
data A = A
値A
は型A
を持ちます。
ここまでは普通のデータ型です。しかし、直積型と直和型によって、より高度なポリモーフィズムを実現する代数的データ型を扱えます。
直積型 (Product Type)
直積型の値は、1つの値が複数の型の値を持ちます。
data Frac = Frac Int Int
値コンストラクタFrac
はInt -> Int -> Frac
という型を持ちます。一般化すると、
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)
直和型は、値が複数ある型です。
data Bool = False | True
型Bool
の値はFalse
かTrue
である、ということです。どちらの値でも、型はBool
になります。
一般化すると、
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の直和型では異なる型の値が複数できることを考えてみましょう。これは、代数的に言い換えると異なる集合の要素を複数含むということです。例えば、次のような直和型を考えます。
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
のどちらもなることができます。
組み合わせる
直積型と直和型を組み合わせて、
data Foo = Bar Int Int | Baz Int Int Int
のような型を作ることができます。一般化すると、
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)と呼ばれます。これらは値をとり、それぞれ定義元の型の値を返します。
Prelude> data Foo = Bar Int | Baz Int Int
Prelude> :t Bar
Bar :: Int -> Foo
Prelude> :t Baz
Baz :: Int -> Int -> Foo
それぞれが関数として定義されていることがわかります。この場合はデータ型の宣言にInt
とあるのでInt
をとるようになっていますが、こうすると
Prelude> data Foo a = Bar a
Prelude> :t Bar
Bar :: a -> Foo a
値コンストラクタの引数が型変数a
になっているのが分かります。
しかし、仮に以下のように定義したとして、
Prelude> data Alpha = Alpha Int
Prelude> data Beta a = Beta Int
Prelude> data Gamma a = Gamma a
こうすると、値コンストラクタの型は次のようになります。
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
)を使ってカインドを確認できます。
Prelude> :k Alpha
Alpha :: *
Prelude> :k Beta
Beta :: * -> *
Prelude> :k Gamma
Gamma :: * -> *
Prelude> :k Maybe
Maybe :: * -> *
*
は型のカインドを意味します。ここに当てはまるのは、Int
やBool
などカインド*
を持つ型です。カインド* -> *
を持つMaybe
を、Beta
に与えてみます。
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
は*
なので* -> *
の「カインドとしての引数(こんな言葉はないが)」になりえます。1そして、* -> *
、また(* -> *) -> *
のような「型を取って型を返すもの」を型コンストラクタ(Type constructor)と呼びます。Maybe a
のa
は型引数(Type parameter)と呼びます。
幽霊型 (Phantom Type)2
ところで、HaskellのData.Functor.Const
には奇妙な型が存在します。
newtype Const a b = Const { getConst :: a }
型宣言の部分にはb
という型変数がありますが、値にはそんな型は存在しません。実際弄ってみると、
Prelude Data.Functor.Const> let x = Const 4 :: Const Int Bool
Prelude Data.Functor.Const> getConst x
4
確かにx
の型注釈に表れているBool
はx
に関係していないようです。このような、値として表れない型を幽霊型と呼びます。幽霊型は、主に型レベルで値に情報をつけたいとき(例えば、同じデータ型で種類を区別したい、など)です。
簡単な例として、消費税込みの値段への変換を実装してみます。まず、品物の値段は次のような型になります。
newtype Price = Price { getPrice :: Float }
deriving (Show)
price :: Float -> Price
price = Price
そして、税の計算はこのような関数で表せます。
withTax :: Price -> Price
withTax = Price . (* 1.1) . getPrice
withoutTax :: Price -> Price
withoutTax = Price . (/ 1.1) . getPrice
しかし、これではwithTax
を2回適用したり、税抜きの品物を1.1で割ったりなどという誤った使い方が出来てしまいます。そこで、型に「税も含めた値段か」という情報を追加します。
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
を適用しようとすると、
*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の構文で記述してみましょう。
data Maybe a where
Nothing :: Maybe a
Just :: a -> Maybe a
値コンストラクタをそれぞれ関数として型注釈をつけられます。単純な例を示します。Zero
とSucc
のみで自然数を構成し、これを計算します。
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
を指定して評価可能なことを明示します。
{-# 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
*Main> eval $ Succ Zero
1
*Main> eval $ IsZero Zero
True
*Main> eval $ Succ $ Succ $ Succ $ Succ Zero
4
Expr Int
として正しく評価されています。
まとめ
- 代数的データ型は直積型、直和型とそれらの組み合わせからなる
- 直積型は1つの型の値が複数の値を持つ
- 直和型は1つの型が複数の値を持つ
- 型コンストラクタは「型を受け取って型を返す」
- カインドは「型の種類」
- 幽霊型は「値には表れない型」
- GADTsは「値コンストラクタを関数として書ける拡張」
参考文献
- コトバンク - 直和
- Wikipedia - 直和
- Seymour Lipschutz 著 マグロウヒル大学演習 離散数学 コンピュータサイエンスの基礎数学
- GADT - shatsumat/wiwinlh-jp Wiki
-
カインド
* -> *
を「型を取って型を返す関数」と考えます。実はType Familiesというまさにそんな拡張があるのですが… ↩ -
実用的な例は、@HirotoShioiさんので、出たー!幽霊型だー!(Phantom Type)で詳しく解説されています。 ↩