<p>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.</p>
<p>In brief: A typeclass is an <span class="math-container">$F$</span>-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 <span class="math-container">$F$</span>-coalgebras, but some typeclasses are neither.</p>
<p>Begin by the definition of <span class="math-container">$F$</span>-algebra and <span class="math-container">$F$</span>-algebra morphisms. Let us choose an endofunctor <span class="math-container">$F$</span> (in the language of programming, <span class="math-container">$F$</span> is a covariant type constructor). A type <span class="math-container">$T$</span> is an <span class="math-container">$F$</span>-algebra if there exists a designated function <span class="math-container">$\alpha_T: F(T) \to T$</span>. The function <span class="math-container">$\alpha_T$</span> is called the structure map of <span class="math-container">$T$</span>.</p>
<p>An <span class="math-container">$F$</span>-algebra morphism between <span class="math-container">$F$</span>-algebras <span class="math-container">$T$</span> and <span class="math-container">$U$</span> is a function <span class="math-container">$f: T \to U$</span> such that the appropriate diagram commutes. See <a href="https://en.wikipedia.org/wiki/F-algebra" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/F-algebra</a></p>
<p>All <span class="math-container">$F$</span>-algebras form a category.</p>
<p>Now we call a &quot;lawful <span class="math-container">$F$</span>-typeclass&quot; any subcategory of <span class="math-container">$F$</span>-algebras <span class="math-container">$T$</span> whose structure maps <span class="math-container">$\alpha_T$</span> satisfies (zero or more) additional laws.</p>
<p>A type <span class="math-container">$T$</span> belongs to the <span class="math-container">$F$</span>-typeclass if there exists an evidence value <span class="math-container">$\alpha_T$</span> of type <span class="math-container">$F(T) \to T$</span>. So, the structure map of the <span class="math-container">$F$</span>-algebra is the evidence value for membership in the typeclass.</p>
<p>For example, the monoid typeclass is described by <span class="math-container">$F(T) = 1 + T \times T$</span>. The two monoid methods, <span class="math-container">$e$</span> and <span class="math-container">$\oplus$</span>, can be derived from a single function of type <span class="math-container">$F(T) \to T$</span>.</p>
<p>This example illustrates how the structure map of an <span class="math-container">$F$</span>-algebra describes at once all the operations of the typeclass.</p>
<p>Now, it is also important that the typeclass laws are described explicitly. This is done via special &quot;law functions&quot; and requires more explanation.</p>
<p>Most often, the typeclass laws have the form of an equation between values of type <span class="math-container">$T$</span>, where <span class="math-container">$T$</span> is the type that belongs to the typeclass. For example, the left identity law of the monoids is <span class="math-container">$\forall (t:T). \, (e\oplus t)=t$</span>. The two sides of the law are symbolic expressions built from some arbitrary values of type <span class="math-container">$T$</span> and the typeclass operations. This motivates the following definition:</p>
<p>A &quot;law function&quot; is a value of type <span class="math-container">$\forall A. \, (\textrm{Nat} \to A) \times (F(A) \to A) \to A \times A$</span>.</p>
<p>A lawful <span class="math-container">$F$</span>-typeclass may have zero or more law functions.</p>
<p>A law function takes an arbitrary number of arbitrary values of type <span class="math-container">$A$</span>, uses the typeclass operations via the evidence value <span class="math-container">$\alpha_A$</span>, and computes a pair of values of type <span class="math-container">$A$</span>. Those two values will be the two sides of the law. The law requires them to be equal.</p>
<p>This motivates the following definition of what it means that the evidence value &quot;satisfies a law&quot;:</p>
<p>Given a law function <span class="math-container">$l:\forall A. \, (\textrm{Nat} \to A) \times (F(A) \to A) \to A \times A$</span>, we say that an evidence value <span class="math-container">$\alpha_T: F(T)\to T$</span> &quot;satisfies the <span class="math-container">$l$</span>-law&quot; if, for any <span class="math-container">$f:\textrm{Nat} \to A$</span>, the value <span class="math-container">$l(f, \alpha_T)$</span> is a pair of equal values of type <span class="math-container">$A$</span>.</p>
<p>So, a type <span class="math-container">$T$</span> is an object of the &quot;lawful <span class="math-container">$F$</span>-typeclass&quot; category if two conditions hold:</p>
<ol>
<li>There exists a designated evidence value <span class="math-container">$\alpha_T$</span> of type <span class="math-container">$F(T) \to T$</span>.</li>
<li>The evidence value <span class="math-container">$\alpha_T$</span> satisfies the laws corresponding to each of the law functions (if any).</li>
</ol>
<p>Starting from these definitions, and assuming that relational parametricity can be applied to the law functions, I have proved several interesting results about lawful <span class="math-container">$F$</span>-typeclasses. Let me list some of those results without proof.</p>
<p>Statement 1. If <span class="math-container">$f: T\to U$</span> is an <span class="math-container">$F$</span>-algebra morphism and the laws of the typeclass hold for <span class="math-container">$\alpha_T$</span> then the same laws will also hold for <span class="math-container">$\alpha_U$</span>. In other words, <span class="math-container">$F$</span>-algebra morphisms automatically preserve the laws.</p>
<p>Statement 2. If <span class="math-container">$T$</span> and <span class="math-container">$U$</span> are two objects of a lawful <span class="math-container">$F$</span>-typeclass category then the product <span class="math-container">$T\times U$</span> is also an object of that category; that is, <span class="math-container">$T \times U$</span> is again an <span class="math-container">$F$</span>-algebra and also all laws will hold for <span class="math-container">$T \times U$</span>. So, if <span class="math-container">$T$</span> and <span class="math-container">$U$</span> belong to a lawful <span class="math-container">$F$</span>-typeclass then the product <span class="math-container">$T \times U$</span> also does.</p>
<p>Statement 3. (a) If <span class="math-container">$T$</span> belongs to a lawful <span class="math-container">$F$</span>-typeclass and <span class="math-container">$E$</span> is a fixed type then the type <span class="math-container">$E \to T$</span> also belongs to the same typeclass.</p>
<p>(b) If <span class="math-container">$P(T)$</span> is an endofunctor that preserves membership in a lawful <span class="math-container">$F$</span>-typeclass (i.e., whenever <span class="math-container">$T$</span> belongs to the typeclass then <span class="math-container">$P(T)$</span> also does), then a fixpoint of <span class="math-container">$P$</span> is a type that also belongs to the same typeclass.</p>
<p>When there are no laws in the typeclass, we can easily construct a &quot;free <span class="math-container">$F$</span>-typeclass instance on X&quot;. This will just be the initial <span class="math-container">$G$</span>-algebra where we define <span class="math-container">$G(A) = X + F(A)$</span>. It will be initial in the <span class="math-container">$F$</span>-typeclass category as long as the typeclass has no laws.</p>
<p>If there are some laws, the initial <span class="math-container">$G$</span>-algebra will not satisfy them, so it is not initial in the lawful <span class="math-container">$F$</span>-typeclass category. To obtain an initial object in that category, we need to find a <span class="math-container">$G$</span>-algebra that has a special property of being a &quot;compatible retract&quot; of the initial <span class="math-container">$G$</span>-algebra. The following definitions and statement describe the known results.</p>
<p>Denote by <span class="math-container">$R$</span> the initial <span class="math-container">$G$</span>-algebra. (It is the least fixpoint of <span class="math-container">$G$</span>.) Then for any <span class="math-container">$G$</span>-algebra <span class="math-container">$T$</span> there exists a unique <span class="math-container">$G$</span>-algebra morphism <span class="math-container">$r_T: R\to T$</span>.</p>
<p>A <span class="math-container">$G$</span>-algebra <span class="math-container">$C$</span> is called a &quot;compatible retract&quot; of the initial algebra <span class="math-container">$R$</span> if there exists a function <span class="math-container">$i: C \to R$</span> such that <span class="math-container">$r_C \circ i = \textrm{id}$</span>.</p>
<p>If <span class="math-container">$C$</span> satisfies some laws then the function <span class="math-container">$i$</span> will not be an <span class="math-container">$G$</span>-algebra morphism (that would contradict Statement 1). However, the composition <span class="math-container">$r_T \circ  i$</span> will be an <span class="math-container">$F$</span>-algebra morphism for <em>some</em> <span class="math-container">$G$</span>-algebras <span class="math-container">$T$</span>.</p>
<p>Statement 4. All such <span class="math-container">$T$</span> form a category that does not depend on the choice of <span class="math-container">$i$</span>. Denote this category by <span class="math-container">$L(C, R)$</span>.</p>
<p>Statement 5. A compatible retract <span class="math-container">$C$</span> is an initial object in the category <span class="math-container">$L(C, R)$</span>.</p>
<p>Statement 6. The category <span class="math-container">$L(C, R)$</span> is the same as the category of all <span class="math-container">$G$</span>-algebras that satisfy <em>at least</em> the same laws as <span class="math-container">$C$</span>.</p>
<p>Statement 7. The type of law functions (<span class="math-container">$\forall A. \, (\textrm{Nat} \to A) \times (F(A) \to A) \to A \times A$</span>) is equivalent, under assumptions of parametricity, to the type <span class="math-container">$FF(\textrm{Nat})\times FF(\textrm{Nat})$</span>, where we denote by <span class="math-container">$FF(\textrm{Nat})$</span> the type of free monad on <span class="math-container">$F$</span> with values in <span class="math-container">$\textrm{Nat}$</span>.</p>
<p>The free monad on <span class="math-container">$F$</span> with values in <span class="math-container">$X$</span>, denoted by <span class="math-container">$FF(X)$</span>, is defined as the least fixpoint of the recursive type equation <span class="math-container">$FF(X) = X + F(FF(X))$</span>.</p>
<p>Statement 8. The same type <span class="math-container">$FF(\textrm{Nat})\times FF(\textrm{Nat})$</span> is equivalent to the type <span class="math-container">$\forall C. (\textrm{Nat}\to C)\to FF(C)\times FF(C)$</span>. This is the type of pairs of unevaluated expression trees with arbitrary leaf values of type <span class="math-container">$C$</span> and operations from the functor <span class="math-container">$F$</span>, i.e., unevaluated expression trees with <span class="math-container">$F$</span>-typeclass operations. Those trees describe the symbolic expressions of two sides of the laws.</p>

