Studying maths on the side
I have been dabbling with category theory for a while, but I'm actually still unsure about really “studying maths” and how serious I want to be about it.
I don't deal much with applied mathematics. I don't need algebra for geometry, calculus for modeling, or advanced statistics for data analysis. I want better abstractions for refactoring legacy code and robust systems programming.
I'm interested in the insights abstract mathematics gives me regarding my programming. Yet, I understand that to fully realize those insights, I need to study mathematics the way mathematics wants to be studied: I need to be more careful and intentional about it.
Working through books
I now have a fair amount of “proper” mathematics books to study, but only a few hours per week that I want to dedicate to it (I have an open-source side-project I'm excited about, and a book and a blog to write)..
The books are:
– Aluffi's Algebra Chapter 0
– the more popularized but still rigorous Seven Sketches in Compositionality
– Awodey's Category Theory
These along with more “informal” material like:
– Category for programmers by Bartosz Milewski, both the book and the lectures
– Programming with Categories, the online lecture by Fong, Spivak and Milewski
– Various functional programming and Haskell meetup recordings
I want to a least follow the proofs in the first set of books—maybe do some proof sketches. I feel that actually doing proofs only maintains interest enough if I can cross-check them with other people. Studying rigorously needs community. I'm not really a puzzle guy—I'm way too impatient.
One way to potentially make proof work more relevant (fun!) for me might be to look into theorem provers. I am afraid of the steep learning curve of doing computer proofs in fields that I am not acquainted with. I had reasonable success going through programming language theory coq tutorials; yet I would often hit a wall where I was unsure if I understood the theory, and was just struggling with the theorem prover, or if I had the theory wrong (even though I was familiar with the field, both on a theoretical and practical level).
Keeping track of my progress and insights in blogs
A fruitful way to solidify my progress, as messy as it might be, is going to be to write about my insights after each study session in this blog. I will be often wrong, and often messy—basically, I will publicly show that I have no clue about what I'm talking about. This always holds me back on my main blog, because I know it gets a fair amount of scrutiny and I am quite sensitive to criticism. I only want to talk about stuff I can back up confidently (sadly I only feel confident about a very few things, mainly that I am thinking my own thoughts.)
In these blog posts, it will become apparent I barely know what a set is, and have to go back to definitions every couple of minutes. One thing I realized however is that this lack of rigor doesn't necessarily make the insights less valuable. After all, I'm not a mathematician, I'm a programmer, and overall my software seems to work well enough. So what if I use fancy words wrong to actually get the work done? The best I can do is work at using them correctly more often.
Extracting value out of theoretical texts
I find that I get the most important ideas out of the very first lines of the introductory chapters. The motivation for a field of study is often what needs to stick because the theory will be forgotten soon enough; working through the theory in detail is however a good way to make the motivation stick. A Zettelkasten is a hack to make the insight retrievable without having to internalize it.
Mathematical texts are often devoid of motivation that I can relate to. I am starting to understand how to take abstract structures and start mining my knowledge (design patterns, applications, domains, programming languages theory) to see if I can something to relate it to. Structures like monoids can be easily found where they obviously relate to mathematical operations, but I am now trying to think out of the box. Can a UI be a monoid? Is there a monoid in handling database connection failures? Do errors form a category? Often, these bring up nothing—even then, I know I need to come back to them once I learn more theory.
For example, I am trying to understand what limits and colimits are about. What are they trying to tell me, why do people study them, and what use do they derive out of it? Can I come up with my own?
Seven Sketches Chapter 1 – Generative Effects
A valuable insight (which I capture in Zettelkasten notes) comes right at the beginning. They talk about generative effects. If I understand it correctly, if we have a system with a compositional structure (for example, virus transmission), it is possible to observe it partially (the observation doesn't conserve the operation of transmission) and end up with seemingly surprising results.
For example, we might observe that individual A had contact with individual B in a certain county and that individual B had contact with individual C in another. In each county, we didn't observe A having had direct or indirect contact with C. But putting both county observations, we clearly see that A had contact with B had contact with C.
This is something that comes up over and over again, for example, partial logs, in my day-to-day job. It applies literally everywhere, it's nothing special per se, but I now know that this has been studied in detail at a very high level of abstraction. This will allow me to group any “partial observation” pattern I can infer from my work into the same mental box.
Now, how is this related to the rest of the chapter? Ordering, partitions of sets, equivalence relations, monotone maps, meets, and joins? I will have to work that out. It will I'm sure shed light on parts of logging and observability I often struggle with: what IDs are assigned to what log, how and where do I store individual entries, what do I do with structured data and how do I index it, how do I fill in or indicate missing data, and how do I ultimately process reports. Ad-hoc approaches often work, but they take effort, and I never feel confident about having covered my bases.
I used to have the same issues with things like concurrency, but by getting more closely acquainted with monads and monoids, I now feel that that is a “solved” problem for me.
Another area I feel better knowledge of ordered sets and monotone maps will help is the startup and termination of concurrent processes. Feel free to call me out in a couple of weeks if I don't circle back on this.