data Term f a = Pure a | Impure (f (Term f a))These monads consist of either pure values or an impure effect, constructed using

`f`

. When `f`

is a functor, `Term f`

is a monad. And in this case, `Term f`

is the free monad being the left adjoint to the forgetful functor `f`

.I am not going into the details of what makes a monad

*free*. I once asked this question on google+ and Edward Kmett came up with a beautiful explanation. So instead of trying to come up with a half assed version of the same, have a look at Ed's response here .

In short, we can say that a free monad is the freeest object possible that's still a monad.

# Composition

Free monads compose and help you build larger abstractions which are pure data and yet manage to retain all properties of a monad. Hmm .. this sounds interesting because now we can not only build abstractions but make them extensible through composition by clients using the fact that it's still a monad.A free monad is pure data, not yet interpreted, as we will see shortly. You can pass it to a separate interpreter (possibly multiple interpreters) which can do whatever you feel like with the structure. Your free monad remains pure while all impurities can be put inside your interpreters.

# And so we interpret ..

In this post I will describe how I implemented an interpreter for a Joy like concatenative language that uses the stack for its computation. Of course it's just a prototype and addresses an extremely simplified subset, but you get the idea. The basic purpose is to explore the power of free monads and come up with something that can potentially be extended to a full blown implementation of the language.When designing an interpreter there's always the risk of conflating the language along with the concerns of interpreting it. Here we will have the 2 completely decoupled by designing the core language constructs as free monads. Gabriel Gonzalez has written a series of blog posts [1,2,3] on the use of free monads which contain details of their virtues and usage patterns. My post is just an account of my learning experience. In fact after I wrote the post, I discovered a similar exercise done for embedding Forth in Haskell - so I guess I'm not the first one to learn free monads using a language interpreter.

Let's start with some code, which is basically a snippet of Joy like code that will run within our Haskell interpreter ..

p :: Joy () p = do push 5 push 6 add incr add2 square cube end

This is our wish list and at the end of the post we will see if we can interpret this correctly and reason about some aspects of this code. Let's not bother much about the details of the above snippet. The important point is that if we fire it up in ghci, we will see that it's pure data!

*Joy> p Free (Push 5 (Free (Push 6 (Free (Add (Free (Push 1 (Free (Add (Free (Push 1 (Free (Add (Free (Push 1 (Free (Add (Free (Dup (Free (Mult (Free (Dup (Free (Dup (Free (Mult (Free (Mult (Free End)))))))))))))))))))))))))))))) *Joy>

We haven't yet executed anything of the above code. It's completely free to be interpreted and possibly in multiple ways. So, we have achieved this isolation - that the data is freed from the interpreter. You want to develop a pretty printer for this data - go for it. You want to apply semantics and give an execution model based on Joy - do it.

# Building the pure data (aka Builder)

Let's first define the core operators of the language ..data JoyOperator cont = Push Int cont | Add cont | Mult cont | Dup cont | End deriving (Show, Functor)

The interesting piece is the derivation of the

`Functor`

, which is required for implementing the forgetful functor adjoint of the free monad. Keeping the technical mumbo jumbo aside, free monads are just a general way of turning functors into monads. So if we have a core operator `f`

as a functor, we can get a free monad `Free f`

out of it. And knowing something is a free monad helps you transform transform an operation over the monad (the monad homomorphism) into an operation over the functor (functor homomorphism). We will see how this helps later .. The other point to note is that all operators take a continuation argument that points to the next operation in the chain.

`End`

is the terminal symbol and we plan to ignore anything that the user enters after an `End`

.`Push`

takes an `Int`

and pushes into the stack, `Add`

pops the top 2 elements of the stack and pushes the sum, `Mult`

does the same for multiplication and `Dup`

duplicates the top element of the stack. `End`

signifies the end of program.Next we define the free monad over

`JoyOperator`

by using the `Free`

data constructor, defined as part of `Control.Monad.Free`

