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

１．リストの長さを整数で

ここまで、リストの長さは、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

２．実行結果

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

{-# 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