代数的データ型と準同型写像

最近考えていることを述べます. 代数的構造準同型写像に関する考察です. 特に必要な知識は無いつもりですが, Haskellのコードを読めると嬉しいです.

import Prelude hiding

以下のものを隠しておいて下さい.

import Prelude hiding ((+), (++), length, True, False, Bool)

自然数とリストの定義

まず, 自然数(非負整数)とリストの定義からスタートします.

data Nat = Zero | Succ Nat
         deriving (Show, Eq)

自然数はこんな感じです. ペアノの公理ですね. ここでは, 表示できるようにShowクラスのインスタンスとして自動導出しています. 更に, 同値であるか調べられる, という意味で, Eqクラスの自動導出もしています.

ここで注意していただきたいのは, 名前が重要ではないということです. 即ち,

data A = B | C A

と書いてもよいということです. 後に説明しますが, このように一対一対応できて構造が同じような関係を同型と言います.

次はリストの定義です.

data List a = Nil | Cons a (List a)
            deriving (Show, Eq)
infixr 6 `Cons`

任意の型をaに取ってリストを定義します. Nilは空リスト, Consはコンスです(こら). 分かりますよね... 中置演算子として使いたいため, 右結合の演算子としてConsを定義します. Haskellでは標準で

data [a] = [] | a : [a]

のように定義されていますが, (先程のNat vs Aの話と同じで, ) 全く等価です. 同型です. ただ, このように書くと, []がなんなのか曖昧なので*1, 明示的に書きました.

実際に使ってみましょう.

main :: IO ()
main = do
  print $ Zero
  print $ Succ Zero
  print $ Succ (Succ Zero)
  print $ 1 `Cons` 2 `Cons` 3 `Cons` Nil
  print $ 1 `Cons` 3 `Cons` 5 `Cons` 7 `Cons` Nil
Zero
Succ Zero
Succ (Succ Zero)
Cons 1 (Cons 2 (Cons 3 Nil))
Cons 1 (Cons 3 (Cons 5 (Cons 7 Nil)))

自然数の方は良いですね. リストの方は, リストとは言えどもリストに見えず. これで良いのです. もしココで, 普段のリストのイメージとかけ離れたものであれば, それは概念が一歩抽象化した証拠です.

2つの二項演算子の定義

構造に二項演算子を入れ, その演算子の性質を調べることはとても大切な事です. ここでは, NatとList aに各々一つの二項演算子を導入します.

まず最初は, Natの足し算(+)です. 取り敢えず書いてみましょう.

infixl 6 +
(+) :: Nat -> Nat -> Nat
Zero     + y = y
(Succ x) + y = Succ (x + y)

「ゼロを左に足しても変わりません」というのと, 「xの次の数にyを足したのは, xにyを足した数の次の数」というのを書いて見ました. ホントに動くでしょうか.

main :: IO ()
main = do
  let zero = Zero
      one = Succ zero
      two = Succ one
      three = Succ two
      four = Succ three
      five = Succ four
  print $ zero + one
  print $ four + five
Succ Zero
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))

1, 2, 3, ... 9! 4+5=9が計算できましたね!


もう一つの演算子は, リストの結合(++)です.

infixl 5 ++
(++) :: List a -> List a -> List a
Nil       ++ y = y
Cons x xs ++ y = Cons x (xs ++ y)

「空リストを左に結合しても変わりません」というのと, 「Cons x xsをyに左から結合するのは, xs++yの左にCons xするのと同じ」というのを書きました. 確かめてみます.

main :: IO ()
main = do
  let nil = Nil
      onetwo = 1 `Cons` 2 `Cons` Nil
      threefourfive = 3 `Cons` 4 `Cons` 5 `Cons` Nil
  print onetwo
  print threefourfive
  print $ nil ++ onetwo
  print $ onetwo ++ nil
  print $ onetwo ++ threefourfive
  print $ threefourfive ++ onetwo
