自然変換の例

『関数プログラミング』の 8.4 に抽象型についての説明があったんだけど、抽象化関数 abstr がそのまま自然変換になってる。こっちには全射（surjective）の条件が必要だけど･･･。

ユーザ定義の (list α) 型と組み込みのリストとの対応関係とか。

抽象化関数の簡単な例は、8.3.2 節で調べた [α] と型 (list α) とのあいだの対応関係を表すものである。

abstr             :: (list α) → [α]
abstr Nil         =  []
abstr (Cons x xs) =  x : abstr xs

チャーチ数と自然数とのあいだの対応関係とか。

abstr          :: nat → num
abstr Zero     =  0
abstr (Succ x) =  abstr x + 1

集合とリストとの対応関係とか。

abstr          :: [α] → set α
abstr []       =  {}
abstr (x : xs) =  {x}∪abstr xs

あとは関手の例も。

集合 s に元 x を追加する演算

addset     :: α → set α → set α
addset x s =  {x}∪s

を考えよう。関数

insert :: α → [α] → [α]

はこの演算をリストによって実現するものであり、これは

abstr (insert x xs) = addset x (abstr xs)

で定められる。このような規定はしばしば可換図式（commuting diagram）と呼ばれる図式で示される。(snip). これは

abstr・(insert x) = (addset x)・abstr

を要求していることを意味している。

      set ――――――→ set
      ↑     addset x     ↑
abstr ｜                  ｜ abstr
      ｜     insert x     ｜
     list ――――――→ list

addset と insert が関手になってる。
……なってる･･･よね？

こうしてみるとなんか自然変換が自然なものに見えてきた不思議。