CC BY-SA 4.0
2023-03-10T10:32:24.050Z
2023-04-17T17:08:58.283Z
2023-04-17T17:08:58.283Z
winitzki
<blockquote>
  <p>How do type classes fit in this model?</p>
</blockquote>

<p>The short answer is: they don't. </p>

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

<p>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:</p>

<pre><code>class Blah a where
   blah : a -&gt; 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"?
</code></pre>

<p>Depending on the choice of instance the compiler makes, <code>blah v</code> could equal either <code>"Hello"</code> or <code>"Goodbye"</code>. 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. </p>

<p>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. </p>

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

<p>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. </p>

<p>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.) </p>

CC BY-SA 3.0
2012-09-13T10:04:07.080Z
what is the runner up candidate that *does* have denotational semantics iyswim?
Ohad Kammar
CC BY-SA 3.0
2012-09-14T07:08:22.723Z
I have no idea, alas.
Neel Krishnaswami
CC BY-SA 3.0
2012-09-14T11:27:05.643Z
Does this merit an additional question?
Ohad Kammar
CC BY-SA 3.0
2013-06-05T13:16:39.973Z
@NeelKrishnaswami: Do you have any idea how ML modules fit into this? And what about Agda modules (which someone mentioned to me are "first class")?
Lii
CC BY-SA 3.0
2013-06-06T08:34:00.547Z
@Lii: ML modules and Agda records are *much* better-behaved, but it's too complicated to explain in a comment -- ask a question about them, and I (or someone else) will explain.
Neel Krishnaswami
CC BY-SA 3.0
2012-09-07T06:44:13.943Z
2012-09-07T06:44:13.943Z
Neel Krishnaswami
<p>
A functional language can be viewed as a <a href="http://www.haskell.org/haskellwiki/Hask">category</a> where its objects are types and morphisms functions between them.</p>