Cons 1 (Cons 2 Nil)
Cons 3 (Cons 4 (Cons 5 Nil))
Cons 1 (Cons 2 Nil)
Cons 1 (Cons 2 Nil)
Cons 1 (Cons 2 (Cons 3 (Cons 4 (Cons 5 Nil))))
Cons 3 (Cons 4 (Cons 5 (Cons 1 (Cons 2 Nil))))

正しく動いてますね.

Zero, Nil単位元

定義として

Zero + y = y

と書きました. 何にゼロを「左から」足しても変わりません. では,

x + Zero = x

は成り立つのでしょうか. 結論から言うと, (限定的に)成り立つのですが, 証明しなければなりません. 証明は大事です.

x = Zeroの時
(左辺) = Zero + Zero
      = Zero                -- Zero + y = y
(右辺) = Zero
よって(左辺) = Zero = (右辺)

x = kについてk + Zero = kが成り立つとすると, x = Succ kの時
(左辺) = (Succ k) + Zero
      = Succ (k + Zero)    -- (Succ x) + y = Succ (x + y)
      = Succ k             -- 仮定 k + Zero = k
(右辺) = Succ k
よって(左辺) = Succ k = (右辺)

以上の2つから, 数学的帰納法により, 全てのNat型のxについて
x + Zero = x

このことから,

全てのNatなxについて,
Zero + x = x
x + Zero = x

が言えました. このように, 二項演算子で右から足しても左から足しても, 元の値と変わらないようなものを「単位元」と言います. Zeroは(Nat, (+))の単位元です.


めでたしめでたし. となればいいのですが, 残念ながら不完全です. なぜなら, 次のようなxもNat型になるからです.

x :: Nat
x = Succ x

あれまぁ. 証明に追加しましょう.

x = Succ xの時
x + Zero = Succ x + Zero
         = Succ (x + Zero)    -- (Succ x) + y = Succ (x + y)
         ...
         ...???
         = Succ x
         = x

あれれ, 証明できない... x + Zero = xを証明するのにx + Zero = xが必要になりました. 困りました. 実は, この, x = Succ x なる「数」xについての取り扱いは, 私には今のところよく分かっていません. 取り敢えず, ここでは, x = Succ xのようなものを除くNatについてのみ言及します.


お次はNil単位元であることの証明.

Nil ++ y = y

は定義ですので,

x ++ Nil = x

を証明します.

x = Nilの時
(左辺) = Nil ++ Nil
      = Nil          -- Nil ++ y = y
      = x
      = (右辺)

xs ++ Nil = xsが成り立つものとして, x = Cons xx xsの時
(左辺) = (Cons xx xs) ++ Nil
      = Cons xx (xs ++ Nil)         -- Cons x xs ++ y = Cons x (xs ++ y)
      = Cons xx xs
      = x
      = (右辺)

数学的帰納法により, 全てのList a型のデータxについて
x ++ Nil = x

この場合も, 全てではないです. つまり,

x = Cons 0 x
y = Cons 'a' y

のような, 無限リストの場合が尽くされていません. これも先程と同じで, ここでは扱いません. ともあれ,

全てのList aなxについて,
Nil ++ x = x
x ++ Nil = x

が成り立つことが分かりました(但し無限リストは除いていますけどね).


以上のことを少しまとめます.

  1. (Nat, (+))の二項演算子(+)の単位元はZero.
  2. (List a, (++)) の二項演算子(++)の単位元Nil.

あれれ, なんだかこの2つって似た構造に見えて来ませんか?

length関数の定義

リスト(List a)には長さがあります. 長さを計算する関数lengthを書いて見ることにします. ここで重要なのは, リストの長さは非負整数(Nat)であるということです. つまり,

length :: List a -> Nat
length Nil         = Zero
length (Cons x xs) = Succ (length xs)

のように定義することができます. 空のリストの長さはゼロ, Cons x xsの長さはxsの長さの次の数, ということです. もちろんIntを使っても良いのですが, 性質の少ないNatを使います. より少ない性質でも言えることならば, そっちの方がいいに決まっています.


ココまでで, 私たちの手元にあるのは

  1. 二項演算子(+)のあるNat, Zeroが単位元.
  2. 結合する演算子(++)のあるList a, Nil単位元.
  3. リストから自然数への写像length

です. やっとこさ役者が揃いました.

length関数は準同型写像

onetwoの長さは2, threefourfiveの長さは3です. では, onetwo++threefourfiveの長さはいくらでしょう?

main :: IO ()
main = do
  let onetwo = 1 `Cons` 2 `Cons` Nil
      threefourfive = 3 `Cons` 4 `Cons` 5 `Cons` Nil
  print $ length onetwo
  print $ length threefourfive
  print $ length (onetwo ++ threefourfive)
Succ (Succ Zero)
Succ (Succ (Succ Zero))
Succ (Succ (Succ (Succ (Succ Zero))))

長さは5です! もちろん, 2 + 3 = 5です. あれ, 2 + 3ってこっちのコードじゃないの?

  print $ (length onetwo) + (length threefourfive)
Succ (Succ (Succ (Succ (Succ Zero))))

ええ, 確かに5ですね. あれれ... どういうことでしょう...

そうです. リストxと, リストyの長さについて次の式が成り立ちます.

length (x ++ y) = (length x) + (length y)

リストの結合は, その長さの世界では自然数の足し算になる. 直感的に正しそう, ではダメです. 証明します.

x = Nil, y = Nilの時
(左辺) = length (Nil ++ Nil)
      = length (Nil)         -- Nil ++ y = y
      = Zero                 -- length Nil = Zero
(右辺) = (length Nil) + (length Nil)
      = Zero + Zero          -- length Nil = Zero
      = Zero                 -- Zero + y = y
よって(左辺) = Zero = (右辺)

x = Nil, y = Cons yy ysの時
(左辺) = length (Nil ++ (Cons yy ys))
      = length (Cons yy ys)                   -- Nil ++ y = y
(右辺) = (length Nil) + (length (Cons yy ys))
      = Zero + length (Cons yy ys)            -- length Nil = Zero
      = length (Cons yy ys)                   -- Zero + y = y
よって(左辺) = length (Cons yy ys) = (右辺)

x = Cons xx xs, y = Nilの時
(左辺) = length ((Cons xx xs) ++ Nil)
      = length (Cons xx (xs ++ Nil))          -- (Cons x xs) ++ y = Cons x (xs ++ y)
      = length (Cons xx xs)                   -- Nilは(++)の単位元
(右辺) = (length (Cons xx xs)) + (length (Nil))
      = (length (Cons xx xs)) + Zero          -- length Nil = Zero
      = length (Cons xx xs)                   -- Zeroは(+)の単位元
よって(左辺) = length (Cons xx xs) = (右辺)

x = Cons xx xs, y = Cons yy ysの時
length (xs ++ Cons yy ys) = length xs + length (Cons yy ys)を仮定します.
(左辺) = length ((Cons xx xs) ++ (Cons yy ys))
      = length (Cons xx (xs ++ (Cons yy ys)))        -- (Cons x xs) ++ y = Cons x (xs ++ y)
      = Succ (length (xs ++ (Cons yy ys)))
(右辺) = (length (Cons xx xs)) + (length (Cons yy ys))
      = Succ (length xs) + (length (Cons yy ys))          -- length (Cons x xs) = Succ (length xs)
      = Succ ((length xs) + (length (Cons yy ys)))        -- (Succ x) + y = Succ (x + y)
よって仮定とlength (Nil ++ Cons yy ys) = length Nil + length (Cons yy ys)より帰納的に(左辺) = (右辺)が成り立つ. なお, 無限リストは扱っていない.

以上のことから, 無限リスト以外の全てのList aなるxについて
length (x ++ y) = (length x) + (length y)

ふぅ... で, 何が分かったんでしたっけ. まとめましょう.

  1. (Nat, (+)), Zeroは(+)の単位元
  2. (List a, (++)), Nilは(++)の単位元
  3. length :: List a -> Natな関数
  4. length (x ++ y) = (length x) + (length y)
  5. length Nil = Zero

