A mathematical (categorical) description of type classes

Question

A functional language can be viewed as a category where its objects are types and morphisms functions between them.

How do type classes fit in this model?

I assume we should only consider those implementations that satisfy the constraint that most type-classes have, but that are not expressed in Haskell. For example, we should only consider those implementations of Functor for which fmap id ≡ id and fmap f . fmap g ≡ fmap (f . g).

Or are there any other theoretical foundations for type classes (for example based on typed lambda calculi)?

Answer 1

How do type classes fit in this model?

The short answer is: they don't.

Whenever you introduce coercions, type classes, or other mechanisms for ad-hoc polymorphism into a language, the main design issue you face is coherence.

Basically, you need to ensure that typeclass resolution is deterministic, so that a well-typed program has a single interpretation. For example, if you could give multiple instances for the same type in the same scope, you could potentially write ambiguous programs like this:

class Blah a where
   blah : a -> String 

instance Blah T where
   blah _ = "Hello"

instance Blah T where
   blah _ = "Goodbye"

v :: T = ...

main :: IO ()
main = print (blah v)  -- does this print "Hello" or "Goodbye"?

Depending on the choice of instance the compiler makes, blah v could equal either "Hello" or "Goodbye". Therefore, the meaning of a program would not be completely determined by the syntax of the program, but rather could be influenced by arbitrary choices the compiler makes.

Haskell's solution to this problem is to require that each type has at most one instance for each typeclass. To ensure this, it permits instance declarations only at the top level, and furthermore makes all declarations globally visible. That way, the compiler can always signal an error if an ambiguous instance declaration is made.

However, making declarations globally visible breaks the compositionality of the semantics. What you can do to recover is to give an elaboration semantics for the programming language -- that is, you can show how to translate Haskell programs into a better-behaved, more compositional language.

This actually gives you a way to compile typeclasses, as well -- it's usually called the "evidence translation" or "dictionary-passing transformation" in Haskell circles, and is one of the early stages of most Haskell compilers.

Typeclasses are also a good example of how programming language design differs from pure type theory. Typeclasses are a really awesome language feature, but they're quite ill-behaved from a proof-theoretic point of view. (This is why Agda does not have typeclasses at all, and why Coq makes them part of its heuristic inference infrastructure.)

Answer 2

Here is a categorical description of (certain kinds of) typeclasses. So far, I can fully elaborate this only for simpler typeclasses such as monoids or semigroups, not for type constructor typeclasses (functors, monads, etc.) but the difficulties are just technical.

In brief: A typeclass is an $F$-algebra with additional laws (and one needs to develop machinery to describe the laws explicitly). This covers most typeclasses (monoids, functors, applicative functors, etc.) but some typeclasses are not of that form. Some other typeclasses are $F$-coalgebras, but some typeclasses are neither.

Begin by the definition of $F$-algebra and $F$-algebra morphisms. Let us choose an endofunctor $F$ (in the language of programming, $F$ is a covariant type constructor). A type $T$ is an $F$-algebra if there exists a designated function $\alpha_T: F(T) \to T$. The function $\alpha_T$ is called the structure map of $T$.

An $F$-algebra morphism between $F$-algebras $T$ and $U$ is a function $f: T \to U$ such that the appropriate diagram commutes. See https://en.wikipedia.org/wiki/F-algebra

All $F$-algebras form a category.

Now we call a "lawful $F$-typeclass" any subcategory of $F$-algebras $T$ whose structure maps $\alpha_T$ satisfies (zero or more) additional laws.

A type $T$ belongs to the $F$-typeclass if there exists an evidence value $\alpha_T$ of type $F(T) \to T$. So, the structure map of the $F$-algebra is the evidence value for membership in the typeclass.

For example, the monoid typeclass is described by $F(T) = 1 + T \times T$. The two monoid methods, $e$ and $\oplus$, can be derived from a single function of type $F(T) \to T$.

This example illustrates how the structure map of an $F$-algebra describes at once all the operations of the typeclass.

Now, it is also important that the typeclass laws are described explicitly. This is done via special "law functions" and requires more explanation.

Most often, the typeclass laws have the form of an equation between values of type $T$, where $T$ is the type that belongs to the typeclass. For example, the left identity law of the monoids is $\forall (t:T). \, (e\oplus t)=t$. The two sides of the law are symbolic expressions built from some arbitrary values of type $T$ and the typeclass operations. This motivates the following definition:

A "law function" is a value of type $\forall A. \, (\textrm{Nat} \to A) \times (F(A) \to A) \to A \times A$.

