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:
- There exists a designated evidence value $\alpha_T$ of type $F(T) \to T$.
- 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.