ごちゃごちゃしているので, 一文字の文字に置き換えます. 何も内容は変えていません.

  1. (M, (+)), eは(+)の単位元
  2. (M', (+')), e'は(+')の単位元
  3. f :: M' -> M
  4. f (x +' y) = (f x) + (f y)
  5. f e' = e

というfが見つかったということです.

このようなf, つまり二項演算子を保存して, 一方の単位元を移してもやっぱり単位元になるようなそんなf, それを「準同型写像」と言います. 今までつらつらとNatとList aの構造や演算子を定義してきましたが, その間を取り持つlength関数が準同型写像であることが分かったのです. 準同型写像が見つかったので, NatとList aは準同型であると言うことができます.

平たく言うと, 「NatとList aは, なんか似た構造だ」ということです. NatとListの定義を再度ここに並べてみましょうか*2.

ほら, 似てるでしょう? NatとList a, ZeroとNil, SuccとCons aが対応しています. 類似性は構造の定義だけではなく, 演算子の定義にも言えます. これも並べてみてみましょう.

これを「似てる」と言わずに何と言うのでしょう!!!*3 それにしても, こうやって並べてみないと, SuccとCons xの対応には気が付きませんよね...

自然数もリストもモノイドである

これまでこの言葉をずっと秘めてきたのですが, 我慢できなくなったので書きます. NatもList aもモノイドです. モノイドMというのは,

  1. 二項演算子 □ を持ち, これが閉じている.
  2. 結合律が成り立つ. つまり, 全てのa, b, cについて (a □ b) □ c = a □ (b □ c).
  3. 単位元がある. つまり, あるeが存在して, 全てのaについてe □ a = a □ e = a.

となるような構造のことです. Natはこの性質を満たしているでしょうか?

  1. 二項演算子+を持つ (確かに定義した)
  2. 結合律. 全てのa, b, c について, (a + b) + c = a + (b + c). そりゃ自然数の足し算はこれは成り立ちますな.
  3. 単位元の存在. 全てのNatなxについて, Zero + x = x + Zero = x と成ることを証明した. つまり単位元はZero.

のようになっているので, Natはモノイドです. 一方, List aも結合の演算子(++), 空リストNil単位元とするモノイドになります.

length関数にはこのような性質がありました.

無限リスト以外の全てのList aなるxについて
length (x ++ y) = (length x) + (length y)
length Nil      = Zero

二項演算子を保存し, 単位元単位元に移すような写像. length関数は, モノイド準同型写像になっています.

同型ではないのか

length関数がモノイド準同型写像であることが分かったのですが, 「準」同型写像の「準」って... 同型写像ではないのでしょうか?

準同型写像が, 全単射であれば同型写像になります. 同型写像があれば, 2つの構造は同型, 即ち, 全く同じ構造ということになります. 全単射とは全射単射ということなのですが, length関数について言えば, 単射条件が怪しいです. 具体的に反例を挙げると,

  length (1 `Cons` 2 `Cons` 3 `Cons` Nil)
= length (3 `Cons` 2 `Cons` 1 `Cons` Nil)
= Succ (Succ (Succ Zero))

のように, 同じ長さでも中身が違うリストなんてものはいくらでも作れてしまうのです. よってlength関数は単射ではないので同型写像ではありません.

と言う風に, 一筋縄ではいかないのがパラメトリック多相の難しさ. ここでは, 殆ど意識することのなかったList aのaの構造が問題になってきます. もし,

x :: List ()
x = () `Cons` () `Cons` () `Cons` Nil
main = do
  print x
  print $ length x
Cons () (Cons () (Cons () Nil))
Succ (Succ (Succ Zero))

のように, a = () の場合だと, あるNatな長さlに対応するようなList ()なxは, 一つしか存在しません. つまり単射です. 従って, List ()とNatはモノイド同型, length関数が同型写像である事になります.
List () ≅ Nat
この場合に限り, length関数の逆写像length'を次のように書くことができます.

length' :: Nat -> List ()
length' Zero = Nil
length' (Succ x) = () `Cons` (length' x)

