Haskell Language Type algebra Addition and multiplication
Example
The addition and multiplication have equivalents in this type algebra. They correspond to the tagged unions and product types.
data Sum a b = A a | B b
data Prod a b = Prod a b
We can see how the number of inhabitants of every type corresponds to the operations of the algebra.
Equivalently, we can use Either and (,) as type constructors for the addition and the multiplication. They are isomorphic to our previously defined types:
type Sum' a b = Either a b
type Prod' a b = (a,b)
The expected results of addition and multiplication are followed by the type algebra up to isomorphism. For example, we can see an isomorphism between 1 + 2, 2 + 1 and 3; as 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
Rules of addition and multiplication
The common rules of commutativity, associativity and distributivity are valid because there are trivial isomorphisms between the following types:
-- 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)
