Functional Programming and Category Theory

I'm a math Ph.D. having done research in Algebraic Geometry and Algebraic Topology in grad school for my thesis and I've studied a fair amount of category theory in the process (e.g. having worked through most of "Categories for the Working Mathematician" as well as more specialized topics in Homological Algebra). Is there some good intro to functional programming that emphasizes the link with category theory in the process?

Context: In my workplace I've run into people that are into functional programming and like throwing around category theory jargon, but when you ask for details they typically fail to even be able to define what a category is. I'm hoping that there's more to it in programming than just abstract nonsense. In other words, for someone who actually knows category theory and has done some functional style programming (immutable classes, map, filter, reduce etc.) in imperative languages is there a good intro to FP in the context of category theory?

• Category Theory for Programmers is an introduction to category theory for programmers, but it could work well in the other direction too, as Bartosz explains many of the examples with examples from programming language (primarily Haskell). This could be a good place to start. Jun 21, 2020 at 16:37

These colleagues of yours, would they happen to be Haskell aficionados? They might have told you that Hask was a category made from Haskell, but that is a lie, notheless a very useful one that inspires new programming techniques.

If you would like to find out how category theory informs functional programming, I can recommend Bartosz Milewski's Category theory for programmers.

There is also the older Category theory for computer science by Michael Barr and Charless Wells, which is more of a straight introduction to category theory. It might be a good book for functional programmers who only ever learned the bastardized category theory through functional programming.

Category theory is useful only in a few places in functional programming:

• Implementing libraries that work with arbitrary type constructors. Category theory is good for this kind of highly abstract code. For example, one can define a product of arbitrary endofunctors, a co-product of arbitrary endofunctors, etc., in a library.

• Implementing certain advanced idioms of functional programming, such as "free monad", "optics", "Church encoding of initial algebras". Category theory is a good language for designing such idioms and proving their properties. See, for example, papers about "profunctor optics" or Wadler's "recursive types for free".

• Formulating laws for new typeclasses, such as "filterable", or for combining typeclasses, such as "monad and filterable and applicative and monoid at the same time". Without category theory, the typeclass laws appear to be chosen at random. Category theory provides good intuition and assurance that the laws are chosen correctly and consistently.

• Proving certain general properties that apply at once to all type constructors, or to all typeclasses, etc. For example, the product of two semigroups is a semigroup, the product of two monoids is a monoid, the product of two functors is a functor, the product of two monads is a monad, the product of two applicative functors is applicative, the product of two pointed functors is pointed, the product of two contravariant functors is contravariant, the product of two filterable functors is filterable, etc. All these examples are particular cases of a general theorem (the product of two typeclasses is again an instance of the same typeclass) that applies to many typeclasses at once. Category theory helps to formulate and prove that theorem using the language of F-algebras and F-algebra morphisms.

Other than that, category theory as such is not directly useful for programming. One can (and should) learn functional programming on its own, in its practical aspects, and category theory is not useful for that.

Category theory is also not useful for answering most of the theoretical questions directly related to practical programming. For example, if you want to prove that a given data type is a lawful monad or a lawful applicative functor, etc., category theory will not be directly helpful. You will need to use proof techniques specifically adapted to functional programming.

I recorded a talk: https://youtu.be/Zau8CxsfxOo with the title "What did category theory ever did for us (functional programmers)" where I gave examples in Scala for specific programming questions where category theory helps to get some answers.

Summary:

• Functional programmers do not require category theory in order to master the main features and design patterns that FP uses to write better code. For example, one can (and should) first learn how to use monads, functors, pattern matching, recursive algebraic data types, map/filter/fold, etc., in a concrete programming language with specific examples. Category theory will not help master these techniques even though the words "functor" and "monad" originally come from category theory.
• At a certain point, programmers will see examples of typeclasses with laws, and understand why those laws are important in practice.
• There will be lots of different laws. To make some order and system among those laws, we can formulate the laws as a generalized "lifting" type signature with "twisted" function types. At this point, it will be useful to write down the definitions that generalize all the examples. Those will be the definitions of category, morphisms, and functors.
• We can then use the definitions of category and functor as generalizations that cover the laws of functors, contrafunctors, filterable functors, filterable contrafunctors, monads, applicative functors, applicative contrafunctors, comonads, and perhaps other type classes.
• I show some examples of categories that are used to describe functors, monads, applicatives, and filterable functors.
• I cover filterable functors in more detail, with backdrop of category theory, because filterable functors are rarely explained as a separate typeclass.
• Another example where category theory is useful: "type constructor libraries", i.e. libraries with functions parameterized by a type constructor. Examples of these are free functor / free monad / etc., and Church encoding of types (including recursive type constructors, e.g. the Church encoding of a free monad). Programmers who need to implement these libraries will need to understand how these constructions are defined and what laws need to hold. Category theory provides some limited guidance about that.
• Conclusion 1: programmers need to learn functional programming and not category theory. The special knowledge required in functional programming (e.g., how to implement and use a free applicative functor in your programming language) is not going to be covered by any book in category theory.
• Conclusion 2: basic definitions of category theory (category, functor, natural transformation) are useful as condensed formulations of general laws for a number of typeclasses. Unless a programmer has experience dealing with all the different laws of those typeclasses, it is unlikely that an appreciation of category theory will be of much help. Even for advanced programmers who are working with high-level type constructor libraries, a study of category theory is unlikely to be of any use beyond a few basic concepts and definitions (category, functor, natural transformation, monoid, initial object, Yoneda identities, F-algebra).
• Conclusion 3: knowledge of category theory will not help us derive or prove laws for specific typeclasses, and will not help us implement those typeclasses correctly in code. The reason is that category theory is so general that it only talks about laws that apply generally to a large number of very different typeclasses (functor, monad, filterable functor, applicative functor, pointed functor, contravariant functor, etc.). For practical coding, e.g. to verify that our implementation of a specific monad is lawful, we need to learn not category theory but the techniques of symbolic derivation and proof.

I am writing a new free textbook ("Science of Functional Programming", https://github.com/winitzki/sofp) to develop and explain these techniques with practical programmers in mind. My book is going to be very light on category theory, and I'm not going to use any advanced abstract concepts unless there is a significant gain for practical work. Having written down several hundred step-by-step proofs, I have found what derivation techniques are useful and what definitions from category theory are helpful when proving the theoretical properties of practically relevant code.

Examples of category theory knowledge that has, so far, proved to be unnecessary and not useful:

• monad is a monoid in the category of endofunctors