ここで注意していただきたいのは, ()という難解な記号に惑わされてはいけないということです. ()は

data () = ()

と定義されていますが, 別に

data Japan = Japan

と定義するならば,
List Japan ≅ Nat
となります. ()とJapanは同型です. List ()とList Japanも当然同型です.


更に... これまで「自然数」, 「リスト」という言葉でもって, NatやList aを意味づけしてきました. しかし, それも必要ありません. 即ち,

data M1   = E1 | S1    M1
data M2 a = E2 | S2 a (M2 a)

infixl 5 +
(+) :: M1 -> M1 -> M1
E1   + y = y
S1 x + y = S1 (x + y)

infixl 5 ++
(++) :: M2 a -> M2 a -> M2 a
E2      ++ y = y
S2 x xs ++ y = S2 x (xs ++ y)

f :: M2 a -> M1
f E2        = E1
f (S2 x xs) = S1 (f xs)

のように書いても文句が出ないということです. 名前にとらわれずに, 構造と, 演算子の性質に着目して下さい. 今ここに書いた2つのモノイドM1, M2 aは, それぞれNatとList aと同型です.


まとめますと,

  1. data M1 = E1 | S1 M1; (+)
  2. data M2 a = E2 | S2 a (M2 a); (++)
  3. M1, M2 aはモノイド (結合律を満たし, 単位元がある)
  4. f :: M2 a -> M1, モノイド準同型写像fがある.
  5. a ≅ () の時に限り, M2 a ≅ M1, fが同型写像になる. それ以外では, fは忘却関数.

情報が落ちるような関数をたぶん「忘却関数」と言います. (forgetful map なのですが, きちんとした定義は見た事無いので, 非正規なワードなのかもしれません. )

リストとは

Haskellを書くようになると, リストの本質に突き当たります. この記事では, 「リストはモノイドである」という結論になりました. 他にも, 「リストはファンクタである」だとか, 「リストはモナドである」だとか, 色んな事をいう人がうじゃうじゃいます*4. 忘れてはならないのは, 彼らは別に大層なことを言っているのではないということです. 単純に, ある性質(例えば結合律であったり, 単位元を持つことであったり)に着目し, 幾つかの性質をまとめて名前をつけているだけなのです(例えばファンクタ則であったり, モナド則であったり). そして, それらの性質が成り立つような構造をまとめてファンクタやらモナドやらモノイドやら言っているのです. この, 満たすべき性質が付随した一般化された構造を, Haskellではclassと言っています.

私たちは自由気ままに抽象的データ型を定義することができます. これは別にHaskellに限ったことではありません. 勝手に作ったデータ型に対して, あるclassの満たすべき性質を全てパスしたら, 大声で「リストはモナドだ」と言って構いません. 但し, その時には, どんな演算を入れたのか, 本当にその性質を全て満たしたのか, それをきちんと明示して下さい. 主張することは大いに結構ですが, 根拠なき主張ほど見苦しいものはありません.

一つ, 面白い事を書いていた論文を紹介します. Abstractより.

Informal human observations like ‘lists are natural numbers with extra labels’ and ‘vectors are lists indexed by length’ are expressed in a first class language of ornaments ...
Each ornament adds information, so it comes with a forgetful function from fancy data back to plain, expressible as the fold of its ornamental algebra: lists built from numbers acquire the ‘length’ algebra. ...

Ornamental Algebras, Algebraic Ornaments CONOR McBRIDE

なんと. リストとは「飾りのついた自然数」と言っているのです. リストは自然数なのです. 思い起こしてみてください. 今まであなたがリストというものをどう捉えていたのかを.

>>> [1,2,3,4,5]
[1, 2, 3, 4, 5]
>>> len([1,2,3,4,5])
5
>>> [1,2,3,4,5][3]
4
>>>

Pythonのリストです. 振り返ってみると, これまで思っていたリストとは, 自由にインデックスアクセスできて, それは或いはポインターだったりして, len関数は組み込みで... と, 非常にベタベタしたものだったように思います. もう一度この画像を貼ります.

