Haskell Language Category Theory Coproduct of types in Hask



The categorical product of two types A and B should contain the minimal information necessary to contain inside an instance of type A or type B. We can see now that the intuitive coproduct of two types should be Either a b. Other candidates, such as Either a (b,Bool), would contain a part of unnecessary information, and they wouldn't be minimal.

The formal definition is derived from the categorical definition of coproduct.

Categorical coproducts

A categorical coproduct is the dual notion of a categorical product. It is obtained directly by reversing all the arrows in the definition of the product. The coproduct of two objects X,Y is another object Z with two inclusions: i_1: X → Z and i_2: Y → Z; such that any other two morphisms from X and Y to another object decompose uniquely through those inclusions. In other words, if there are two morphisms f₁ : X → W and f₂ : Y → W, exists a unique morphism g : Z → W such that g ○ i₁ = f₁ and g ○ i₂ = f₂

Coproducts in Hask

The translation into the Hask category is similar to the translation of the product:

-- if there are two functions
f1 :: A -> W
f2 :: B -> W
-- and we have a coproduct with two inclusions
i1 :: A -> Z
i2 :: B -> Z
-- we can construct a unique function
g  :: Z -> W
-- such that the other two functions decompose using g
g . i1 == f1
g . i2 == f2

The coproduct type of two types A and B in Hask is Either a b or any other type isomorphic to it:

-- Coproduct
-- The two inclusions are Left and Right
data Either a b = Left a | Right b

-- If we have those functions, we can decompose them through the coproduct
decompose :: (A -> W) -> (B -> W) -> (Either A B -> W)
decompose f1 f2 (Left x)  = f1 x
decompose f1 f2 (Right y) = f2 y