型の数
データ型を数値と見なし、実際に演算を行って代数的な感覚を見る
数値は取りうる値の種類の個数を表す
つまり、その間に全単射を定義できる
Bool$ \congBitのようなもの勿論、
これは$ 2\cong 2
Maybe Bool$ \congA|B|Cのように和積が絡んでも成り立つ
これは$ 2+1\cong 3
0
data Zero
e.g. Void
関連
1
ただ一つの型コンストラクタを持つ
data One = One
e.g.
ユニット型()
2
data Bool = True | False
1+1
e.g.
Bool
data Bit = I | O
∞
こう書いているのを見たことがない
取りうる値の数だと考えれば∞は妥当だと思うmrsekut.icon
これは代数データ型云々の話ではないのか？
e.g.
String
Int
$ a\times b種類の値を持つ
交換律, 結合律を満たす
e.g.
data Product a b = Product a b
(a, b, c)
$ a+b種類の値を持つ
交換律, 結合律を満たす
e.g.
data Either a b = Left a | Right b
同様に考えれば
data Maybe a = Just a | Nothigngは、$ a+1であることがわかる
関数型
冪
a -> bは$ b^a種類の値を持つ
例えば$ 3\to 2という関数型は、$ 2^3を表す
リスト
[a]は、$ \frac{1}{1-a}
リストの長さ$ 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つは一致する
参考
型の数の微分とか