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.