A lawful $F$-typeclass may have zero or more law functions.

A law function takes an arbitrary number of arbitrary values of type $A$, uses the typeclass operations via the evidence value $\alpha_A$, and computes a pair of values of type $A$. Those two values will be the two sides of the law. The law requires them to be equal.

This motivates the following definition of what it means that the evidence value "satisfies a law":

Given a law function $l:\forall A. \, (\textrm{Nat} \to A) \times (F(A) \to A) \to A \times A$, we say that an evidence value $\alpha_T: F(T)\to T$ "satisfies the $l$-law" if, for any $f:\textrm{Nat} \to A$, the value $l(f, \alpha_T)$ is a pair of equal values of type $A$.

So, a type $T$ is an object of the "lawful $F$-typeclass" category if two conditions hold:

1. There exists a designated evidence value $\alpha_T$ of type $F(T) \to T$.
2. The evidence value $\alpha_T$ satisfies the laws corresponding to each of the law functions (if any).

Starting from these definitions, and assuming that relational parametricity can be applied to the law functions, I have proved several interesting results about lawful $F$-typeclasses. Let me list some of those results without proof.

Statement 1. If $f: T\to U$ is an $F$-algebra morphism and the laws of the typeclass hold for $\alpha_T$ then the same laws will also hold for $\alpha_U$. In other words, $F$-algebra morphisms automatically preserve the laws.

Statement 2. If $T$ and $U$ are two objects of a lawful $F$-typeclass category then the product $T\times U$ is also an object of that category; that is, $T \times U$ is again an $F$-algebra and also all laws will hold for $T \times U$. So, if $T$ and $U$ belong to a lawful $F$-typeclass then the product $T \times U$ also does.

Statement 3. (a) If $T$ belongs to a lawful $F$-typeclass and $E$ is a fixed type then the type $E \to T$ also belongs to the same typeclass.

(b) If $P(T)$ is an endofunctor that preserves membership in a lawful $F$-typeclass (i.e., whenever $T$ belongs to the typeclass then $P(T)$ also does), then a fixpoint of $P$ is a type that also belongs to the same typeclass.

When there are no laws in the typeclass, we can easily construct a "free $F$-typeclass instance on X". This will just be the initial $G$-algebra where we define $G(A) = X + F(A)$. It will be initial in the $F$-typeclass category as long as the typeclass has no laws.

If there are some laws, the initial $G$-algebra will not satisfy them, so it is not initial in the lawful $F$-typeclass category. To obtain an initial object in that category, we need to find a $G$-algebra that has a special property of being a "compatible retract" of the initial $G$-algebra. The following definitions and statement describe the known results.

Denote by $R$ the initial $G$-algebra. (It is the least fixpoint of $G$.) Then for any $G$-algebra $T$ there exists a unique $G$-algebra morphism $r_T: R\to T$.

A $G$-algebra $C$ is called a "compatible retract" of the initial algebra $R$ if there exists a function $i: C \to R$ such that $r_C \circ i = \textrm{id}$.

If $C$ satisfies some laws then the function $i$ will not be an $G$-algebra morphism (that would contradict Statement 1). However, the composition $r_T \circ i$ will be an $F$-algebra morphism for some $G$-algebras $T$.

Statement 4. All such $T$ form a category that does not depend on the choice of $i$. Denote this category by $L(C, R)$.

Statement 5. A compatible retract $C$ is an initial object in the category $L(C, R)$.

Statement 6. The category $L(C, R)$ is the same as the category of all $G$-algebras that satisfy at least the same laws as $C$.

Statement 7. The type of law functions ($\forall A. \, (\textrm{Nat} \to A) \times (F(A) \to A) \to A \times A$) is equivalent, under assumptions of parametricity, to the type $FF(\textrm{Nat})\times FF(\textrm{Nat})$, where we denote by $FF(\textrm{Nat})$ the type of free monad on $F$ with values in $\textrm{Nat}$.

The free monad on $F$ with values in $X$, denoted by $FF(X)$, is defined as the least fixpoint of the recursive type equation $FF(X) = X + F(FF(X))$.

Statement 8. The same type $FF(\textrm{Nat})\times FF(\textrm{Nat})$ is equivalent to the type $\forall C. (\textrm{Nat}\to C)\to FF(C)\times FF(C)$. This is the type of pairs of unevaluated expression trees with arbitrary leaf values of type $C$ and operations from the functor $F$, i.e., unevaluated expression trees with $F$-typeclass operations. Those trees describe the symbolic expressions of two sides of the laws.