The functor of the identity monad can be defined as:

data Identity a = Identity a

Because this monad is free, an alternative definition is the following:

data Term f a = Pure a | Impure (f (Term f a))

data Zero a

type IdentityF a = Term Zero a

Since this is the same monad defined in two ways, they shoud be convertible into each other. That is to say that one should be able to define two functions f :: Identity a -> IdentityF a and g :: IdentityF a -> Identity a such that their compositions f . g and g . f are identities. The function f is easy to define:

f :: Identity a -> IdentityF a
f (Identity a) = Pure a

But what about the function g?

g :: IdentityF a -> Identity a
g (Pure a) = Identity a
g (Impure x) = ??????

What should be the value of g (Impure x). I could try to cheat and say it is undefined but then f . g would not be the identity function and Identity and IdentityF would not be isomorphic.

If such function g cannot be defined, does it mean that Identity and IdentityF are not isomorphic and thus the identity monad is not really free?

CodePudding user response：

One suitable definition is:

g (Impure x) = case x of

There are no branches in the case. This was not a typo. There are exactly as many branches in the case as there are constructors in Zero a, as required; this is a complete pattern match.

(You must turn on the EmptyCase extension for GHC to accept this as-is.)