ああ, リストって自然数に飾りがついたものなんだな... リストの見方が少し変わった人がいらっしゃるなら, それだけで光栄です.

で, 何の役に立つの

と聞かれると, ものすごく悲しくなります. あなたはおそらくプログラマーでしょう. 「同じ事を繰り返すな」 そう聞いているはずです. ならば, データ型の同じ性質を抜き出す意味は大いにあります.

例えば, ある入力Xから, 何らかの自然数Natを計算するプログラムf1があったとします.

f1 :: X -> Nat

しかし, 同じような処理で, 情報の違うもの, 例えば整数のリストを返すプログラムf2を書く必要が出たとします.

f2 :: X -> List Int

処理がほとんど同じ時, 同じような関数を二度も書くでしょうか? f1とf2を見比べてみると, 返り値がモノイドであれば処理を統一することに気が付いた, そんな時に看過するでしょうか?

class Monoid m where
  ...
instance Monoid Nat where
  ...
instance Monoid (List a) where
  ...

...

f :: (Monoid m) => X -> m

ええ, こうですよね. fの中で, モノイドならば出来る演算のみを用いることにより, NatであれList aであれ, はたまたあなたのプログラムを使う人が勝手にMonoidのインスタンスにした構造であれ, 何でもござれなのです. この自由度が, 同じ性質を抜き出した最大のメリットであり, 応用例なのです. 「リストは〇〇である」と叫んでも, それを活かせないようでは意味がありませんからね.

モノイドの性質を思い起こしてみると, 結合律と単位元でした. 結合律が成り立つということは, a + b + c + d + ... を, 右から足しても左から足しても大丈夫だと, 保証してくれるのです. これ, ものすごく「いい性質」です. そもそも, リストを3つ結合するという場面で, (右結合か左結合かを気にせずに) x ++ y ++ z と書けること自体, 結合律のおかげなのです.

[追記]
むしろ,

f :: (Monoid m) => [m] -> m

とか

f :: (Monoid m) => m -> m -> m

のようなケースのほうが多いかもしれませんね.
[/追記]

もっとモノイド

モノイドというのは, 結合律と単位元しか要請しませんので, 非常に様々な構造がモノイドの性質をクリアします. 例えばブーリアンです.

data Bool = False | True
          deriving (Show, Eq)

infixl 2 ||
(||) :: Bool -> Bool -> Bool
False || y = y
True  || y = True

Boolの(||)は結合律を満たし, 単位元Falseを持つのでモノイドになります(確認して下さい. Natなどより遥かに証明は簡単です). 気になるのは, この記事でさんざん取り扱ってきたNatやList aとの絡みです. 明らかにNatやList aよりもBoolの方が構造が簡単なので, 忘却関数がありそうです. 実際に, 次のように書けます.

positive :: Nat -> Bool
positive Zero     = False
positive (Succ x) = True

nonempty :: List a -> Bool
nonempty Nil         = False
nonempty (Cons x xs) = True

positive関数は, 自然数が正の数かゼロかチェックする関数です.

全てのx, y :: Natについて
positive (x + y) = (positive x) || (positive y)
positive Zero = False

が成り立つので, positiveもやはり準同型写像です.

nonempty関数は, リストが空のリストかどうかチェックする関数です.

全てのx, y :: List aについて
nonempty (x ++ y) = (nonempty x) || (nonempty y)
nonempty Nil = False

が成り立つので, やっぱりnonemptyも準同型写像になります. ここの証明は簡単(四通り確認するだけ)なので読者に任せます.

改めてこれら3つを見比べてみましょう.

List a, Nat, Boolの関係を図にすると次のようになります.

length, positive, nonempty, 全て準同型写像です. 更に,

nonempty = positive . length

が成り立ちます. これら3つの関数は非常によく似ていて, 定義を並べてみると

となります. 綺麗ですね.

総括

