Does this sound like you? You've learned all you can about object-oriented programming, about functional programming, and about other exotic forms of programming. You're constantly challenging yourself to become a better software developer, to find and pursue new opportunities.
And yet, it feels like there's something out there that they're just not telling you. Some ultimate truth about math, coding, and stuff.
Welcome to the world of category theory. This is the closest you will ever get to a branch of mathematics that you should have learned long ago, that seems to have been kept a secret from you for decades as though there were a giant conspiracy behind preventing you from knowing about it, because that would just make you too powerful.
Category theory provides a fresh view of all of mathematics by providing "maps" of various mathematical fields. Not only that, but it unites distant parts of mathematics using "bridges" that tie together seemingly unrelated concepts. For example, logic and type theory enter into a deep correspondence through the Curry-Howard isomorphism.
In this course, despite the inherent abstractness of the topic, we'll take a fiercely pragmatic approach. Everything will be accompanied by concrete, practical examples, and examined from the viewpoint of executing things in a computing environment. We'll make use of popular languages, such as Java, C#, C++, and Perl — as well as fringe languages, such as Haskell, ML, Agda, Idris and Coq. All in the name of finding ultimate truths.
This course will blow your mind! A bag to collect up the fragments of your mind is not included in the course.
A solid grounding in algebra (but nothing beyond grade school needed, really). Preferably years of programming.
- Just enough universal algebra
- Lots of examples without categories yet
- Objects and morphisms and composition, oh my!
- Diagrams
- Isomorphism
- Duality
- Initial and terminal objects
- Take an arrow to the knee: more about morphisms
- Lots of examples of categories
- Functors
- Covariance and contravariance
- Products and coproducts
- Natural transformations
- Limits and colimits
- Universal constructions
- 2-categories
- Monoidal categories
- Adjoint functors
- Monads
- Hom functors
- Lambda calculus and cartesian closed categories
- Representable functors
- The Yoneda lemma
- Recursion and (guarded) corecursion
- Total programs and infinite loops
- Martin-Löf type theory
- Homotopy type theory
Wow, just found this post. I'm not sure I've seen it before. It seems a good inspiration for a possible course.