Я ☞ Articles ☞ Push it to the limit!

If you want to quickly take a look at how limits/colimits are used in order to get some intuition on it first you can jump to Products and sums section.

Constant functors

Functor is a mapping between categories:

There is an interesting type of functor called constant - it sends all morphisms to identity and all objects to a specific object:

A bit later we will discover in what sense this special object should be, but we still need some prerequisites just in order to come to a difinition.

Put some cones first…

I hope you didn’t forget about natural transformations yet:

So what will happen if we try to make a natural transformation between a constant functor and some arbitrary one?

Wow, the source category get squashed! Let’s rotate this diagram a bit so that…

… now you can see that it’s a cone! We replaced TT[i] by X since it’s literally just an object.

I’m actually superoversimplifying here. A cone is a natural transformation between a diagram (a functor between an indexed category and a normal one) and a constant functor. I just want to avoid this detail since we are not going to use it at all.

Push it to the limit

Let’s say that there could be many objects we want to refer our constant functor to.

But you can see that X is kinda special one since all objects in the end refer to this once - a frontier, there is no objects behind. This special object is called a limit.

Discrete categories

It’s kinda weird to start talking about categories now since we ignored it so far. But here we go:

Category is a bunch of objects so that:

• All morphisms between objects are associative
• Every object has its own identity morphism

Hey, I wouldn’t bring this topic today if it wouldn’t be important! There is an interesting case of categories without morphisms between objects (only identities) called discrete.

All morphisms are gone… (except identities). But it doesn’t make it useless though!

Since discrete category is still a category, we can try to map a functor between them.

Functor between discrete categories is going to look like this:

We almost done with theory - it’s time to bring our intuition into play.

Products and sums

If we try to use a discrete category as a target for a cone:

You could recognize a difinition of a Product!

So, if limit is a Product, then how do we get a Sum? Obviously, just reverse the arrows!

You can notice that for Sum morphism titles are capitalized. This is because they are constructors - in terms of Haskell:

This: i `AR__` i `S` ii
That: ii `AR__` i `S` ii

Compare it to morphisms for Products:

this: i `P` ii `AR__` i
that: i `P` ii `AR__` ii

Products and Sum are actually the only datatypes (defined with data keyword) in Я. All other definitions are either newtypes or aliases.

Decomposing trees

Here is an example that could help you understand that Product is actually a limit:

You can either apply unwrap morphism thrice or use objective to get rid of all wrappers:

(unwrap `ha` unwrap `ha` unwrap): Tree i `AR___` i `p` Forest i
                 (objective): Tree i `AR___` i `p` Forest i 

But it doesn’t change the main point - Product is a limit for Tree construction.

Case splitting

Boolean, Progress, Optional in Я are just wrappers over Sums - so we can say that Sum is a colimit.

Supertype (Boolean) ~ Unit `S` Unit
Supertype (Optional i) ~ Unit `S` i
Supertype (Progress e i) ~ e `S` i

Here is a diagram for Optional, for Boolean and Progress it’s going to look similar. The difference between them is how Units are arranged:

We can case split any expressions which objective target is Sum with la operator:

This `la` That `li` by False `AR__` by This
This `la` That `li` by True `AR___` by That
This `la` That `li` by None `AR___` by This
This `la` That `li` by Some `AR___` by That
This `la` That `li` by Error `AR__` by This
This `la` That `li` by Valid `AR__` by That

We also can case split a List - it can either be empty (Unit) or contain at least one item (Nonempty List):

Notice, that compared to a diagram with a Tree morphisms are reversed! Since Tree target objective is a Product and for List it’s a Sum.

(wrap `ha` wrap): Unit `S` Nonempty List i `AR___` Tree i
   (objective): Unit `S` Nonempty List i `AR___` Tree i

This is how we can case split a List:

(Empty @List `la` is `ho'he` List): List item `AR___` List item

Argument branching

So far we covered la operator. It’s time to look at its counterpart - lo:

(`la`): from a o `AR` from aa o `AR` from (a `S` aa) o
(`lo`): into a o -> into a oo -> into a (o `P` oo)

The difference is a symmetry between limits and colimits:

The most basic usage of lo is providing the same argument to many handlers and get back a tuple of results:

is `lo` is: a `AR___` a `P` a

That’s it so far! What woould you like to see next? Maybe adjoint functors?

If you want to go deep into this topic I can recommend you to spend some time with these articles:

• Limits and Colimits, Part 1 (Introduction)
• Limits and Colimits, Part 2 (Definitions)
• Limits and Colimits, Part 3 (Examples)