<p><strong>How do <a href="https://en.wikipedia.org/wiki/Type_class">type classes</a> fit in this model?</strong></p>

<p>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 <code>Functor</code> for which <code>fmap id ≡ id</code> and <code>fmap f . fmap g ≡ fmap (f . g)</code>.</p>

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

CC BY-SA 3.0
2012-09-06T17:08:32.407Z
You might want to be more explicit about exactly what you want a model for. If you want something that can rigorously describe the open world assumption, the behavior of instance resolution, the interaction of various GHC extensions, &c., that's rather more complicated than an idealized version. Similarly, note that bottoms are often ignored when discussing Hask.
C. A. McCann
CC BY-SA 3.0
2012-09-06T17:41:30.140Z
@camccann I want something that captures the concept of type classes mathematically so that one can study its properties. For example, we can say what monads are in Haskell, how they work and what rules they have, but only when we describe them mathematically we really see what they are. | Standard Haskell is just fine, no extensions etc., just the basic concept. And yes, I want to consider only total functions, no bottoms.
Petr
CC BY-SA 3.0
2012-09-06T17:53:17.513Z
Type classes can be thought of as [signatures](http://en.wikipedia.org/wiki/Signature_(logic)) (in the universal algebra sense). The collection of all entities sharing the same signature (elements of the same type class) is  a [variety](http://en.wikipedia.org/wiki/Variety_(universal_algebra)).
Dave Clarke
CC BY-SA 3.0
2012-09-06T18:43:59.303Z
@DaveClarke: It's not immediately obvious to me how to describe type classes on higher kinds that way, but I'm not terribly familiar with universal algebra and might be misunderstanding the correspondence you have in mind...
C. A. McCann
CC BY-SA 3.0
2012-09-06T19:16:41.270Z
@camccann: I'm not sure how far the correspondence goes. It certainly seemed like a good starting point.
Dave Clarke
CC BY-SA 3.0
2012-09-06T19:43:30.000Z
@camccann: Just change the base category over which you are defining your algebra: basic type classes like num are signatures over the category of haskell types (or objects of the Hsk category), type classes over type constructors are algebras over the category of functors from Hask to Hask. Note that universal algebra is completely subsumed by the notion of algebra in category theory. Also: Dave: you should turn your comment into an answer.
cody
CC BY-SA 3.0
2012-09-06T20:04:41.313Z
@cody: Type constructors need not be functors in general, but yes--for some reason I was thinking the base category ought to be the same. I don't think this approach would survive several well-known GHC extensions, but that's not an issue here.
C. A. McCann
CC BY-SA 3.0
2012-09-06T20:06:51.887Z
Something in this should be an answer :)
Suresh Venkat
CC BY-SA 3.0
2012-09-09T16:40:39.827Z
@DaveClarke Please turn your comment into an answer so that people can vote for it.
Petr
<lo.logic><functional-programming><ct.category-theory><denotational-semantics><type-systems>
A mathematical (categorical) description of type classes
Petr
# A mathematical (categorical) description of type classes

