Hacker News new | past | comments | ask | show | jobs | submit login
Category Theory in Programming (racket-lang.org)
161 points by todsacerdoti 34 days ago | hide | past | favorite | 72 comments



I'm seeing a lot of commentary that basically complains that category theory isn't useful. Like most topics in programming, it's useful for some things and not others, so YMMV. The parts of the programming discipline that are truly useful to all programmers are pretty much all learned at the beginning of one's career, or are really difficult to teach and must be learned by participating over time. The fact that you haven't found something useful doesn't mean it's useless in general, since it could just be too specialized to apply to your domain.

As a professional programmer, I personally can say that I have found category theory to be at least occasionally useful in my work, and for me it was worth knowing for that. But I've also studied a lot of math, so it wasn't a big leap out of my comfort zone to learn about it. Like I said, YMMV.


This is a phony work in progress (I do not mean to disparage the author, just the work itself, or perhaps the YC submission). There's no direction, it's just "let's do it because ... ?" Here is the authors' answer to "Why Category theory?":

>The answer lies in the abstraction and generalization capabilities provided by category theory. It allows us to see beyond the specifics of a particular programming language, problem, or system, revealing the underlying structures that are common across different domains

Rest assured you will not find much of that by reading category theory (CT). This type of studying of CT reminds me of Shaolin monks trying to fight boxers (hint: the boxer wins).

