Just $ A sandbox

プログラミングと計算機科学とかわいさ

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 hh :: 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>

となることが分かる.