For the past month, I’ve been following along with the Programming with Categories course at http://brendanfong.com/programmingcats.html (all lectures, notes, assignments available online).
I’m not really able to fully form coherent thoughts about it yet, but curious if anyone else has been following it and might want to discuss the topic here.
I missed this announcement, I’ll start reading along as I have time. I’m always interested in talking about Category Theory in Programming.
I had a long talk with Paul Bone regarding Category Theory and Programming. Our consensus was that Categories are a poor UI/UX for expressing thoughts in programming. However it is extremely important to keep high level programming concepts consistent with, and expressible in Categorical semantics.
The reason for this is that you can be confident that your programming concepts are composable with each other. An example is the async problem in Python, and how asynchronous code tends to infect codebases. I think that Haskell just has better tools to manage the infection due to the Monads.
As a middleware, Categories are fantastic for expressing different Aspects of a system, and compiling to their appropriate representations. This was pointed out by Conal Elliot here. I recommend skipping the paper, and reading the slides for a taste.
I’ll admit that the importance of composition is not something that I’ve really fully appreciated as a programmer until somewhat recently. I mean, it’s been there all along, but it just hasn’t been foremost in my thoughts.
I have watched the entirety of the MIT course now and I feel like I’m left with more questions than answers. I think my big one might be is there any kind of profound/deep result that arises from thinking about categories? For example, I can look at something like lambda calculus and admire it as something truly beautiful and profound about the nature of computation. If there is something analogous to that in category theory, I’m just not seeing what it is–at least not yet. Instead it feels like CT is largely an exercise in naming different kinds of “design patterns” related to functions/relations.
Also, I’m sort of curious whether CT has actually directly inspired the design/development of specific programming languages or programming language features. By that, I mean, something that was created directly by looking at CT first as opposed to having CT applied to it after the fact. In seems like much of CT is so general and so abstract, that it can be applied to almost anything at all. So, it’s little wonder that programming constructs would be described by it.
I don’t mean for these comments to be a criticism by the way. I’ve just never looked at category theory at all before going through this course. I’m genuinely curious about it, but don’t have a good sense for the historical connection between CT and CS.
I think you’ve picked up the right scent.
The most obvious difference to the Categorical Approach to Programming is the encoding of design patterns.
From this approach you can’t misapply a pattern or apply it awkwardly (at least without fighting the compiler kicking and screaming). This gives Novice and Intermediate programmers advance warning that something is going wrong and they might be trying to do the wrong thing.
Compare with Python/Java where design patterns get slathered around indiscriminately.
The Grothendieck Construction is being directly applied to databases to allow for features I’m unaware of any other Database attempting – namely full provenance and versioning of all data in a lossless fashion. I know one is on the market and being used by Amgen.
Twitter: Jules @(_julesh_) gave an overview of Lenses in Programming. Their origin seems to be from a categorical construction proving an incompleteness result using a Categorical Construction. Lenses are now being applied to a wide range of topics that were previously thought to be computationally intractable such as Game Theory, to provide a way of surveying a Computationally tractable branch of the theory.
I’d ask Twitter: Edward Kmett (@kmett) for more. He’s written a large portion of the Haskell ecosystem, and my understanding is that he daydreams in Categories, then writes in Haskell.
Exactly. It does apply to practically everything. And now you can meaningfully relate them using a shared lexicon.
Category Theory encodes in it the specific relationship between broad disciplines. e.g. Functional Programming is fundamentally an Algebraic approach to producing values, whereas Object Oriented code is fundamentally Co-Algebraic and produces states.
Explaining from a naive perspective it is easier to say “they’re different” and stop there.
Speaking in broad strokes from my biased perspective.
Category Theory codifies Analogy.