代数的データ型はある意味で可換半環とみなせる
ある程度の条件を満たした代数的データ型は単位元を持つ可換半環 (semiring) とみなすことができる。
半環:環の条件のうち加法逆元(負の数)が無いやつ。
可換半環:半環であって乗法が可換なやつ。
可換半環であって可換環じゃないものの例:(ℕ, +, ×)、(ℝ∪{∞}, min, +)
より正確には、型の集まりに対して代数的データ型を作るときの演算(タプルを作るための積と、タグ付きユニオンを作るための和)を入れた代数構造は、可換半環になる。
ただし型の間のequalityはtype isomorphismで与える。
本当は「型の集まり」って何、をちゃんと定義する必要がある。
たとえばシンプルには、A, B ::= 0 | 1 | A + B | A × B として型の集合を定義すれば良い。
可換半環であることの確認
和が単位元を持つ
bottomが単位元0になる ← bottomが言語機能としては存在しない場合はある
A + 0 = A
タグ付きユニオンなので、ここは注意が必要
和が可換モノイドになる
(A + B) + C = A + (B + C)
Either (Either A B) C = Either A (Either B C)
A + B = B + A
Either A B = Either B A
積が単位元を持つ
unitが単位元1になる
A × 1 = A
積が可換モノイドになる
(A × B) × C = A × (B × C)
A × B = B × A
分配則をみたす
A × (B + C) = (A × B) + (A × C)
(A, Either B C) = Either (A, B) (A, C)
0を掛けると0になる
A × 0 = 0