bitterharvest’s diary

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

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

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)と異なるデータ型を用いている。このように、値コンストラクタの求めに応じて、作成されるデータの型を変えられるのが、一般化代数的データの利点である。

2.リストの先頭、残りのリスト、長さを求める

長さ注釈つきのリストもリストであることには変わりないので、ここで、リストの先頭、先頭を除いた残りのリスト、リストの長さを求める関数を定義する。

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'の定義は通常のものに比べて、より安全である。

3.プログラムを実行してみる

次のようなデータを用意してプログラムを実行してみる。

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:20140909053525p:plain

4.プログラム全体

最後にプログラムの全体を示す。

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