- CT: Category Theory
- FP: Functional Programming (typically meaning more pure functional programming)
- TFP: Total Functional Programming
- TDD: Type Driven Development (e.g. via Idris or Agda)
- TT: Type Theory
- PLT: Programming Language Theory
- CS: Computer Science
Here are my own experiences with study materials related to the field of Category Theory. Your mileage may vary (YMMV). Background: my bachelors degree was in mathematics so I was once familiar with rigorous mathematics, especially proofs, etc but by the time I discovered the utility of Category Theory for my work as a software developer I had already been out of college for over a decade and my rigor level for mathematics had atrophied and needed practice to build up my reasoning muscles again. Practice really is the key to all of this, so it takes time but be patient.
My timeline for learning what I know now with the aim of internalizing understanding so I can more fluidly apply reasoning techniques was not efficient or particularly effective but I think it might benefit seeing where I went wrong:
- 2011-2013: Started using Scalaz at work, learned the definition of a category and functor in a math sense and using concepts like
Functor,Applicative,ValidationNEL,Monoid,Semigroup, etc and vaguely seeing how the software definitions mapped to mathematical concepts but not deeply. I also developed intuitions for what the dreadedMonadwas but got caught up in a lot of FP folklore (my advise is just focus on the fact that these are just abstractions with a precise mathematical definition that abide by certain mathematical laws). Through lots of pain and suffering from production bugs I learned deeply flawed most version of “Future” (and there were many at this time in the Scala ecosystem) were and how it was related to violating laws of common FP abstractions. - late 2013-2015: Bought Pierce’s BCTCS (see below). Flicked through it and realized my mathematical reasoning skills had atrophied significantly. Demotivated by my lack of current rigor, I read only the first four chapters and then left it on the bookshelf for another year. Working as an SRE and then soon after that engineering manager at a toxic workplace that required I work very long hours: I read a couple of papers during this time related to CT, FP, type theory, and reasoning about programs but many were false starts at deeper understanding and I ended up revisiting a lot of this material after I switched jobs.
- mid-2015-2016: I stupidly took a new job in yet another toxic software company yet I read TAPL (see below) - although not thoroughly - and FPS (see below) as well as experimenting with Idris via TDD book and dependent types which helped me flesh out my understanding on CT, how to use types more effectively, and desirable properties of type systems plus general FP techniques which are not entirely coupled yet have a large overlap of research and community.
- since Q3 2016: delving into recursion schemes, reading more papers, attending graduate level courses (MGS), and attending ICFP sessions and workshops. Concepts from CT that I developed a deeper understanding of during this time were: limits, colimits, algebras, coalgebras, adjunctions, natural transformations. I still have a lot more to understand and cover but I do find myself identifying categorical patterns seen in the wild much more than I used to. A better understanding of lambda calculus allowed me to grok
Fixand how that eliminates recursion on the data structure level by relating the same idea from the term-level in lambda calcululs (keywords: self-application, y-combinator, omega-combinator). A basic but more formal understanding of lambda calculus came from a course taken from Capretta at Midland Graduate School in April 2018.
Learning academic material in my 30s after a decade of professional experience - thinking that was all behind me - taught me a few things about how ineffective my learning attitudes and practices were as an adult. Below is a list of things I wish I knew when I started this journey in 2011:
- Do more practice of the material under study. This includes doing exercises from the books, especially in code if possible.
- Take breaks and chunk the study material.
- Read around the topic under study actively seeking out differing perspectives (e.g. a mathematical perspective vs a CS perspective vs a software development perspective).
- Practice, practice, practice!
- Carve out small periods of time each or every other day to study material and revisit the material to make sure you retain it for longer.
- Identify what other topics are related to the current study topic and understand how they are related.
- Sleep between your study sessions on a topic.
- Quiz yourself on the material you have recently encountered and revisit via self-testing until you don’t even pause to answer. You can do this by writing questions for yourself the following day immediately after you have studied some material and/or immediately after listening, watching, or reading make notes in your own words (avoid highlighting as it gives you a false sense of understanding) and if possible convert to executable code or type definitions that type check that demonstrates your recent topic.
- Come up with questions for further research. Add them as TODOs for a new day (some time in the next week) and schedule 15 minutes to find new material to answer your questions. Write notes and/or code to demonstrate the new learning from the research item.
- FPS: Functional Programming in Scala by Chiusano and Bjarnason
- TDDI: Type Driven Development with Idris by Edwin Brady
- TLT: The Little Typer by Friedman and Christiansen
- CTC: Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl
- BCTCS: Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce
- TAPL: Types and Programming Languages (The MIT Press) by Benjamin C. Pierce
A great FP text for the working Scala developer. Introducing a number of important fundamnetal ideas for FP. Some indirect references to CT. Do the exercises. Don’t be passive consuming this material. You will get more out of the material if you do the exercises even the earlier chapters (even if you think you are “above” the earlier chapters; I suffered from this delusion until I reviewed the effectiveness of my learning strategies and rebooted).
Learned a great deal about dependent types which I was a total n00b to at the time of first reading and also exercised my inductive definition muscles through the exercises. Again, work through the exercises, it will improve your understanding if dependent types and type directed programming is interesting to you. I always thought the phrase type-drive or type-directed over emphasized the type specification part while ignoring the huge benefit which is that you get program inference almost for free as long as you specify your program’s type well enough. :)
A fun exploration of dependently typed ideas and concepts through a scheme/Lisp-based language named Pie.
Lots of examples but many of the examples shown are from set/group theory or topological realms of mathematics. The many examples were very useful for me to help me see more deeply some patterns.
Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce (aka BCTCS)
Relatively approachable, good exercises, more directly applicable material for software developers than Riehl’s book.
While not directly related to CT this book does relate to the programming language theory (PLT) which has a large overlap of research activities with applying CT to software development and CS generally.
- Lambda Calculus by Capretta
- Domain Theory and Denotational Semantics by Jung
- Coalgebra by Kurz
- Category Theory by Crole
- Univalent Foundations by Ahrens
TODO
TODO