加法和乘法

加法和乘法在这种类型代数中具有等价物。它们对应于标记的联合和产品类型。

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)