加法和乘法
加法和乘法在這種型別代數中具有等價物。它們對應於標記的聯合和產品型別。
data Sum a b = A a | B b
data Prod a b = Prod a b
我們可以看到每種型別的居民數量如何與代數的運作相對應。
同樣地,我們可以使用 Either
和 (,)
作為加法和乘法的型別建構函式。它們與我們之前定義的型別是同構的:
type Sum' a b = Either a b
type Prod' a b = (a,b)
加法和乘法的預期結果之後是型別代數直到同構。例如,我們可以看到 1 + 2,2 + 1 和 3 之間的同構; 為 1 + 2 = 3 = 2 + 1。
data Color = Red | Green | Blue
f::Sum () Bool -> Color
f (Left ()) = Red
f (Right True) = Green
f (Right False) = Blue
g::Color -> Sum () Bool
g Red = Left ()
g Green = Right True
g Blue = Right False
f' :: Sum Bool () -> Color
f' (Right ()) = Red
f' (Left True) = Green
f' (Left False) = Blue
g' :: Color -> Sum Bool ()
g' Red = Right ()
g' Green = Left True
g' Blue = Left False
加法和乘法規則
交換性,結合性和分配性的共同規則是有效的,因為以下型別之間存在微不足道的同構現象:
-- Commutativity
Sum a b <=> Sum b a
Prod a b <=> Prod b a
-- Associativity
Sum (Sum a b) c <=> Sum a (Sum b c)
Prod (Prod a b) c <=> Prod a (Prod b c)
-- Distributivity
Prod a (Sum b c) <=> Sum (Prod a b) (Prod a c)