As functional programmers we are interested in functions. Category theorists are similarly interested in morphisms. There is a slight difference in approach, though. A programmer must implement a function, whereas a mathematician is often satisfied with the proof of existence of a morphism (unless said mathematician is a constructivist). Category theory if full of such proofs. It turns out that many of these proofs can be converted to code, often resulting in quite unexpected encodings.

A lot of objects in category theory are defined using universal constructions and universality is used all over the place to show the existence (as a rule: unique, up to unique isomorphism) of morphisms between objects.

There are two major types of universal constructions: the ones asserting the mapping-in property, and the ones asserting the mapping-out property. For instance, the product has the *mapping-in* property.

# Product

Recall that a product of two objects and is an object together with two projections:

This object must satisfy the universal property: for any other object with a pair of morphisms:

there exists a unique morphism such that:

In other words, the two triangles in Fig 1 commute.

This universal property can be used any time you need to find a morphism that’s *mapping into* the product, and it can actually produce code.

For instance, let’s say you want to find a morphism from the terminal object to . All you need is to define two morphisms and . This is not always possible, but if it is, you are guaranteed the existence of a morphism (Fig 2).

Morphisms from the terminal object are called *global elements*, so we have just shown that, as long as and have global elements, say and , their product has a global element too. Moreover the projection of this global element is the same as , and is the same as . In other words, an element of a product is a pair of elements. But you probably knew that.

The universal construction of the product is implemented as an operator in Haskell:

(&&&) :: (c->a) -> (c->b) -> (c -> (a, b))

We can also go the other way: given a mapping-in , we can always extract a pair of morphisms:

This bijection between and a pair of morphisms is in fact an *adjunction*.

You might think this kind of reasoning is very different from what programmers do, but it’s not. Here’s one possible definition of a product in Haskell (besides the built-in one, `(,)`

):

data Product a b = MkProduct { fst :: a , snd :: b }

It is in one-to-one correspondence with what I’ve just explained. The two functions `fst`

and `snd`

are and , and `MkProduct`

corresponds to our . The categorical definition is just a different, much more general, way of saying the same thing.

Here’s another application of universality: Show that product is functorial. Suppose that you have a pair of morphisms:

and you want to lift them to a morphism:

Since we are dealing with products, we should use the mapping-in property. So we draw the universality diagram for the target , and put the source at the top. The pair of functions that fits the bill is (Fig 3).

The universal property gives us, uniquely, the , which is usually written simply as .

*Exercise for the reader*: Show, using universality, that categorical product is symmetric.

# Coproduct

The coproduct, being the dual of the product, is defined by the universal mapping-out property, see Fig 4.

So if you need a morphism *from* a coproduct to some , it’s enough to define two morphisms:

This universal property may also be restated as the isomorphism between pairs of morphisms and morphisms of the type (so there is, in fact, a corresponding adjunction).

This is easily illustrated in Haskell:

h :: Either a b -> c h (Left a) = f a h (Right b) = g b

Here `Left`

and `Right`

correspond to the two injections and . There is a convenient function in Haskell that encapsulates this universal construction:

either :: (a->c) -> (b->c) -> (Either a b -> c)

*Exercise for the reader*: Show that coproduct is functorial.

So next time you ask yourself, what can I do with a universal construction? the answer is: use it to define a morphism, either mapping in or mapping out of your construct. Why is it useful? Because it decomposes a problem into smaller problems. In the examples above, the problem of constructing one morphism was nicely decomposed into defining and separately.

The flip side of this is that there is no simple way of defining a mapping *out* of a product or a mapping *into* a coproduct.

# Distributive Law

For instance, you might wonder if the familiar distributive law:

holds in an arbitrary category that defines products and coproducts (so called bicartesian category). You can immediately see that defining a morphism from right to left is easy, because it involves the mapping out of a coproduct. All we need is to define a pair of morphisms leading to the common target (Fig 5):

The trick is to take advantage of the functoriality of the product, which we have already established, and use it to implement and as:

But if you try to construct a proof in the other direction, from left to right, you’re stuck, because it would require the mapping *out* of a product. So the distributive property does not hold in general.

“Wait a moment!” I hear you say, “I can easily implement it in Haskell.”

f :: (Either a b, c) -> Either (a, c) (b, c) f (Left a, c) = Left (a, c) f (Right b, c) = Right (b, c)

# Exponential

That’s correct, but Haskell does a little cheating behind the scenes. You can see it clearly when you convert this code to point free notation (I’ll explain later how I figured it out):

f = uncurry (either (curry Left) (curry Right))

I want to direct your attention to the use of `curry`

and `uncurry`

. Currying is the application of another universal construction, namely that of the exponential object , representing the function type `b -> c`

. This is exactly the construction that provides the missing *mapping out* of a product, `(a, b) -> c`

. Here we go:

uncurry :: (c -> (a -> b)) -> ((c, a) -> b)

Categorically, we have the bijection between morphisms (again, a sign of an adjunction):

Universality tells us that for every and there is a unique in Fig 6 (and vice versa). The arrow is the lifting of the pair by the product functor (we’ve established the functoriality of the product earlier).

Not every category has exponentials–the ones that do are called cartesian closed (cartesian, because they must also have products).

So how does the fact that we have exponentials in Haskell help us here? We are trying to define a mapping out of a product:

Here’s where the exponential saves the day. This mapping exists if we can define another mapping:

see Fig 7.

This morphism, in turn, is easy to define, because it involves a mapping out of a sum. We just need a pair of morphisms:

We can define the first morphism using the universal property of the exponential, picking the injection :

This translates to Haskell as `h1 = curry Left`

. Similarly for we get `curry Right`

.

We can now combine all these diagrams into a single point-free definition, and that’s exactly how I came up with the original code:

f = uncurry (either (curry Left) (curry Right))

Notice that `curry`

is used to get from to , and `uncurry`

from to in the original diagram.

Products and coproducts are examples of more general constructions called limits and colimits. Importantly, the universal property of limits can be used to define the mapping-in morphisms, whereas the universal property of colimits allows us to define the mapping-out morphisms. I’ll talk more about it in the upcoming post.

December 9, 2019 at 12:00 am

[…] Перевод статьи Бартоша Милевски «Programming with Universal Constructions» (исходный текст расположен по адресу — Текст оригинальной статьи). […]