代数的データ型が「代数」と呼ばれる所以

データ型を数値と見なし、実際に演算を行って代数的な感覚を見る

数値は取りうる値の種類の個数を表す

inhabitantの個数、cardinality

同じ型の数の型同士は同型になる

つまり、その間に全単射を定義できる

Bool \cong Bit のようなもの勿論、

これは2\cong 2

Maybe Bool \cong A|B|C のように和積が絡んでも成り立つ

これは2+1\cong 3

0

e.g. Void

関連

1

ただ一つの型コンストラクタを持つ

e.g.

ユニット型 ()

2

1+1

e.g.

∞

とは言わない #??

こう書いているのを見たことがない

取りうる値の数だと考えれば∞は妥当だと思う

これは代数データ型云々の話ではないのか？

e.g.

a\times b種類の値を持つ

交換律, 結合律を満たす

e.g.

a+b種類の値を持つ

交換律, 結合律を満たす

e.g.

同様に考えれば

data Maybe a = Just a | Nothigng は、a+1であることがわかる

関数型

冪

a -> b はb^a種類の値を持つ

例えば3\to 2という関数型は、2^3を表す

指数法則が成り立つ

リスト

[a] は、\frac{1}{1-a}

ここで2つの考え方でコレを導いている

リストの長さnごとに、a^nを足し合わせたものなので\sum_{n\ge 0}a^n

[] と x:xs の和と考えることで、T=1+a\times Tと書ける

よって、T=\frac{1}{1-a}

-1\lt a\lt 1の時、この2つは一致する

参考

型の数の微分とか