Haskell type class and initial algebra

Question

For the example below, I am trying to understand how Haskell type classes, type class instances, and data types relate to the concept of initial algebra. There are two Haskell data types sharing a pair of operations for equality and addition. From my, perhaps incorrect, understanding the instances, which include the data types, specify two non-isomorphic initial algebras. It seems to me that the type class permits the overloading of the operations and plays no role in the specification of the initial algebra. Is this a correct interpretation of the given example?

data Nat0 = Zero | Succ0 Nat0 deriving Show
data Nat1 = One | Succ1 Nat1 deriving Show

class PeanoNum n where
 eq :: n -> n -> Bool
 add :: n -> n -> n

-- Two different non-isomorphic algebras.
instance PeanoNum Nat0 where
 eq Zero Zero = True 
 eq (Succ0 m) (Succ0 n) = eq m n
 eq _ _  = False 
 add m Zero = m 
 add m (Succ0 n) = Succ0 (add m n) 


instance PeanoNum Nat1 where
 eq One One = True
 eq (Succ1 m) (Succ1 n) = eq m n
 eq _ _ = False
 add m One = Succ1 m
 add m (Succ1 n) = Succ1 (add m n)

Answer 1

tl;dr: we can show that they are in fact isomorphic. Defining two different instances over them does not make them different. Defining two different functions over two types does not make them non-isomorphic! The instances are not describing an initial algebra structure, the data keyword is. As you say, the two instances play no role in the specification of the initial algebra.

---

In our example, we work with algebras for the functor $1 + -$. That is, an algebra $A$ is given by a morphism $1 + A \to A$, or, in other words, an element of type $A$, which can be seen as a morphism $1 \to A$, and an endomorphism $A \to A$.

data Nat0 = Zero | Succ0 Nat0
data Nat1 = One | Succ1 Nat1

Here, Zero and One are the elements while Succ0 and Succ1 are the endomorphisms. We will see that they are isomorphic as F-algebras. A morphism $f$ between two F-algebras $A$ (with element $a$ and endomorphism $u$) and $B$ (with element $b$ and endomorphism $v$) is a $f \colon A \to B$ making the following diagram commute.

$$\require{AMScd}\begin{CD} A+1 @>f+1>> B+1\\ @VVa+uV @VVb + vV\\ A @>f>> B \end{CD}$$

And, in fact, we can find a pair of invertible morphisms making them isomorphic. I will only define the first one, but the second one is analogous and checking that they are inverses should be easy.

$$\require{AMScd}\begin{CD} \mathsf{Nat0}+1 @>f+1>> \mathsf{Nat1}+1\\ @VV\mathsf{Zero+Succ0}V @VV\mathsf{One + Succ1}V\\ \mathsf{Nat0} @>f>> \mathsf{Nat1} \end{CD}$$

The commutativity of the diagram determines that the only possible $f$ must send Zero to One and Succ0 x to Succ1 x. This translates into code as follows.

f :: Nat0 -> Nat1
f Zero = One
f (Succ0 x) = Succ1 x

Precisely because $A$ is initial, this is the only possible $f$ making this diagram commute. We had no choice when defining $f$ (apart from undefined or any other of the constructions that make this kind of categorical reasoning fail in Haskell).

What about the two instances? They define two different functions over each one of the types, but that does not make them non-isomorphic as algebras. As you say, the instances play no role on the definition of the two algebras. The algebra structure concerns only the $1+A \to A$ morphism, not the two additional morphisms $A \times A \to A$ and $A \times A \to \mathsf{Bool}$ that define the instance. Even if we call the two different functions add, the second one is simply a different function. We could rename the second add, and we would see that they are, essentially, two different instances of the same class for (essentially) the same type.

What if we want an "add" (a binary) function to be part of the algebra? Then we would be looking for the initial algebra for the functor $F(X) = 1 + X + X \times X$, and neither Nat0 nor Nat1 (with their respective add functions) are initial algebras for this functor. The initial algebra would be the following one.

data Foo = Zero | Succ Foo | Add Foo Foo

What if we also want an "equality" function to be part of the algebra? There may be a better approach for this, but we can consider algebras on the category whose objects are pairs of types. An algebra is of the form $F(A,B) \to (A,B)$ for some endofunctor $F$, and in this case, we consider algebras of the form $(1 + A + A \times A, A \times A) \to (A,B)$. The natural numbers ($A$) and the booleans ($B$) endowed with zero $1 \to A$, the successor function $A \to A$, addition $A \times A \to A$, and the equality function $A \times A \to B$ would be an algebra of this form, but not the initial algebra. I think the initial algebra in this case could be written in Haskell as follows.

-- Initial algebra (where the object is a pair of types!).
data A = Zero | Succ A | Add A A
data B = Equ A A

-- Given any other algebra.
data C
data D
z :: C
s :: C -> C
a :: C -> C -> C
e :: C -> C -> D

-- There is a unique morphism (two morphisms) from the initial
-- algebra making the relevant diagram commute.
u1 :: A -> C
u1 Zero = z
u1 (Succ x) = s (u1 x)
u1 (Add x y) = a (u1 x) (u1 y)

u2 :: B -> D
u2 (Equ x y) = e (u1 x) (u1 y)

Where the relevant diagram is the following one.

$$\require{AMScd}\begin{CD} (1+A+A\times A,A \times A) @>>> (1+C+C\times C,C \times C)\\ @V(Zero+Succ+Add,Equ)VV @VV(z+s+a,e)V\\ (A,B) @>(u1,u2)>> (C,D) \end{CD}$$