- 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, liftings, 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 encouter examples of typeclasses with laws, and understand why those laws are important in practice.
- There will be lots of 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.
- 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 thean appreciation of category theory will be of much help. At the same timeEven for programmers 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), any further study of category theory is not likely to be of any use for a practicing functional programmer.
- 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.
- 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, liftings, 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 encouter examples of typeclasses with laws, and understand why those laws are important in practice.
- There will be lots of 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.
- 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 the appreciation of category theory will be of much help. At the same time, beyond a few basic concepts and definitions (category, functor, natural transformation, monoid, initial object, Yoneda identities, F-algebra), any further study of category theory is not likely to be of any use for a practicing functional programmer.
- 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.
- 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, liftings, 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 encouter examples of typeclasses with laws, and understand why those laws are important in practice.
- There will be lots of 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.
- 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 programmers 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.
Most answers on this page are research-oriented. They answer the question: what algebraic structures will help us publish more theoretical papers on computer science. But most of those theoretical papers will not be directly relevant to the work of a software practitioner, even when the programs are written in Haskell or another functional language.
Most frequently, category theory is mentioned as the algebraic structure used in functional programming, so let me comment on that. Category theory has certain but limited use for learning functional programming or in actual practice of functional programming. I recently made a presentation to answer that question. https://www.youtube.com/watch?v=Zau8CxsfxOo
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, liftings, 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 encouter examples of typeclasses with laws, and understand why those laws are important in practice.
- There will be lots of 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.
- 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 the appreciation of category theory will be of much help. At the same time, beyond a few basic concepts and definitions (category, functor, natural transformation, monoid, initial object, Yoneda identities, F-algebra), any further study of category theory is not likely to be of any use for a practicing functional programmer.
- 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
- any monad comes from a pair of adjoint functors
- a free monad comes from the free/forgetful functor adjunction
In contrast, naturality laws are used in about 30% of all proofs, and the functor composition law is also used in around 30% of proofs. This shows the importance of learning the concepts of functor and natural transformation.