Haskell Language Category Theory Product of types in Hask
Example
Categorical products
In category theory, the product of two objects X, Y is another object Z with two projections: π₁ : Z → X and π₂ : Z → Y; such that any other two morphisms from another object decompose uniquely through those projections. In other words, if there exist f₁ : W → X and f₂ : W → Y, exists a unique morphism g : W → Z such that π₁ ○ g = f₁ and π₂ ○ g = f₂.
Products in Hask
This translates into the Hask category of Haskell types as follows, Z is product of A, B when:
-- if there are two functions
f1 :: W -> A
f2 :: W -> B
-- we can construct a unique function
g :: W -> Z
-- and we have two projections
p1 :: Z -> A
p2 :: Z -> B
-- such that the other two functions decompose using g
p1 . g == f1
p2 . g == f2
The product type of two types A, B, which follows the law stated above, is the tuple of the two types (A,B), and the two projections are fst and snd. We can check that it follows the above rule, if we have two functions f1 :: W -> A and f2 :: W -> B we can decompose them uniquely as follow:
decompose :: (W -> A) -> (W -> B) -> (W -> (A,B))
decompose f1 f2 = (\x -> (f1 x, f2 x))
And we can check that the decomposition is correct:
fst . (decompose f1 f2) = f1
snd . (decompose f1 f2) = f2
Uniqueness up to isomorphism
The choice of (A,B) as the product of A and B is not unique. Another logical and equivalent choice would have been:
data Pair a b = Pair a b
Moreover, we could have also chosen (B,A) as the product, or even (B,A,()), and we could find a decomposition function like the above also following the rules:
decompose2 :: (W -> A) -> (W -> B) -> (W -> (B,A,()))
decompose2 f1 f2 = (\x -> (f2 x, f1 x, ()))
This is because the product is not unique but unique up to isomorphism. Every two products of A and B do not have to be equal, but they should be isomorphic. As an example, the two different products we have just defined, (A,B) and (B,A,()), are isomorphic:
iso1 :: (A,B) -> (B,A,())
iso1 (x,y) = (y,x,())
iso2 :: (B,A,()) -> (A,B)
iso2 (y,x,()) = (x,y)
Uniqueness of the decomposition
It is important to remark that also the decomposition function must be unique. There are types which follow all the rules required to be product, but the decomposition is not unique. As an example, we can try to use (A,(B,Bool)) with projections fst fst . snd as a product of A and B:
decompose3 :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3 f1 f2 = (\x -> (f1 x, (f2 x, True)))
We can check that it does work:
fst . (decompose3 f1 f2) = f1 x
(fst . snd) . (decompose3 f1 f2) = f2 x
But the problem here is that we could have written another decomposition, namely:
decompose3' :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool)))
decompose3' f1 f2 = (\x -> (f1 x, (f2 x, False)))
And, as the decomposition is not unique, (A,(B,Bool)) is not the product of A and B in Hask
