LoginSignup
12
2

More than 3 years have passed since last update.

@Izawa_

Haskellの代数的データ型とGADTs

Last updated at Posted at 2020-09-05

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は「値コンストラクタを関数として書ける拡張」

参考文献

  1. カインド* -> *を「型を取って型を返す関数」と考えます。実はType Familiesというまさにそんな拡張があるのですが… ↩

  2. 実用的な例は、@HirotoShioiさんので、出たー！幽霊型だー！(Phantom Type)で詳しく解説されています。 ↩

12
2
2

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
12
2