..data Free f a = Pure a | Free (f (Free f a))

-- | The free monad over JoyOperator type Joy = Free JoyOperator

And then follow it up with some of the definitions of Joy operators as operations over free monads. Note that

`liftF`

lifts an operator (which is a `Functor`

) into the context of a free monad. `liftF`

has the following type ..liftF :: Functor f => f a -> Free f a

As a property, a free moand has a forgetful functor as its left adjoint. The unlifting from the monad to the functor is given by the

`retract`

function ..retract :: Monad f => Free f a -> f a

and needless to say

retract . liftF = id

-- | Push an integer to the stack push :: Int -> Joy () push n = liftF $ Push n () -- | Add the top two numbers of the stack and push the sum add :: Joy () add = liftF $ Add ()

.. and this can be done for all operators that we wish to support.

Not only this, we can also combine the above operators and build newer ones. Remember we are working with monads and hence the *do* notation based sequencing comes for free ..

-- | This combinator adds 1 to a number. incr :: Joy () incr = do {1; add} -- | This combinator increments twice add2 :: Joy () add2 = do {incr; incr} -- | This combinator squares a number square :: Joy () square = do {dup; mult}

Now we can have a composite program which sequences through the core operators as well as the ones we derive from them. And that's what we posted as our first example snippet of a target program.

# An Interpreter (aka Visitor)

Once we have the pure data part done, let's try and build an interpreter that does the actual execution based on the semantics that we defined on the operators.-- | Run a joy program. Result is either an Int or an error runProgram :: Joy n -> Either JoyError Int runProgram program = joy [] program where joy stack (Free (Push v cont)) = joy (v : stack) cont joy (a : b : stack) (Free (Add cont)) = joy (a + b : stack) cont joy (a : b : stack) (Free (Mult cont)) = joy (a * b : stack) cont joy (a : stack) (Free (Dup cont)) = joy (a : a : stack) cont joy _ (Free Add {}) = Left NotEnoughParamsOnStack joy _ (Free Dup {}) = Left NotEnoughParamsOnStack joy [] (Free End) = Left NotEnoughParamsOnStack joy [result] (Free End) = Right result joy _ (Free End) = Left NotEmptyOnEnd joy _ Pure {} = Left NoEnd

`runProgram`

is the interpreter that takes a free monad as its input. Its implementation is quite trivial - it just matches on the recursive structure of the data and pushes the appropriate results on the stack. Now if we run our program `p`

using the above interpreter we get the correct result ..*Joy> runProgram p Right 7529536 *Joy>

# Equational Reasoning

Being Haskell and being pure, we obviously can prove some bits and pieces of our program as mathematical equations. At the beginning I said that End is the end of the program and anything after End needs to be ignored. What happens if we do the following ..runProgram $ do {push 5; incr; incr; end; incr; incr}

If you have guessed correctly we get

`Right 7`

, which means that all operations after `end`

have been ignored. But can we prove that our program indeed does this ? The following is a proof that `end`

indeed ends our program. Consider some operation `m`

follows `end`

..end >> m -- definition of end = liftF $ End >> m -- m >> m' = m >>= \_ -> m' = liftF $ End >>= \_ -> m -- definition of liftF = Free End >>= \_ -> m -- Free m >>= f = Free (fmap (>>= f) m) = Free (fmap (>>= \_ -> m) End) -- fmap f End = End = Free End -- liftF f = Free f (f is a functor) = liftF End -- definition of End = end

So this shows that any operation we do after

`end`

is never executed.
## 3 comments:

Love the blog, this is an excellent overview of free monads! BTW, you should post your posts on the haskell sub-reddit http://www.reddit.com/r/haskell. Lot's of good discussion usually ensues!

Every time I come back to haskell I generally spend a few days hammering boilerplate monad instantiation back into my head. I was also unaware that deriving functors was possible. You saved me a few days and then some.

Definition of incr should be : incr = do {push 1; add}

Post a Comment