1．長さ注釈つきのリスト
前回リストのつくり方を説明したが、ここでは、Gonzalezのブログを参考に、長さを注釈として持つリストを考えることとする。
長さは、二つのデータ型で表すことにする。一つは長さをゼロとするもの、他の一つは、要素を一つ加えたことにより長さが一つ増えたことを表すものにする。後者の表し方は、少し変に感じるかもしれないが、これは、後で、圏論で自然数をどのように表すかを議論するときに明らかになるので、しばらく我慢してほしい。それでは、次のように表すことにする。
data Z data S n
このデータ型を用いて、長さ注釈つきのリストを前回と同じように、一般化代数的データ(GADT)を用いて表すと次のようになる。
data List a n where Nil :: List a Z Cons :: a -> List a m -> List a (S m)
このプログラムを見ると、一般化代数的データ型を用いることで、作成されるデータの型に対する制約が緩んでいることがわかる。代数的データ型では、Nilの場合もConsの場合も作成されるデータの型は、型コンストラクタで定義したList a nに限られていた。しかし、このプログラムでは、Nilの時に作成されるデータの型は、長さがゼロであることを示すためにList a Zで表している。これに対して、Consの作成されるデータの型は、長さが一つ増えたことを示すList a (S m)となっている。従って、長さを表す部分が、NilではZ、Consでは(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
このプログラムから以下のことがわかる。リストの先頭は、Consとのパターン照合を行っているので、必ず空ではないリストに操作することとなる。このため、このプログラムでは空リストへのアクセスは生じないため、head'の定義は通常のものに比べて、より安全である。
３．プログラムを実行してみる
次のようなデータを用意してプログラムを実行してみる。
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
実行結果は例えば次のようになる。
４．プログラム全体
最後にプログラムの全体を示す。
{-# 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) 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
