Haskellの真髄に迫る - 一般化代数的データ（７）

１．一般的代数的データ型に米田の補題を利用

米田の補題の説明にだいぶ紙幅を割いてしまったが本題に移ることにする。これまで、長さ注釈つきのリストは一般化代数的データを利用して、次のように定義していた。

{-# LANGUAGE GADTs #-}

data Z   
data S n 

data List a n where
  Nil  :: List a Z
  Cons :: a -> List a m -> List a (S m)

List a Z

は、List aを関手とみなすと、米田の補題から得られた

f a -> (forall x. (a -> x) -> f x)

を用いると、List a Zは

(Z -> n) -> List a n

となる。上記で、forall nという記述を省いているが、nが多相型でforallの意味を含んでいるので省いた。
同様に、Consの部分は、

a -> List a m -> (S m -> n) -> List a n

となる。上記に記述をまとめると、

{-# LANGUAGE GADTs #-}

data Z   
data S n 

data List a n where
  Nil  :: (Z -> n) -> List a n
  Cons :: a -> List a m -> (S m -> n) -> List a n

となる。出力が両方とも一緒、即ち、List a nとなったので、これを通常のデータ型で記述すると次のようになる。

{-# LANGUAGE GADTs, Rank2Types #-}

data Z   
data S n 

data List a n =
  Nil (Z -> n) | forall m. Cons a (List a m) (S m -> n)

また、List aが関手であるので、次のプログラムを必要とする。

instance Functor (List a) where
  fmap f (Nil k) = Nil (f . k)
  fmap f (Cons a as k) = Cons a as (f . k)

２．プログラムを実行する

全体のプログラムは次のようになる。

{-# LANGUAGE GADTs, Rank2Types #-}

class Nat n where
  toInt :: n -> Int

instance Nat Z where
  toInt _ = 0

instance Nat n => Nat (S n) where
  toInt x = 1 + toInt (pred x)
    where
      pred :: S n -> n
      pred = undefined

data Z  
data S n

data List a n =
    Nil (Z -> n)
  | forall m. Cons a (List a m) (S m -> n)

instance Functor (List a) where
  fmap f (Nil k) = Nil (f . k)
  fmap f (Cons a as k) = Cons a as (f . k)

head' :: List a (S n) -> a
head' (Cons a _ _) = a

length' :: List a n -> n
length' = undefined

as1 = Nil id
as2 = Cons 'a' as1 id
as3 = Cons 'b' as2 id
as4 = Cons 'c' as3 id

as11 = Nil id
as12 = Cons 1 as11 id
as13 = Cons 2 as12 id
as14 = Cons 3 as13 id