
Applied Category Theory (2019) [video] - Kinrany
https://www.youtube.com/watch?v=iwvl0tBJhoM
======
jmount
Unfortunately in mathematics "application" is often a synonym for "prove a
lemma or theorem."

David Spivak told me Peter Freyd once said, “Perhaps the purpose of
categorical algebra is to show that which is trivial is trivially trivial.”

This will only work for those who already find category theory trivial (a hard
thing, as it is so general) and the target domain novel (so they are not yet
confident what is trivial and non-trivial in that domain). If done wrong it
can look like the art of making the easy hard.

One good use of category theory is: admitting there are composition patterns
other than function composition. For example: in scikit learn the
fit_transform interface has composition. When you wire up compatible classes
in a pipeline they lash together the fit, transform, and fit_tranform methods
in a simultaneously useful and consistent manner. With category theory you can
say this is a nice form of composition, even though it is not mere composition
of functions.

Another idea that can be made clearer is: separating a function's identity
from its action. This lets us claim code optimizations are correct. That is f1
:= x -> 2.0 x can be thought of as doubling every real number. Now for real
numbers (unfortunately not for mere floating point numbers!) we have an
inverse f2 := x -> x/2.0. Under a very narrow view of composition we might
force f1(f2(x)) to be realized by code such as 2.0(x/2.0). If we think of
composition as different than action, we might say f1(f2(x)) is just x (though
again, this is true over the real numbers- not over the floating point
numbers).

------
ssivark
The concepts are intuitive enough, and make sense. But I don’t see what non-
trivial insights this gives us.

I found the talk frustratingly vague. After all the hard work of setting up
categories/operads in an example, the talk moved on without using them to do
anything interesting.

~~~
lidHanteyk
Here is one non-trivial insight: Every formal logic corresponds to a category.

When we do logical deduction, we have facts and rules. We can apply rules to
facts to get more facts. More specifically, formal logic is built from
situations where we have some fact P, some rule P => Q, and some conclusion Q.

In a category, we have objects and arrows. We can imagine arrows as mapping
one object to another, or sending one object to another. We might have objects
P and Q, and an arrow f : P -> Q relating them.

The connection continues. We can take multiple rules in logic and apply them
sequentially, building a proof tree; we can take multiple arrows in a category
and compose them sequentially, building a _path_. In some logics, there is an
idea of ex falso quodlibet, or from the false fact, anything can be proven;
similarly, in some categories, there are _initial objects_ , which come with
arrows from the initial object to every other object.

Just like how logical formalism eventually removed the possibility that logic
is non-mathematical, category theory removes the possibility that logic is
unstructured. Logic is actually incredibly highly structured, and those
structures happen to coincide with structures in other parts of maths and
physics.

~~~
jiggawatts
Again though, how do I _use_ this to solve everyday problems?

I've seen some vaguely cool stuff done with Category theory in Haskell, e.g.:
composable tree parsing and traversal, but I've never seen anyone actually use
any of this stuff to make a deliverable piece of software that is notably
better than what developers can readily produce using traditional procedural
languages.

I mean sure, I suppose it would be nice if the C# team added some sort of
category theoretically "pure" tree processing sub-language akin to some
bastard child of LINQ and XSLT, but... meh. I don't think it would see a lot
of use in practice.

~~~
lidHanteyk
A few months ago, while employed at a shop, I wrote about a hundred lines of
Python which performed a basic katamorphism on some XML, outputting a PNG.
Nobody else on my team could conceive of this, and were mystified by the fact
that I could just sit down and do this. It wasn't too hard, though, because I
could imagine the entire katamorphism in my mind.

The traditional approaches weren't just stymied by this problem, BTW; the
other developers wanted to go shopping for off-the-shelf components which
transform XML to PNG, as if that would get us the specific katamorphism we
desired.

The nature of your everyday work will inform what you can do with category
theory. I personally use category theory to design programming languages; it's
something for which category theory gives a turn-the-key recipe:

* Pick some objects of interest

* Define a relatively free Cartesian closed category whose objects include your objects of interest

* Enrich the category with interesting arrows

* Extract a combinator basis

The MarshallB programming language [0] is a good example of this recipe in
action.

[0]
[https://dl.acm.org/doi/10.1145/3341703](https://dl.acm.org/doi/10.1145/3341703)

~~~
auggierose
But the real interesting part here is the use of exact real arithmetic, not
the category theoretic part. Category theory is just used as scaffolding. I
would also say it is dangerous to see things only through the category-
theoretic lens, because no doubt, as with any generalisation, there will be
plenty of situations where it does not provide the right generalisation.

~~~
lidHanteyk
Better scaffolding leads to bigger, better buildings. Don't knock the
auxiliary and ancillary techniques; they're still necessary for this sort of
work to be understandable.

Also, from my perspective, the exact real arithmetic isn't super-interesting
because it's not new; Turing was doing this sort of thing when he first got
access to computers. Legend has that one of Turing's first recreational
programs was computation of zeros of the Riemann zeta function, and ever
since, there's been a tradition of exploring exact real arithmetic with
computers and programming languages. MarshallB is one more incremental step
forward in a big research programme of overcoming the inconvenient fact that
we can't test real numbers for interesting properties with computers alone.

At no point have I advocated _only_ category theory. Categories are always
composed of some collection of arrows (and objects, but I prefer object-free
presentations!), and those arrows are always homogeneous, if not homoousios,
composed of a single substance. We can study that substance on its own.
Perhaps an analogy to materials science would be appropriate. We ought to
study both each building material, be it sets, vector spaces, relations,
graphs, or type theories; but also the architectural principles used to make
buildings, like abstract algebra and category theory.

~~~
auggierose
Yes, nothing against better scaffolding, as long as you recognise it for what
it is. Arguably exact real arithmetic is older than inexact real arithmetic
;-) But that's not the point, I think the point is that it becomes interesting
now to actually do computations with it. It helped me program solid modelling
operations for triangle meshes, when I was despairing doing it with normal
floats. Switching to exact real arithmetic allowed me to see things clearer,
and once I had what I wanted running with exact real arithmetic, I could
switch back to floats to make it faster.

------
dang
Url changed from [http://lambda-the-ultimate.org/node/5581](http://lambda-the-
ultimate.org/node/5581), which points to this.

~~~
Kinrany
I initially decided against posting the video because the thread has a small
amount of discussion.

Mainly the link to related work: Seven Sketches in Compositionality,
[https://arxiv.org/abs/1803.05316](https://arxiv.org/abs/1803.05316)

Edit: previously on HN:
[https://news.ycombinator.com/item?id=20376325](https://news.ycombinator.com/item?id=20376325)

