My overdue post on free monads

Intuition

Just like how we can get a free Monoid ([]) for a type t.

We can get a free Monad for a functor F.

The methodology is the same, build up repeated contexts:

data [a] = [] | a : [a]
data Free f a = Pure a | Roll (f (Free f a))

Let’s see how we define the instances for Free.

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

class Functor f => Functor (Free f) where
  fmap f (Pure a) = Pure $ f a
  fmap f (Roll x) = Roll (fmap (fmap f) x)

class Functor f => Monad (Free f) where
  return = Pure a
  Pure a >>= f = f a
  Roll x >>= f = concatFree (fmap f x)
      where
          --AKA join ::              m      (m      a) -> m      a
          concatFree :: Functor f => Free f (Free f a) -> Free f a
          concatFree (Pure x) = x
          concatFree (Roll y) = Roll (fmap concatFree y)
          -- E.g.
          --   concatFree $ Roll (Identity (Pure (Roll (Identity (Pure a)))))
          -- = Roll (fmap concatFree $ Identity (Pure (Roll (Identity (Pure a))))) -- Essence of why concatFree works
          -- = Roll (Identity (concatFree $ Pure (Roll (Identity (Pure a)))))
          -- = Roll (Identity (Roll (Identity (Pure a))))

Why is it useful?

As I was thinking how we can use DSLs to model computations e.g. IO, I came across free monads.

A familiarity with Monads is expected in this post.

In our case, we want to factor out impure parts from any code using free monads.

Free monads allows us to decompose any impure program into a pure representation of its behavior and a minimal impure interpreter.

Suppose we want to model IO parts:

-- | Taken from haskell for all (see references)
import Control.Monad.Free
import System.Exit hiding (ExitSuccess)

data TeletypeF x
  = PutStrLn String x
  | GetLine (String -> x)
  | ExitSuccess

instance Functor TeletypeF where
    fmap f (PutStrLn str x) = PutStrLn str (f x)
    fmap f (GetLine      k) = GetLine (f . k)
    fmap f  ExitSuccess     = ExitSuccess

type Teletype = Free TeletypeF

putStrLn' :: String -> Teletype ()
putStrLn' str = liftF $ PutStrLn str ()

getLine' :: Teletype String
getLine' = liftF $ GetLine id

exitSuccess' :: Teletype r
exitSuccess' = liftF ExitSuccess

-- Our interpreter
run :: Teletype r -> IO r
run (Pure r) = return r
run (Free (PutStrLn str t)) = putStrLn str >>  run t
run (Free (GetLine  f    )) = getLine      >>= run . f
run (Free  ExitSuccess    ) = exitSuccess

echo :: Teletype ()
echo = do str <- getLine'
          putStrLn' str
          exitSuccess'
          putStrLn' "Finished"

main = run echo

It seems like we paid a price however…? Our program is more much verbose… and… we still seem to have an error as shown below

import System.Exit

main = do x <- getLine
          putStrLn x
          exitSuccess
          putStrLn "Finished" -- <-- oops!

There is no way to prove it. For instance exitSuccess could be redefined as exitSuccess = return (). That way "Finished" still gets printed to stdout.

References

logo