Another peculiar thing about these notes is that the author colored every CT diagram (and worse even, there is no logic to the color choices, it's just randomized.)

CT is a nice subject as any other, and useful to those doing research. You don't need it if you're not doing specific math/CS research that uses it. Anything that could be useful to you from CT can be explained in one afternoon over some coffee or beer. For example, the notion of universality could be useful to many programmers: the "most general" object of its kind, and how that is reflected in relation to other objects of its kind; a brief example would be that the "free" language of all strings in the letters A and B is universal amongst all languages of strings A, B with relations, (relations such as AAAB = A.)

Don't enter turbulent waters if you're not a swimmer! Maybe you can take a boat instead. For those who already know CT because of other motivations (in particular, because they're mathematicians who have spent many years studying mathematics), the applications of CT to computer science can come somewhat naturally, but for others, it's an uphill battle and a waste of time.


IMO Bartosz Milewski gave a pretty good answer to the "why" question in the preface to his book:

> Second, there are many different kinds of math, and they appeal to different audiences. You might be allergic to calculus or algebra, but it doesn’t mean you won’t enjoy category theory. I would go as far as to argue that category theory is the kind of math that is particularly well suited for the minds of programmers. That’s because category theory — rather than dealing with particulars — deals with structure. It deals with the kind of structure that makes programs composable.

Composition is at the very root of category theory — it’s part of the definition of the category itself. And I will argue strongly that composition is the essence of programming. We’ve been composing things forever, long before some great engineer came up with the idea of a subroutine. Some time ago the principles of structured programming revolutionized programming because they made blocks of code composable. Then came object oriented programming, which is all about composing objects. Functional programming is not only about composing functions and algebraic data structures — it makes concurrency composable — something that’s virtually impossible with other programming paradigms.

https://bartoszmilewski.com/2014/10/28/category-theory-for-p...

And regarding:

> Anything that could be useful to you from CT can be explained in one afternoon over some coffee or beer.

Yes, you can go through the definitions, but you won't understand all of those concepts in one afternoon unless you're a savant.


During an afternoon someone who understands the concepts can explain the relevant parts without requiring an understanding of CT from the other party. Hence: don't bother with CT.

I don't mean to be rude, but what has Bartosz Milewski done that is relevant in programming?


> I would go as far as to argue that category theory is the kind of math that is particularly well suited for the minds of programmers. That’s because category theory — rather than dealing with particulars — deals with structure. It deals with the kind of structure that makes programs composable.

I would argue this shows that Bartosz Milewski has no idea what programmers actually do. Programming is all about the particulars. Programmers are the ones who have to think about and ask "but what if the person's last name in their country of birth includes characters which our OCR system can't reliably discriminate" or "but what if an attacker sends us a small UDP packet with a spoofed source IP, will we send a lot of data to that IP and spam them?".

Programming is very, very rarely about abstract structure. We programmers are the ones who have to handle of the myriad nitty gritty details of abstract ideals, not the other way around. Sure, sometimes a nice abstract library can solve certain simple recurring problems. But that is a minute minority of all programming work. And if you don't enjoy getting your hands dirty and finding out how many pixels actually fit on the screen, or what exactly happens to bit 15 of the output register when bits 5 and 7 of the control register are set and the input signal is larger than 1024, then you won't last long in the profession.


Yes. The 'purity' of math versus the 'messy reality' of the real world.

Sure, programmers deal with more stuff, like formatting a date/time.

The argument would be that if you follow some of the ideas in composability, then it makes dealing with the real world easier.

Like defining your structure in a way that you don't get 'leaky abstractions' when dealing with the real world.

Just because programmers have to deal with mess, doesn't mean you can't spend some time learning how to organize to minimize mess.

It sounds like you are arguing against studying architecture.


I'm not, not at all. I'm just pointing out that programmers are people who learn to, and like to, delve into the details. Architecture is fun, but it's a tiny part of the job, ultimately.

The biggest part of a programming job is pinning down the details of your requirements.


Your own words betray you.

Pinning down the details of your requirements is _exactly_ the act of choosing the correct level of abstraction. When picking out what matters for correct behavior, and what doesn't, you are defining an abstraction.


Sure, but abstraction is not in any way the same thing as architecture (which is what you were talking about), and it's not structure (which Bartosz Milewski was talking about).

And besides, Category Theory is mostly concerned with finding similarities between different mathematical objects, when you look at them abstractly and ignore some details. It helps you find that numbers with adding are homomorphic to functions with composition. But programming is about telling a computer how to actually add 156 with 1571 by adding bit to bit, and how to compute the composition of two functions by computing the result of the first and putting it in a register so the second one can take it as input, which CT doesn't concern itself and no category theorist cares about in the slightest.


> programming is about telling a computer how to actually add 156 with 1571 by adding bit to bit

programming can also be about producing generic solutions that commit to some minimal set of assumptions so that solutions work across a variety of contexts, e.g. regardless of whether your data is floats or ints.

sometimes good engineering is about finding decisions you can avoid making or thinking about. Sometimes you have to decide how to add the numbers bit by bit, but for that particular example, it's even better to not care about how the numbers are added up (which is a detail of the CPU or a bignum library or whatever).


The section on "Mapping Category to Programming" seems to totally miss the point of how category theory is actually relevant in programming. Functors, applicatives, and monads are category theory concepts that are particularly useful in programming, but they aren't even mentioned here.

Category theory is way more abstract than programming, so the truth is that you don't need to know what these concepts mean in category theory; just understand them as programming concepts to start with. For example, monoids are ubiquitous in programming, but the category theory view of a monoid as a one-object category is too abstract to be helpful. Instead, it's much more useful to just think of a monoid as a set equipped with an associative binary operation and an identity element. Then you can easily see that strings, list, and numbers (with their applicable operations) are all monoids.


> the category theory view of a monoid as a one-object category is too abstract to be helpful

That’s not true at all! It goes to the essence of what it means for a thing to be foldable unto itself, ie.: the things that you can reduce() or fold().

There’s an entire paradigm of data processing where all you do is map-and-reduce, so there’s something very important and practical there.


Sure, but my point is just that the category theory view of a monoid is harder for most people to understand.

For example, it's easy to see that integer addition is an operation that combines two elements of the set "Integer" into another element of the same set. E.g. 1 + 2 = 3. From there, it's a small step to seeing the same pattern elsewhere, and recognizing it as the "monoid" pattern. E.g. "foo" + "bar" = "foobar" for string concatenation.

In category theory, one instead has to think of this as the composition of two morphisms being equivalent to another morphism. E.g. +2 ∘ +1 = +3. That is much less intuitive for most people, I think.

I have nothing against category theory. It is very powerful precisely because it is so abstract. But if you want to learn how to apply the relevant concepts to programming, that abstraction is often more of an obstacle than a help.


I hear what you’re saying, but I don’t see any of this as standing in the way of programming.

Effort and curiosity and learning are where skills and understanding come from.


Isn't CT much about higher-order parameterized type-signatures of a set of "classes" that can usefully work and be combined with each other?

Then instead of grokking the CT and its theorems as a whole it would seem to be useful to learn about such type-signatures among a set of collaborating (OOP-like) classes which are useful for many programming tasks?

In a sense categories then could be seen as formalization of "Design Patterns"?

Something like that?


I was going to say “not at all”… But not really, no.


If you have a compositional system, such as a programming language, you can use category theory to predict its behavior, in the same way that if you have a symmetric system, such as particles in a box, you can predict its behavior. In the former, maybe you prove that your programming language "can't go wrong"; in the latter, maybe you prove your physical system "conserves energy". (Or, do both at once: https://conferences.inf.ed.ac.uk/clapscotland/atkey.pdf). In any case, the point of category theory is to model compositional systems, which may or may not be worthwhile in any given context.


It is all about functor, and functions between them. So what is functor for ?


In computer science, we can squint and claim that a functor is just something that has a .map function, taking a function. Option, Promise, List... all functors.

The fact that functor is a concept, and follows specific laws, allows us to have other abstractions that work across all functors without having to repeat ourselves over and over again. See, for instance, Scala's for comprehension. it offers different iterating capabilities over basically anything, and it will give you more capabilities if instead of just functor, you pass a monad, or something that supports .filter.

Also see the possibilities of generic transformations. Every language that supports Promise needs some way to turn a list of Promises into a Promise holding a list, and vice versa. We can do this with options, or Eithers, or some home-made thing that is holding on to any other property we like... but it's so much easier to do so without having to write every possible combination of two things, and rely on the fact that one might be a monoid, or a monad, and not have to write all the boilerplate.

In languages that take this very seriously, you can do things like, say, apply a tracing library to an http request, or a logger, or manage creation of resources, all throught category theory concepts, and have all the wiring basically disappear, instead of havign to either pass a million parameters, or relying on some dubious Aspect-oriented-programming instrumentation that might or might not work. All visible, and checkable at compile time. And you get there by making all your abstractions are functors, monoids, monads and such.


Went through the table of contents and it seems to be more of understanding CT than applying it to day to day programming tasks?

I’d have liked to see them start with something concrete in coding and show how CT makes it easier. Instead they dive headlong into CT.


Category theory is just another way of looking at math besides the impoverished notion "everything is a set". Mathematics is used in computer science. Rust is a great example. Jean-Yves Girard invented linear logic to make Gerhard Gentzen's sequent calculus symmetric, similar to Paul Dirac's theory that led to the discovery of positrons. Girard's concern about using a proposition exactly once in a proof led to borrow checking.

Putting on category theory glasses can help discover and clarify new facts. Thinking in terms of objects and arrows leads to duality: reverse the direction of the arrows.

The category Set is only one of many categories. The objects are sets and the arrows are functions. A function I -> S that is 1-1/injective/mono[1] corresponds to the set theory notion of a "subset". The dual is a function S -> I that is onto/surjective/epi[2]. What set theory notion does this correspond to?

Hint: Look into David Ellerman. He is the von Neumann of our times.

[1] f is mono if fg = fh implies g = h. [2] f is epi if gf = hf implies g = h.

Hi Dang.


I've gone down this rabbit hole a few times, and I always return pissed off and a dozen hours poorer. Maybe someday I'll get it.


The main problem is that category theorists keep writing stuff claiming that, if only you get through the math, you'll eventually be able to apply the category theory to typical everyday programming problems. And by the time they get to the Yoneda lemma or whatever, they've forgotten they're supposed to show some applications. All they show is how to express category theoretical concepts in a program. And it is mostly because the demonstrated applications are few (I have spent a lot of time looking and have found little convincing evidence).

Having learned the subject myself, I'm not convinced it's useful for programmers. Hell, it's not even useful for all areas of mathematics, and that is its raison d'etre.


I often go back to this post by John D Cook. Quote below: https://www.johndcook.com/blog/applied-category-theory/

    Category theory can be very useful, but you don’t use it the same way you use other kinds of math. You can apply optimization theory, for example, by noticing that a problem has a certain form, and therefore a certain algorithm will converge to a solution. Applications of category theory are usually more subtle. You’re not likely to quote some theorem from category theory that finishes off a problem the way the selecting an optimization algorithm does.

    I had been skeptical of applications of category theory, and to some extent I still am. Many reported applications of category theory aren’t that applied, and they’re not so much applications as post hoc glosses.

    At the same time, I’ve seen real applications of categories, such as the design of LINQ mentioned above. I’ve been a part of projects where we used category theory to guide mathematical modeling and software development. Category theory can spot inconsistencies and errors similar to the way dimensional analysis does in engineering, or type checking in software development. It can help you ask the right questions. It can guide you to including the right things, and leaving the right things out.

Category theory in LINQ

https://queue.acm.org/detail.cfm?id=2024658


This two-part keynote might give you a good flavour:

* https://www.youtube.com/watch?v=4WMfKhKKVN4

* https://www.youtube.com/watch?v=zooYfk5-yPY

If you can stand up a Cartesian-closed category, it is a model of a lambda calculus. So you can make a compiler plugin that takes lambda terms (a large subset of Haskell) and compiles it into all sorts of exotic settings (dataflow diagrams, derivatives of the function, ...)

KittyHawk used it to compile Haskell to C in https://github.com/sellout/compiling-anything-to-categories and someone talks about their work here: https://www.youtube.com/watch?v=VUBj8NW7uMA


> Having learned the subject myself, I'm not convinced it's useful for programmers.

I think it is demonstrably useful to people who design programming languages with strong type systems. Not a very common use case in practice, but it did find an application. Damned with faint praise, perhaps. I haven't seen anyone demonstrate a use outside that niche.


I've been down that rabbit hole, and while some few select people do it, the vast majority of people doing this rely on PL papers that long preceded the attempt to put category theory in the mix.


What's the application of languages with strong type systems?

Some people do the work of learning category theory and still decide in the end to write lint.


> The main problem is that category theorists keep writing stuff claiming that, if only you get through the math, you'll eventually be able to apply the category theory to typical everyday programming problems.

There is no "typical everyday programming problems." It's an incredibly broad discipline, and one person's typical is another's esoteric.

When you're designing an API, it's useful to know when you're dealing with one of the common structures that occurs in category theory, and there's a somewhat high cost to missing that, since you can end up with a "broken" feeling API where the pieces don't fit together properly, or where the different parts aren't consistent with one another.


I'm interested in reading about the application of Category Theory to API design.


The only practical use I have found for knowing some category theory, is to be able to decode what your FP fanatic colleague is talking about.


It's hard to write something that is both accessible and well-motivated.

The best uses of category theory is when the morphisms are far more exotic than "regular functions". E.g. it would be nice to describe a circuit of live queries (like https://materialize.com/ stuff) with proper caching, joins, etc. Figuring this out is a bit of an open problem.

Haskell's standard library's Monad and stuff are watered down to the point that they are barely category theory, but they are also quite useful and would not have been readily invented without category theory. See even if you have no taste for "abstract nonsense", maybe you can still accept the fact that its left a trail of more accessible "semi-abstract semi-nonsense" in its wake.

This stuff takes time. If it's not your cup of tea, no need to make yourself an early adopter. See also things like Lean where fancy type systems are finally reaching "regular non-CS" mathematicians with great success.


On the pure math side, Locales (https://ncatlab.org/nlab/show/locale) are so much more beautiful an axiomatization scheme than regular topological spaces, even if one is just doing regular classical rather than constructive math. We would have not discovered them except for category theory.


I would also check out https://en.wikipedia.org/wiki/Algebraic_logic#Algebras_as_mo...

The basic (pre-category theory) idea is instead of making up new weird math just for logical purposes, start thinking more abstractly and using "regular" math concepts. The section says "models" but it should work for syntax too not just semantics (the syntax is the "initial" semantics).

Category theory takes all that order/lattice stuff and generalizes it in the same way programming generalizes logic ("whether" true/false to "which" inhabitant of a type). So it is definitely useful for people trying to explore the space of programming language designs.

The reason category theory might be useful to "regular programmers" not programming language designers, basically boils down to the belief that programming and language design are not so different after all. I can't really argue that explicitly, but think "where does designing a library interface end, and designing a domain-specific language being?". That's the basic idea.


> The section says "models" but it should work for syntax too not just semantics (the syntax is the "initial" semantics).

Can you elaborate on that?

Do you mean initial in terms of initial objects? [0]

Is this related to Herbrand universes? [1] (in which we build an interpretation of first order logic where each symbol stands as themselves)

[0] https://en.wikipedia.org/wiki/Initial_and_terminal_objects

[1] https://en.wikipedia.org/wiki/Herbrand_structure


Yes to 0, no idea but don't think so to 1



I was a college math major. Category theory wasn't one of the offered courses at my college, so I didn't study it specifically. But I didn't get through any of my math classes without working the problems and proofs, and without having a teacher to help guide me through the material. It can't be read like a book. At least that's my experience.

And as I get older, being interested in the topic helps more and more.


As a counterexample, I have self-studied queuing theory, extreme value analysis, combinatorics, generalised linear regression, etc. and had no problem with it.

Category theory I just can't get through. Either it does not fit with my brain or I fail to see the practical implications, but something makes it not stick.

(Curiously, differential equations (beyond the basics) are in a similar spot for me, even though they are obviously immediately practical in a huge number of areas!)


This oughtn't be super surprising, even the DE comment at the end - people do just have bits of maths they gel with more than others!

Even so, CT is not easy to motivate without a lot of experience in a few specific areas of maths - it's definitely a very "meta" subject (even though a lot of these blogs pretend it's super applicable to everyday engineering) and is a very different lens from the maths taught up to that point.


This is the only right attitude. Thank you for saying it.


That's such an amazing description of my experience as well. I find the topic inscrutable.


Category theory is a great tool for thinking about programming language design (especially types in functional programming). In some sense that translates to better programming, but there’s a lot more math topics that are likely to be directly applicable day to day.

Do you know how to evaluate a polynomial efficiently? Fit a curve to points? Solve a linear system? What the Fourier transform is for? If no, hold off on the categories.


Is Bézier curves not enough to fit curve to points? Just checking as I am very curious about this problem.


Bézier curves parameterise a curve with points. When people talk about "fitting a curve" I would expect they mean fitting a model rather than that the curve is fully determined by the points. Typically people fit linear or low-order polynomials, it'd be a weird day where someone wanted to use a Bézier for their model - those curves weren't designed for being statistically tractable or interesting.

See https://en.wikipedia.org/wiki/Curve_fitting


To expand upon roenxi's answer: Bezier curves are an example of creating a cubic (degree 3) parametric polynomial curve by using four points to describe where you want it to go.

Curve fitting is about starting with a cloud of points, and trying to decide how to draw a polynomial (of whatever degree you want) that does a good job of describing the trend line of those points.

Then you can use that polynomial to approximately interpolate points between the samples, or extrapolate points beyond the samples as an example.


No. Here are two common and practical kinds of curve fitting:

1. Least squared polynomial fit.

This finds a curve that approximates a set of (x, y) pairs.

2. Polynomial interpolation

This makes a polynomial which goes exactly through the given points.


The answer is obviously no, but I’m not the right person to explain (biochemist).

For some reason you were downvoted down to oblivion, and I think that was unfair.


As a math course, I felt category theory was interesting as a way of unifying ideas across different areas of mathematics. But I never quite seen a value of it for programming (but maybe it's just me)


As primarily an engineer doing maths, with code on the side, I feel the exact same.

It’s been way more of use to me in pulling together parts of topology, linear algebra, geometric algebra, homology et al than discovering furtive programming abstractions.


It's IMO the right setting to talk about logic. That's one of the reasons it unifies ideas in math.

Computer science is mostly an application of logic which is why category theory has become a useful tool in theoretical computer science.


If you're talking about toposes, many logics do not correspond to them. It's the other way around: many category theorists/logicians needed jobs and found computer jobs and hence the category theoretic perspective in CS.


You don't know what you're talking about. Applications of category theory to computer science predate the first US computer science department. There weren't any computer science jobs to speak of.

Categorical logic is larger than elementary topoi. I would wager that you can't name a logic not expressible in category theory.


>Applications of category theory to computer science predate the first US computer science department.

This doesn't sound plausible: according to Wikipedia, Eilenberg and Mac Lane introduced concepts of CT in 1942, and CT was originally used mainly homological algebra, with applications in logic/semantics later. Certainly CT was given credence by Grothendieck and Serre, working on (and solving) Weil's conjecture in the 50s and 60s. Lawvere's 1963 thesis predated categorical logic (according to his own words, <http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html> p. 12, "but the method here, and indeed in the whole ensuing categorical logic, is to exploit the uniqueness by using adjointness itself as an axiom"). The first computer science department in the US was started in 1962 in Purdue University. Meanwhile for contrast the proofs of Church and Turing were published in 1936.

>I would wager that you can't name a logic not expressible in category theory.

I prefaced my statement with an "if"; you're not talking about toposes apparently. The interpretability of one theory in another is a concern of logicians and I'm not familiar with any restrictions on category theory, indeed it can be used for logics. I do not know topos theory but I was basing my statement on what I heard Colin McLarty say in an interview of his <https://www.youtube.com/watch?v=81sPQGIWEfM>, can't give timestamp; he definitely named logics that cannot be expressed by the topos of a space.

I feel that you've used two straw men: 1) specifically naming US 2) ignoring my "if topos" and saying "expressible in CT".


I feel that the main thing that can change it is having a plethora of examples. Also, I think math has much better examples than programming.


Even though I went pretty deep in math/cs in college and worked as a SWE for five years, I never really "got" the connection between category theory and actual practical software problems until I started working on a new project with complex uses of types and functional programming. IMO most programmers are not working on projects like that where category theory is even relevant. And for me even though it was relevant, other than being to identify something by its category theory vocab term, it wasn't really helpful to actually know category theory.

Also, you probably should study axiomatic set theory and abstract algebra before taking on category theory and even in materials like this where they try to bring you up to speed on them, you'll not have had the exposure time to those subjects (or perhaps higher math in general) to understand things well. You'll also skip over stuff like https://en.wikipedia.org/wiki/Multiplicative_group_of_intege... which aren't category theory per se but prime your brain into thinking about the properties of sets, relations within/between sets, and repeatable "structures" across sets.

The other problem I ran into is that most programming languages do not have sophisticated enough type/functional systems to be able to properly implement a lot of fancy stuff where category theory is relevant. For example, even though typescript had all the information necessary to know that class A is abstract and B extends it, or that class C is templatized by types subject to some constraint, it can't at compile time implement a lot of checks that it technically should to handle Functors (https://en.wikipedia.org/wiki/Functor_(functional_programmin...). The languages that do handle these things properly are typically lacking in other ways that made them not worth it (for me) to use - it was better to handle the problem inelegantly in the less sophisticated language.


Exactly. While Category Theory is interesting and the way it can abstract things like the Diagonal argument is very elegant every time I try to learn it I end up feeling I would have been better off learning almost anything else.


There is nothing to “get” that is worth getting unless you are interested in pure math. As a programmer we already know how to compose types/functions/applications/systems. No need for category theory to understand how to do that.


I share this experience.

Perhaps another way of asking the question is: Are there any results, either about individual programs or in PL theory as a whole, that were made simpler / clarified / generalized because of category theoretic insights?


Sure, Haskell's type system (and type systems in general) are informed by categories:

https://en.wikibooks.org/wiki/Haskell/Category_theory

This article is also nice:

https://www.haskellforall.com/2012/08/the-category-design-pa...

It explins how Haskell's monad laws follow directly from how categories work.


Yes, but it's much, muvh faster and more productivr to just learn Haskell's type system (mainly Functors, Monads and Applicatives) as 3 individual "design patterns" than it is to figure it how you can even begin to apply the Yoneda Lemma to whatever programing problem you have in front of you.

Category Theory has birthed some useful abstraction, but you don't really need any of CT to learn and use the abstractions.

The basics of Abstract Algebra on the otherhand are absolutely worth the bit of time it takes to learn them.

Groups, semi-groups, rings, fields, monoids - distribution, identity, zeros, associstivity, communitavity are pretty trivia to learn - most people already know the underlying concepts and they pop up all the time in programing.

Monoids are incredibly useful - most people already know them, and intuitively use them, but it's helpful naming and understanding the pattern.

Category Therory just doesn't have the same return on investment for software development.


There is a very useful perspective in which categories are just typed monoids, and the monoid operation can only be applied when the types "line up". For example, here are some useful operations which do not form a monoid:

- PUSH(n) where n is a floating-point number

- POP

- CLEAR

- ADD, SUB, MUL, DIV

- ID

These can be interpreted as operations on a stack of floating-point numbers in the obvious way, PUSH(1.2) * [3.14] == [1.2, 3.14], POP * [1, 2, 3] == [2, 3], ADD * [1, 2, 5] == [3, 5], CLEAR * [1, 2, 3] == [], ID * [1, 2, 3] == [1, 2, 3], etc. However, not all of the compositions of stack operations are legal. For example, ADD * PUSH(1) * PUSH(2) is fine and equivalent to PUSH(3), but ADD * PUSH(1) * CLEAR is illegal.

Ok, so our stack operations don't form a monoid. But they obviously can still be composed, sometimes, so what do we have if not a monoid? They form a category! There is one object for each natural number, representing the height of the stack. So there are arrows like PUSH(3.14) : Height_{n} -> Height_{n+1} for all n, and POP : Height_{n} -> Height_{n-1} whenever n >= 1, and ADD : Height_{n} -> Height_{n-2} whenever n >= 2.

Another common example is matrices. Square matrices form a monoid, but what about arbitrary rectangular matrices? They don't form a monoid, but they do form a category where the objects are natural numbers, and the arrows N -> M are just the MxN matrices. You can't multiply any two matrices, but if you have a P -> Q matrix (QxP) and a Q -> R (RxQ) matrix then you can multiply them to get a P -> R matrix (RxP).


Monads are a traditional stumbling block for Haskell newbies, including me when I was one. I found that those articles I linked demystified them more than any number of "monad tutorials" ever could do.


Indeed; Haskell is purely functional, and Category Theory is nothing but a purely functional language of mathematics.


Category theory is not “purely functional”, it is about morphisms, and morphisms are more abstract than functions.

Category theory envelopes relations as well, as well as arguably anything else that can be formalized.


But what does that buy you?


The thing about questions like this is that the complexity of mathematical explanations is highly dependent on what each reader considers "simple." Consider two different approaches to understanding a concept, expressed in information-theoretic terms:

  H(concept) + H(existing explanation|concept) 
vs

  H(concept) + H(existing explanation|concept) + H(categorical explanation|existing explanation, concept)
This additional complexity layer of categorical framing has a nonzero cognitive cost, which varies based on the learner's intuitions and background. The investment in learning categorical thinking only becomes worthwhile when the learner can amortize its cost by envisioning its broad applicability - when they can see how categorical frameworks enable systematic problem decomposition and generalization. This implies they've already recognized the limitations and redundancies of non-categorical approaches, understanding intuitively how many concepts would need to be reinvented as the problem evolves within its conceptual framework (gestell).

However, there exists a middle path that often goes unrecognized as categorical thinking, despite embodying its essence. This approach involves incrementally discovering generalizations -- "oh, this can be generalized with this type" or "oh, if I wrap this in another type I can do something else later on" or "oh this syntactic sugar for this particular operator overload feels quite nice"


Yes, there are a number of them. Here are some examples off the top of my head:

- Moggi was studying the problem of equivalence of programs, and noted that the traditional approach to modeling a program as a total function Input -> Output is problematic. He pioneered the use of monads and Kleisli categories as a foundation for reasoning about equivalence of real programs, including all the real-world nastiness like non-termination, partiality (e.g. throwing an exception that kills the program), non-determinism, and so on. https://person.dibris.unige.it/moggi-eugenio/ftp/lics89.pdf

- Linear logic (and it's close relative affine logic) was the inspiration behind Rust's ownership model, from what I understand. Linear logic was originally described in terms of the sequent calculus by Girard (http://girard.perso.math.cnrs.fr/linear.pdf), but later work used certain categories as a model of linear logic (https://ncatlab.org/nlab/files/SeelyLinearLogic.pdf). This answered and clarified a number of questions stemming from Girard's original work.

- Cartesian-closed categories (CCCs) form models of the simply-typed lambda calculus, in the sense that any lambda term can be interpreted as a value in a CCC. Conal Elliott pointed out that this means that a lambda term doesn't have just one natural meaning; it can be given a multitude of meanings by interpreting the same term in different CCCs. He shows how to use this idea to "interpret" a program into a circuit that implements the program. http://conal.net/papers/compiling-to-categories/

- Mokhov, Mitchell, and Jones studied the similarities and differences between real-world build systems and explained them using different kinds of categories. https://www.microsoft.com/en-us/research/uploads/prod/2018/0...

- There is a classical construction about minimizing a DFA due to Brzozowski which is a bit magical. Given a DFA, do the following process twice: (a) get an NFA for the reverse language by reversing all edges in the DFA and swapping start / accept nodes, then (b) drop any nodes which are not reachable from a start node in the NFA. The result will be the minimal DFA that accepts the same language as your original DFA! Bonchi, Bonsangue, Rutten, and Silva analyzed Brzozowski's algorithm from a categorical perspective, which allowed them to give a very clear explanation of why it works along with a novel generalization of Brzozowski's algorithm to other kinds of automata. https://alexandrasilva.org/files/RechabilityObservability.pd...

- I would also put the development of lenses in this list, but they haven't leaked very far outside of the Haskell universe yet so I don't think they are a compelling example. Check back in 5 years perhaps. Here's a blog post describing how lenses relate to jq and xpath: https://chrispenner.ca/posts/traversal-systems

- I've personally had success in finding useful generalizations of existing algorithms by finding a monoid in the algorithm and replacing it with a category, using the fact that categories are like "many-kinded monoids" in some sense. I haven't written any of these cases up yet, so check back in 2 years or so. In any case, they've been useful enough to drive some unique user-facing features.


This comment pairs very well with the recent thread on Heaviside’s operator calculus. He got ahead of theory, did groundbreaking work, and was ultimately superseded by more principled approaches. I think this illustrates a kind of intellectual leapfrog. Sometimes we do things that are right, but it’s not clear why they work, and other times we have theoretical structures that open up new realms of practice.


I just realized I botched the description of Brzozowski's algorithm, step (b) should be "determinize the NFA using the powerset construction". Mea culpa.


Yes?


"In the following chapters, we will explore the core concepts of category theory — objects, morphisms, categories, functors, natural transformations, Yoneda Lemma, 2-categories, (co)limits, sketches, Cartesion closed categories & typed lambda, Curry–Howard–Lambek corresponding, adjunctions, (co)monads, kan-extensions, toposes, and more..."

That'll be a no from me




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: