Writing the Identity monad in terms of Free

Question

In "Data types a la carte" Swierstra writes that given Free (which he calls Term) and Zero you can implement the Identity monad:

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

Term Zero is now the Identity monad. I understand why this is. The issue is that I can never use Term Zero as a Monad because of the pesky Functor f => constraint:

instance Functor f => Monad (Term f) where
    return x = Pure x
    (Pure x) >>= f = f x 
    (Impure f) >>= t = Impure (fmap (>>=f) t) 

How do I make Zero a Functor?

instance Functor Zero where
    fmap f z = ???

It seems like there's a trick here: Since Zero has no constructors, Impure can never be used, and so the Impure case of >>= is never called. This means fmap is never called, so there's a sense in which this is ok:

instance Functor Zero where
    fmap f z = undefined

The problem is, this feels like cheating. What am I missing? Is Zero actually a Functor? Or perhaps Zero isn't a Functor, and this is a shortcoming of how we express Free in Haskell?

Answer 1

If you turn on DeriveFunctor, you can write

data Zero a deriving Functor

but you might consider that cheating. If you want to write it yourself, you can turn on EmptyCase, instead, then write the funky-looking

instance Functor Zero where
    fmap f z = case z of

Answer 2

A trick way of defining Zero a is the following.

newtype Zero a = Zero (Zero a)

In other words, it encodes the sort of silly, slightly non-obvious statement that there is actually one way to get a value of Zero a: you must already have one!

With this definition, absurd :: Zero a -> b is definable in a "natural" way

absurd :: Zero a -> b
absurd (Zero z) = absurd z

In some sense these definitions are all legal because they point out exactly how they are not possible to instantiate. No values of Zero a can be constructed unless someone else "cheats" first.

instance Functor Zero where
  fmap f = absurd

Answer 3

One way to go about this is to use Data.Void instead of an empty data declaration, like this:

import Data.Void

-- `Zero a` is isomorphic to `Void`
newtype Zero a = Zero Void

instance Functor Zero where
    -- You can promise anything if the precondition is that
    -- somebody's gotta give you an `x :: Void`.
    fmap f (Zero x) = absurd x

See this question for some really great explanations of what Void is useful for. But the key idea is that the absurd :: Void -> a function lets you go from that can-never-happen x :: Void binding into any type you like.

Answer 4

Another spin on Luis Casillas's answer is to build your type entirely from stock parts:

type Id = Free (Const Void)

The Functor instance for Const x will work as you wish (its fmap doesn't do anything, which is just fine), and you'll only need to take care when unpacking:

runId (Pure x) = x
runId (Free (Const ab)) = absurd ab

All of these things, of course, are only "morally" equivalent to Identity, because they all introduce extra values. In particular, we can distinguish among

bottom
Pure bottom
Free bottom