How does category theory represent type constructors, higher order functions and typeclasses?

Question

In Haskell programming language, according to https://en.wikibooks.org/wiki/Haskell/Category_theory#Translating_categorical_concepts_into_Haskell

59.2.2 Translating categorical concepts into Haskell

1. We work in the category $Hask$ and its subcategories.

2. Objects are types.

3. Morphisms are functions.

4. Things that take a type and return another type are type constructors.

5. Things that take a function and return another function are higher-order functions.

6. Typeclasses, along with the polymorphism they provide, make a nice way of capturing the fact that in category theory things are often defined over a number of objects at once.

How does category theory represent the things in 4, 5 and 6, specifically,

• Is a type constructor just a function, so does category theory represent a type constructor as a morphism?

• How does category theory represent a higher order function? As special morphisms from or to special objects representing function types?

• How does category theory represent a typeclass? As a subcategory of $Hask$?

Thanks.

Answer 1

I think a more accurate description of what is trying to be said is that:

Hask is a category, but it is not Category Theory.

So "translate category theory into Hask" means only that because Hask is a category you can write down something in category theory and see what it means in Hask. One is not however exploring a model of Category Theory! This example category may have nothing to say about what it means in general categories. By analogy, just because the integers $\mathbb{Z}$ are a group doesn't mean you can do all group theory in $\mathbb{Z}$. In all the blogs and books on the links of category theory with programming languages don't loose sight that they are one example category, not a model of category theory.

For 4. A type constructor (take a type return another type)...this is trying capture the concept like List Int, List String, and so on which gets defined eventually with a generic type like List a where a is the variable. Because these also extend to functions, e.g. a function f:a->b will turn a List a into a List b. This is where your Lisp styled map functions play their role. One often thinks of these as "functors", i.e. a functor from the category Hask back to Hask which sends objects to objects and morphisms to morphisms. And it map preserves composition so it does have that functor like quality.

Notice unlike functors in general, these functors are always endo-functors. In particular it makes it easy to ask for properties like "is this a monad" while also asking if it is a "left adjoint". In general functors $F:\mathcal{A}\to \mathcal{B}$ will have no meaningful "is it a monad" questions until one shows $\mathcal{A}=\mathcal{B}$. But the consequences of the restriction to one category Hask introduces opportunities to expose categorical jargon that would otherwise be nonsense but actually makes sense in this restricted setting.

For 5. "High-order" in logic has a definite meaning (quantifying over relations). In type theory too, at least if one has as usual a hierarchy of universes of types, then higher-order is in reference to types in a universe higher then your present discourse. In computer science higher-order seems now to be given to any function that takes as input or gives as output a function. Category Theory can use "higher-order" in all three of these modes of thought, but the point is "higher-order" is inconsistently applied.

As to @musa-al-hassy point, note that in set theory (and in types) the exponential $X^Y=\{f:Y\to X\}$ is the set of functions $Y\to X$. So a function that takes other functions as input is a function $f:X^Y\to Z$ and a function that outputs functions is a function $f:X\to Y^Z$. That is higher-order in the computer science lingo but nothing about that requires it to be higher-order in the sense of logic. If $X$ and $Y$ are finite sets this function could very well be described in first order logic.

So again, consider the concept as a good introduction but not a mathematical theorem.

For 6. Certainly a subcategory could be modeled by a type class, but it takes some head scratching to decide if you believe type classes always give subcategories and vice-versa. For example, if you impose a type class it is clear it restricts the types, i.e. the "objects" in the category. What is less clear is to what extent we intend to restrict the functions (morphisms). If we take the full subcategory then f:a->b need not respect the type class's intentions. E.g. adding a type class that insists a has an addition, and likewise b, doesn't force f to be a homomorphism of addition. That would be a type constraint on f which is not easily done in Hask (or in type systems in general -- how do you enforce the homomorphism property without an extensional type system?).

So yes, any subset of types induces a subcategory, e.g. the full subcategory, but in the spirit of "subcategory", if I insist I only want types that have a + then I probably also expect all my morphisms to do something accurate with the +, like be a homomorphism. To that extent, no type classes do not model subcategories. It will be the responsibility of the Haskell programmer to add this as a untestable external criteria, perhaps well documented and property tested, but not type checked.

The exception here might be made if one adds singleton types and dependent types to Hask through various packages. Then one might in some special cases insert type checkable proofs of axioms of a type class and thus elevate them to subcategories in the sense one is likely expecting.

---

To actually model category theory, for example if you want the terms of a type to be objects, rather than types being the objects, you need more than Haskell (which is Girard's System F). Some aspects of category theory need a better type theory than that, something like UTT as found in Agda or Coq or Idris.

If you are serious about working with a category try looking at some of the research level languages Agda/Coq or for older stuff http://www.cs.man.ac.uk/~david/categories/