What is the initial algebra of the identity functor?

Question

I am trying to solve some of the exercises in Bird's Algebra of Programming. He defines an initial algebra as the initial object in the category of some F-algebra.

In the book, he says that

data Nat = Zero | Succ Nat

is the initial algebra of the Maybe Functor, i.e, the functor F, where $FA = 1 + A$ and $Ff = id_1 + f$.

Then he asks the following question as an exercise:

What is the initial algebra of the Identity Functor?

I have two guesses for this:

• My first guess, going by the pattern indicated for Nat, would be some bizzare object like this: data X = Tag X. But in this case, I cannot figure out what the homomorphism from X to an arbitrary A be.
• My second guess is that the initial object is some kind of tagged union of all the types and the homomorphism is an appropriate projection.

Any help is appreciated

Answer 1

NOTE: copy-paste the sections in this answer to play with inside ghci

Note that the initial object can be represented in Haskell as as an inhabitant of the type Mu (as shown below).

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE EmptyCase #-}
import Prelude hiding (Maybe, Just, Nothing)

-- | Mu F = initial object with respect to functor F
data Mu f = Mu (f (Mu f))

I now exhibit the ismorphism between Nat and Mu Maybe below:

-- | Maybe
data Maybe a = Just a | Nothing deriving(Show)

-- | Naturals
data Nat = Zero | Succ Nat deriving(Show)

-- | Bijection between naturals and initial object of Maybe functor
natfwd :: Nat -> Mu (Maybe)
natfwd Zero = Mu Nothing
natfwd (Succ n) = Mu (Just (natfwd n))

natbwd :: Mu (Maybe) -> Nat
natbwd (Mu Nothing) =  Zero
natbwd (Mu (Just mu)) = Succ (natbwd mu)

Next, I show that the initial object generated by Id is isomorphic to Void --- that is, it is uninhabited.

Intuitively, the initial object contains "arbitrary many nestings" of the original functor F. In the Maybe case, we had the ability to use Nothing to terminate this nesting. However, in the case of Id, this is no longer the case: there is no "branch" in the type Id to break this arbitrary recursion. Hence, it cannot be inhabited by any inductive value.

Void is a way to declare values in haskell that cannot be inhabited, in case you have not seen it before. Void has no data constructors.

data Void

data Id a = Id a

isoFwd :: Mu Id -> Void
isoFwd (Mu (Id x)) = isoFwd x

isoBwd :: Void -> Mu Id
isoBwd v = case v of

Claim: isoFwd : Mu Id -> Void proves that Mu Id is not inhabited

Assume for contradiction that Mu Id is inhabited. Hence, there exists an x : Mu Id. Now, compute y = (isoFwd x) : Void. But we know that Void is uninhabited. Hence, contradiction. Therefore, Mu Id must be uninhabited.

Claim: isoFwd, isoBwd define an isomorphism between Void and Mu Id

To discuss equality of functions, we define: \begin{align*} \forall f, g : X \rightarrow Y, \quad f ~\texttt{==}~g \equiv \forall x \in X, f (x) = g(x) \end{align*}

Note that if $X$ is uninhabited, then the relation ${f~\texttt{==}~g}$ is vacuously true. Armed with this, we show that isoFwd. isoBwd = id = isoBwd . isoFwd.

• isoFwd . isoBwd :: Void -> Void == id :: Void -> Void since Void is uninhabited, and hence the two LHS and RHS are vacuously equal.

• isoBwd . isoFwd :: Mu Id -> Mu Id == id :: Mu Id -> Mu Id since Mu Id is uninhabited, and hence the LHS and RHS are vacuously equal.

Further reading

For more of this kind of computational perspective, I can recommend reading about recursion schemes and cata/anamorphisms, from Bananas, Lenses, and Barbed Wire as well as the recursion-schemes library.

Answer 2

The initial algebra of the identity functor is a set $X$ together with a map $X\to X$ that is initial among all such maps : for any set $Y$ and map $Y\to Y$, there is a unique map $X\to Y$ making

$$\require{AMScd}\begin{CD} X @>>> X \\ @VVV @VVV \\ Y@>>> Y\end{CD}$$commute. In particular, for any $Y$ there is a unique map $X\to Y$ (taking $id_Y :Y\to Y$), so $X$ is initial.

Conversely, if $X$ is initial...