# Free Monads and the Yoneda Lemma

Last week I gave a talk on Purely Functional I/O at Scala.io in Paris. The slides for the talk are available here. In it I presented a data type for `IO` that is supposedly a “free monad”. But the monad I presented is not exactly the same as `scalaz.Free` and some people have been asking me why there is a difference and what that difference means.

## IO as an application of Free

The `Free` monad in Scalaz is given a bit like this:

And throughout the methods on `Free`, it is required that `F` is a functor because in order to get at the recursive step inside a `Suspend`, we need to `map` over the `F` somehow.

But the `IO` monad I gave in the talk looks more like this:

And it could actually be stated as an application of `Free`:

So in a very superficial sense, this is how the `IO` monad relates to `Free`. The monad `IO[F,_]` for a given `F` is the free monad generated by the functor `(F[I], I => _)` for some type `I`. And do note that this is a functor no matter what `F` is.

## IO as equivalent to Free

There is a deeper sense in which `IO` and `Free` are actually equivalent (more precisely, isomorphic). That is, there exists a transformation from one to the other and back again. Since the only difference between `IO` and `Free` is in the functors `F[_]` vs `∃I. (F[I], I => _)`, we just have to show that these two are isomorphic for any `F`.

### The Yoneda lemma

There is an important result in category theory known as the Yoneda lemma. What it says is that if you have a function defined like this…

…then you certainly have a value of type `F[A]`. All you need is to pass the identity function to `map` in order to get the value of type `F[A]` out of this function. In fact, a function like this is in practice probably defined as a method on a value of type `F[A]` anyway. This also means that `F` is definitely a functor.

The Yoneda lemma says that this goes the other way around as well. If you have a value of type `F[A]` for any functor `F` and any type `A`, then you certainly have a `map` function with the signature above.

In scala terms, we can capture this in a type:

And the Yoneda lemma says that there is an isomorphism between `Yoneda[F,A]` and `F[A]`, for any functor `F` and any type `A`. Here is the proof:

### CoYoneda

Of course, this also means that if we have a type `B`, a function of type `(B => A)` for some type `A`, and a value of type `F[B]` for some functor `F`, then we certainly have a value of type `F[A]`. This is kind of obvious, since we can just pass the `B => A` and the `F[B]` to the `map` function for the functor and get our `F[A]`.

But the opposite is also true, and that is the really interesting part. If we have a value of type `F[A]`, for any `F` and `A`, then we can always destructure it into a value of type `F[B]` and a function of type `B => A`, at least for some type `B`. And it turns out that we can do this even if `F` is not a functor.

This is the permutation of the Yoneda lemma that we were using in `IO` above. That is, `IO[F, A]` is really `Free[({type λ[α] = CoYoneda[F,α]})#λ, A]`, given:

And the lemma says that `CoYoneda[F,A]` is isomorphic to `F[A]`. Here is the proof:

Of course, this destructuring into `CoYoneda` using the identity function is the simplest and most general, but there may be others for specific `F` and `A` depending on what we know about them.

So there you have it. The `scalaz.Free` monad with its `Suspend(F[Free[F,A]])` constructor and the `IO` monad with its `Req(F[I], I => IO[F,A])` constructor are actually equivalent. The latter is simply making use of `CoYoneda` to say the same thing.

Why bother? The useful part is that `CoYoneda[F,_]` is a functor for any `F`, so it’s handy to use in a free monad since we can then drop the requirement that `F` is a functor. What’s more, it gives us map fusion for free, since `map` over `CoYoneda` is literally just function composition on its `f` component. Although this latter is, in the absence of tail call elimination, not as useful as it could be in Scala.

I hope that sheds a little bit of light on the Yoneda lemma as well as the different embeddings of free monads.