加法和乘法

加法和乘法在這種型別代數中具有等價物。它們對應於標記的聯合產品型別

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)