読者です 読者をやめる 読者になる 読者になる

bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

Haskellの真髄に迫る - 一般化代数的データ(3)

1.リストの長さを整数で

ここまで、リストの長さは、ZとS nを用いて表してきたが、リストの長さを分かりやすくするために、整数で表すことにする。そこで、自然数を表す型クラスを準備する。ここでは、これはNatで表すこととする。そして、この型クラスは、自然数を整数で表す関数toIntを有しているものとする。これらの定義は次のように表される。

class Nat n where
  toInt :: n -> Int

Natの方クラスを実装することにする。これまでと同じように、ZとS nで表すことにする。(前の繰り返しになるが、Zはゼロを表す意味で、S nはnの次に来る自然数という意味で使っている)。インスタンスZは、自然数の始まりを表し、これは通常0としているので、次のように表すことができる。

instance Nat Z where
  toInt _ = 0

また、インスタンスS nは、自然数を整数で表したものを再帰的に求めるようにすると、次のようになる。ここで、predはpredececcorの略で、xのひとつ前の自然数を表す。

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

2.実行結果

プログラムの全体を表すと次のようになる。

{-# LANGUAGE GADTs #-}

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 where
  Nil  :: List a Z
  Cons :: a -> List a m -> List a (S m)

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

tail' :: List a (S n) -> List a n
tail' (Cons a b) = b

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

ex1 = Nil
ex2 = Cons 'a' ex1
ex3 = Cons 'b' ex2
ex4 = Cons 'c' ex3

ex11 = Nil
ex12 = Cons 1 ex11
ex13 = Cons 2 ex12
ex14 = Cons 3 ex13

リストの長さは、例えばつぎのようになる。
f:id:bitterharvest:20140913120127p:plain