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.
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₂
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
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