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
リストの長さは、例えばつぎのようになる。