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?

yes, `Zero` is a functor from `Hask` to `0`, the empty category (which then is embedded back into Hask). — Sassa NF, Sep 22 '15 at 11:50

score 12 · Accepted Answer · answered Sep 22 '15 at 04:52

12

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

answered Sep 22 '15 at 04:52

Daniel Wagner

145,880
9
220
380

I wondered what happens if we cheat and do `fmap f _|_` in both these functor instances. In GHCi 7.10.2, the first instance errors out with `Exception: Void fmap`, without trying to evaluate the bottom, while the second does evaluate it. I'd have expected a non-exhaustiveness error instead. Not that this really matters -- both instances are fine, albeit they produce different bottoms if we pass one. – chi Sep 22 '15 at 08:59
2

@chi You definitely shouldn't expect a non-exhaustiveness error: these pattern matches are exhaustive! – Daniel Wagner Sep 22 '15 at 16:54
I somehow expected the practical equivalence between `case e of p1 -> e1 ; .. ; pn -> en` and `case e of ... ; pn -> en ; _ -> error "non exhaustive"`. This "under-the-hood" equivalence only breaks for n=0 (if we do not identify "different" bottoms). About exhaustiveness... I would be more convinced in Agda/Coq or any other total programming language. In Haskell, you are right, but bottoms are strange beasts, and I have no clear idea about whether `case _|_ :: Void of {}` should evaluate the argument or not, operationally speaking. – chi Sep 22 '15 at 17:28

score 7 · Answer 2 · edited May 23 '17 at 11:50

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.

score 7 · Answer 3 · answered Sep 22 '15 at 13:45

7

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

answered Sep 22 '15 at 13:45

J. Abrahamson

72,246
9
135
180

It's worth pointing out that this is more or less how the `Data.Void` module is implemented. – Luis Casillas Sep 22 '15 at 18:32
Hah, yes, that is true! – J. Abrahamson Sep 22 '15 at 18:34
1

`Data.Void` used to do this, before `EmptyCase` came out (it was changed when it moved from `void` to `base`). I don't know if it changed for clarity, efficiency, or error reporting reasons. Do you? – dfeuer Sep 22 '15 at 18:34
1

@dfeuer: Oh, I hadn't noticed that `base` now has `Void` (since 4.8.0.0). Note that the old `void` package advertised itself as "a Haskell 98 logically uninhabited data type"; that's the original point of this answer's trick. – Luis Casillas Sep 23 '15 at 01:09

score 3 · Answer 4 · edited May 23 '17 at 11:59

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

Writing the Identity monad in terms of Free

4 Answers4