Does FreeT keep the equational reasoning benefits of Free?

Question

In this blog post , the author explains the equational reasoning benefits of purifying code with the Free monad. Does the Free monad transformer FreeT retain these benefits, even if its wrapped over IO?

Answer 1

Yes. FreeT does not depend on any specific properties of the base monad, other than the fact that it is a monad. Every equation that you can deduce for Free f has an equivalent proof for FreeT f m.

To demonstrate that, let's repeat the exercise in my blog post, but this time using FreeT:

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

type Teletype = FreeT TeletypeF

exitSuccess :: (Monad m) => Teletype m r
exitSuccess = liftF ExitSuccess

Let's use the following definitions for free monad transformers:

return :: (Functor f, Monad m) => r -> FreeT f m r
return r = FreeT (return (Pure r))

(>>=) :: (Functor f, Monad m) => FreeT f m a -> (a -> FreeT f m b) -> FreeT f m b
m >>= f = FreeT $ do
    x <- runFreeT m
    case x of
        Free w -> return (Free (fmap (>>= f) w))
        Pure r -> runFreeT (f r)

wrap :: (Functor f, Monad m) => f (FreeT f m r) -> FreeT f m r
wrap f = FreeT (return (Free f))

liftF :: (Functor f, Monad m) => f r -> FreeT f m r
liftF fr = wrap (fmap return fr)

We can use equational reasoning to deduce what exitSuccess reduces to:

exitSuccess

-- Definition of 'exitSuccess'
= liftF ExitSuccess

-- Definition of 'liftF'
= wrap (fmap return ExitSuccess)

-- fmap f ExitSuccess = ExitSuccess
= wrap ExitSuccess

-- Definition of 'wrap'
= FreeT (return (Free ExitSuccess))

Now we can reprove that exitSuccess >> m = exitSuccess:

exitSuccess >> m

-- m1 >> m2 = m1 >>= \_ -> m2
= exitSuccess >>= \_ -> m

-- exitSuccess = FreeT (return (Free ExitSuccess))
= FreeT (return (Free ExitSuccess)) >>= \_ -> m

-- use definition of (>>=) for FreeT
= FreeT $ do
    x <- runFreeT $ FreeT (return (Free ExitSuccess))
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- runFreeT (FreeT x) = x
= FreeT $ do
    x <- return (Free ExitSuccess)
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- Monad Law: Left identity
-- do { y <- return x; m } = do { let y = x; m }
= FreeT $ do
    let x = Free ExitSuccess
    case x of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- Substitute in 'x'
= FreeT $ do
    case Free ExitSuccess of
        Free w -> return (Free (fmap (>>= (\_ -> m)) w))
        Pure r -> runFreeT ((\_ -> m) r)

-- First branch of case statement matches 'w' to 'ExitSuccess'
= FreeT $ do
    return (Free (fmap (>>= (\_ -> m)) ExitSuccess))

-- fmap f ExitSuccess = ExitSuccess
= FreeT $ do
    return (Free ExitSuccess)

-- do { m; } desugars to 'm'
= FreeT (return (Free ExitSuccess))

-- exitSuccess = FreeT (return (Free ExitSuccess))
= exitSuccess

The do block in the proof belonged to the base monad, yet we never needed to use any specific source code or properties of the base monad in order to manipulate it equationally. The only property we needed to know was that it was a monad (any monad!) and obeyed the monad laws.

Using only the monad laws, we were still able to deduce that exitSuccess >> m = exitSuccess. That's the reason why the monad laws matter, because they allow us to reason about code over a polymorphic base monad, knowing only that it is a monad.

More generally, this is the reason that people say that type classes should always have associated laws (like the monad laws, or the functor laws, or the category laws), because these allow you to reason about code that uses that type class without consulting the specific instances of that type class. Without these kinds of laws, the type class interface wouldn't truly be a loosely coupled interface since you wouldn't be able to equationally reason about it without consulting the original instance source code.

Also, if you want an extra dose of category theory, we can easily prove that every property that holds for Free must also hold for FreeT if the base monad is polymorphic. All we have to do is prove that:

(forall m. (Monad m) => FreeT f m r) ~ Free f r

The ~ symbol means "is isomorphic to", which means that we must prove that there are two functions, fw, and bw:

fw :: (forall m . (Monad m) => FreeT f m r) -> Free f r

bw :: Free f r -> (forall m . (Monad m) => FreeT f m r)

... such that:

fw . bw = id

bw . fw = id

It's an interesting proof, and I leave it as an exercise!