(Asked by: username_0 on 2012-09-06)

A functional language can be viewed as a [category](http://www.haskell.org/haskellwiki/Hask) where its objects are types and morphisms functions between them.

**How do [type classes](https://en.wikipedia.org/wiki/Type_class) 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)?

**Tags:** lo.logic, functional-programming, ct.category-theory, denotational-semantics, type-systems

> **Comments:**
> **username_1**: You might want to be more explicit about exactly what you want a model for. If you want something that can rigorously describe the open world assumption, the behavior of instance resolution, the interaction of various GHC extensions, &c., that's rather more complicated than an idealized version. Similarly, note that bottoms are often ignored when discussing Hask.  
> **username_0**: @camccann I want something that captures the concept of type classes mathematically so that one can study its properties. For example, we can say what monads are in Haskell, how they work and what rules they have, but only when we describe them mathematically we really see what they are. | Standard Haskell is just fine, no extensions etc., just the basic concept. And yes, I want to consider only total functions, no bottoms.  
> **username_2**: Type classes can be thought of as [signatures](http://en.wikipedia.org/wiki/Signature_(logic)) (in the universal algebra sense). The collection of all entities sharing the same signature (elements of the same type class) is  a [variety](http://en.wikipedia.org/wiki/Variety_(universal_algebra)).  
> **username_1**: @DaveClarke: It's not immediately obvious to me how to describe type classes on higher kinds that way, but I'm not terribly familiar with universal algebra and might be misunderstanding the correspondence you have in mind...  
> **username_2**: @camccann: I'm not sure how far the correspondence goes. It certainly seemed like a good starting point.  
> **username_3**: @camccann: Just change the base category over which you are defining your algebra: basic type classes like num are signatures over the category of haskell types (or objects of the Hsk category), type classes over type constructors are algebras over the category of functors from Hask to Hask. Note that universal algebra is completely subsumed by the notion of algebra in category theory. Also: Dave: you should turn your comment into an answer.  
> **username_1**: @username_3: Type constructors need not be functors in general, but yes--for some reason I was thinking the base category ought to be the same. I don't think this approach would survive several well-known GHC extensions, but that's not an issue here.  
> **username_4**: Something in this should be an answer :)  
> **username_0**: @DaveClarke Please turn your comment into an answer so that people can vote for it.  

---

## 2 answers

### Answer by username_6 on 2012-09-07. Score: 24 | Accepted answer

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.)

> **Comments:**
> **username_7**: what is the runner up candidate that *does* have denotational semantics iyswim?  
> **username_6**: I have no idea, alas.  
> **username_7**: Does this merit an additional question?  
> **username_8**: @NeelKrishnaswami: Do you have any idea how ML modules fit into this? And what about Agda modules (which someone mentioned to me are "first class")?  
> **username_6**: @username_8: ML modules and Agda records are *much* better-behaved, but it's too complicated to explain in a comment -- ask a question about them, and I (or someone else) will explain.  

---

### Answer by username_5 on 2023-03-10. Score: 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.


---

