DataKindsとGADTの使い方について
Haskellで型レベルプログラミング(あるいはごく簡単な証明)を書くときに, DataKindsでデータ型をそのまま持ち上げると困る場面がある.
{-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies #-} data a :=: b where Refl :: a :=: a data Nat = Zero | Succ Nat type family (:+:) a b where Zero :+: n = n (Succ n) :+: m = Succ (n :+: m)
と定義した時, 「任意の自然数nについてn+0=n」を示すにはどうすればよいだろうか.
prop :: (n :: Nat) -> (n :+: Zero) :=: n prop = undefined {- error: Expected a type, but ‘n’ has kind ‘Nat’ In the type signature for ‘prop’: prop :: (n :: Nat) -> (n :+: Zero) :=: n -}
はコンパイルが通らない.
これは, n :: Nat
だが(:=:) :: * -> * -> *
なので, カインドが合わないと怒られている.
こういう時に, Natの方の定義を工夫して, 上のような命題が表現できるようにしたい.
[追記] コメントで教えてもらったように,
data SNat (n :: Nat) where SZ :: SNat Zero SS :: SNat n -> SNat (S n)
として, Nat a
とする代わりにSNat a
としてやれば上手くいくみたいです。
[/追記]
(Kindに昇格したい)データ型が与えられた時, 以下のような変形を行う.
data Hoge = A a b | B c ↓ data A a b data B c data Hoge h where A :: a -> b -> Hoge (A a b) B :: c -> Hoge (B c)
このとき, Hoge h
はh :: Hoge
のように考えればよい.
これによって自然数の例も上手くかける.
data Zero data Succ n data Nat n where Zero :: Nat Zero Succ :: Nat n -> Nat (Succ n) type family (:+:) a b where Zero :+: n = n (Succ n) :+: m = Succ (n :+: m) prop :: Nat a -> (a :+: Zero) :=: a prop Zero = Refl prop (Succ n) = case prop n of Refl -> Refl
上のやり方は, GADTの使い方をよく考えれば自然に分かる: 集合AがA := {(x,y)|x ∈ X, y ∈ Y}によって定義される時,
data A a where pair :: X -> Y -> A <X,Y>
と置くと, A *
型の値全体とAは一致する.
pair
によって構成される値の型はA <X,Y>
となっているが, これはXとYの値((x,y)
のこと)を保持する必要があるので直積の形にする.
さらにAがいくつかの集合の和の形にかけているとき, すなわちA := {(x,y)}∪{(z,w)} = A1∪A2のような場合は, Aの元はA1またはA2に入っているので, 上で定義したpair_A1とpair_A2の直和の形にかけていると考えればよい.
data A a where pair_1 :: X -> Y -> A <X,Y> pair_2 :: Z -> W -> A <Z,W>
あるいはAが帰納的な定義になっている場合(自然数など)の場合も, 全く同様に定義ができる.
自然数の例では, N = {0}∪{succ n | n ∈ N}
より,
data Nat n where pair_0 :: {*} -> Nat <{*}> pair_succ :: Nat n -> Nat <succ n>
となることが分かる.