リストと自然数, そしてブーリアンに焦点を当て, 「モノイド」という構造を紹介しました. 応用に関しては非常にぼかしながらも, 書いたつもりです. 個人的には先日, A Play on Regular Expressionsを読んで, 非常に感銘を受けたのです. この論文を読んで, 「あ, Haskellのclassや, 代数的構造ってこうやって使うものなのか」と思ったのです. この論文に出てくる構造は, Semiringという構造なのですが, これを巧みに使っていました. ぜひ読まれることをお勧めします.

今年は私がHaskellを始めた年です. マックレーンも手に取りました. そして, 自然な流れで抽象代数学の重要さに気が付きました. 構造と性質の公理化. 代数学はまだまだ未熟ですが, これから勉強していきたいと思っています.

ソースコード概要

せっかく書いたので貼っておきます. とはいっても, とても短いですね. 性質や証明のほうが大事です.

import Prelude hiding ((+), (++), length, True, False, Bool)

data Bool   = False |         True
            deriving (Show, Eq)

data Nat    = Zero  | Succ    Nat
            deriving (Show, Eq)

data List a = Nil   | Cons a (List a)
            deriving (Show, Eq)
infixr 6 `Cons`


infixl 2 ||
(||) :: Bool -> Bool -> Bool
False     || y = y
True      || y = True

infixl 6 +
(+) :: Nat -> Nat -> Nat
Zero      +  y = y
Succ   x  +  y = Succ   (x + y)

infixl 5 ++
(++) :: List a -> List a -> List a
Nil       ++ y = y
Cons x xs ++ y = Cons x (xs ++ y)


length   :: List a -> Nat
length   Nil         = Zero
length   (Cons x xs) = Succ (length xs)

nonempty :: List a -> Bool
nonempty Nil         = False
nonempty (Cons x xs) = True

positive :: Nat    -> Bool
positive Zero        = False
positive (Succ   x ) = True

main :: IO ()
main = do
  print $ Zero
  print $ Succ Zero
  print $ Succ (Succ Zero)

  print $ 1 `Cons` 2 `Cons` 3 `Cons` Nil
  print $ 1 `Cons` 3 `Cons` 5 `Cons` 7 `Cons` Nil
  print $ 2 `Cons` 3 `Cons` 1 `Cons` Nil

  let zero = Zero
      one = Succ zero
      two = Succ one
      three = Succ two
      four = Succ three
      five = Succ four
  print $ zero + one 
  print $ four + five

  let nil = Nil
      onetwo = 1 `Cons` 2 `Cons` Nil
      threefourfive = 3 `Cons` 4 `Cons` 5 `Cons` Nil
  print onetwo
  print threefourfive
  print $ nil ++ onetwo
  print $ onetwo ++ nil
  print $ onetwo ++ threefourfive
  print $ threefourfive ++ onetwo

  print $ length onetwo
  print $ length threefourfive
  print $ length (onetwo ++ threefourfive)
  print $ (length onetwo) + (length threefourfive)

  print $ length $ 2 `Cons` 3 `Cons` 1 `Cons` Nil ++ 1 `Cons` Nil
  print $ nonempty Nil
  print $ nonempty $ 1 `Cons` Nil
  print $ length Nil
  print $ length $ 1 `Cons` Nil
  print $ (positive . length) Nil
  print $ (positive . length) $ 1 `Cons` Nil

  let three = Succ (Succ (Succ Zero))
      five = Succ (Succ three)
  print $ three + five

  print $ positive Zero
  print $ positive three

*1:種で言えば * か *->* か, ということです

*2:この記事のために特別にシンタックスカラーを用意して色付けしました. NatとListの対応に集中できるように, dataやderiving, infixlなどのHaskell元々のワードの色付けを切りました.

*3:ここが, Twitterで言及したSucc x + y = x + Succ yと, Succ x + y = Succ (x + y)のどちらが綺麗かというところに結びついています(参考: https://twitter.com/itchyny/status/152597684207894528 ). 前者の定義だと, 対応するList aでの演算子がとても奇妙(具体的に言うと, \x y -> (reverse x) ++ yで, 結合法則を満たさない)になるのです.

*4:モノイドになった「リスト」と, ファンクタやモナドになる「リスト」では全然違うことに勘の良い人ならお気づきでしょう.