bitterharvest’s diary

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

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

1.雑記

米田の補題を用いて、射を集合に、逆に、集合を射に変換できることが分かったが、この原理を利用したのがオペレーショナル・モナドである。このブログにも、オペレーショナル・モナドを用いた例を「Haskellで分野向けの機械を開発する」で紹介しているので、参考にしてほしい。

最後に、自然数について触れておく。長さ注釈つきのリストを記述した最後のプログラムは、次のようになっていた。

data List a n where
  Nil  :: (Z -> n) -> List a n
  Cons :: a -> List a m -> (S m -> n) -> List a n

このプログラムでは、自然数は次のように関数の形で表されている。

(Z -> n)
(S m - > n

自然数を[0,1..]のように表すことに慣れている人にとっては、少し、違和感を持つ表現である。しかし、圏論では射を中心に考えるので、自然数を射で表すことに至極当然である。自然数は、圏論の世界ではモノイドと呼ばれる圏に属す。モノイドは、対象は一つで、射はいくつあっても構わない世界である。射の合成は、射を出てきた順につなぎ合わせる。加算・乗算、リストの結合などがモノイドの世界になる。モノイドを図を用いて表現すると、次のようになる。
f:id:bitterharvest:20140917090523p:plain
この図で*は対象を表す。矢印はもちろん射である。

自然数は、射も一つで、それは「その次」という意味で、succで表す。自然数は0(あるいは1)から始まる整数であるが、モノイドの記述では、始まりの場所を示すことができない。そこで、圏論では、終対象1を用意し、そこから、自然数のモノイドに対して、始まりの位置を示す射を定義する。この射をzeroということにすると、圏論では自然数を次のように表すことができる。
f:id:bitterharvest:20140917091233p:plain

(蛇足:無用な混乱を引き起こすかもしれませんが、zeroの先はどこでも構わないし、succの次は1大きい数でなくてもよい。例えば、3大きな数でも構わない。これは、出来上がる構造は全く変わらないので、どのように決めても構わないということによる)。
これで、「Haskellの真髄に迫る - 一般化代数的データ」は終了です。長いこと、お疲れ様でした。

2.課題

長さ注釈つきのリストをオペレーション・モナドを用いて実現し、これまでの議論と比較しなさい。