Free Monads Won't Detox Your Colon—Busting the Myths of a Misunderstood Concept

(Note: This is an adapted version of an article that originally appeared in The Haskell Courant.)

At the local Functional Programming meetup, I met a haskeller who's building an IoT business. He's leveraging Haskell to power his backend data collection services. While browsing on the web, he saw how frequently free monads were mentioned. The FOMO hit him hard: he just gotta have some free monads in his codebase. So he tried to read a bunch of articles about the concept but came up none the wiser.

More precisely, he read Gabriel Gonzalez's "Purify Code Using Free Monads" which was written back in 2012. From the (long! complicated!) haskell subreddit convo, you could see how some folks have already clued in to the flaws of the blog post. For instance, redditor /u/gasche starts the critique in a thread which happens to be the most informed one of the convo. But even there, facts and opinions are so intermixed that it's hard to follow the chain of logic.

High time that the following facts are put up front and center:

Free monads only make sense if you want to DSL-ize parts of your codebase.
Free monads come with a considerable cost of roll-your-own runtime interpretation that misses out on optimizations that compiler devs have already done for you.
Free monads don't purify code in the sense of automagically debugging it.

What follows is a self-contained read to help you arrive at the above conclusions yourself.

Let's start by debriefing on how the free monad translation actually works.

Here's a little Teletype subset of IO comprising exactly two functions: putStrLn :: String -> IO () and getLine :: IO String. And here's the base functor that data-encodes this subset:

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

Believe it or not, this teeny-tiny fragment of the IO space is enough for us to deduce the general pattern for the rest. If you have a natively effectful function

fooIO :: A -> B -> C -> IO Z

where A, B, C stand—not for type variables—but for concrete, non-IO types like Int, Char, Bool; then fooIO gets mapped to the data constructor FooIO in

data BaseF x
   = ...
   | FooIO A B C (Z -> x)
   | ...

So for instance, putStrLn :: String -> IO () is actually mapped to the constructor PutStrLn with two parameters: String and () -> x. In other words, the base functor should strictly speaking look like this:

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

But () -> x and x are mostly equivalent. So we elide and just refer to x.

Now let's expand our little subset of IO by adding the program-terminating action: exitSuccess :: IO (). Again we apply the equivalence between () -> x and x to get:

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

But wait! If you pull up the "Purify code" blog post, here's what you'll find:

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

It's small and easily missed, but yes, the data constructor ExitSuccess should have the parameter x—for the reasons already given—whereas "Purify code" doesn't.

So what, you might ask. What's the impact of this difference?

Well, for one thing, you'll find that this blog post claim no longer holds: "Any command after exitSuccess' never executes." Instead of the blog's claim of

exitSuccess' >> m = exitSuccess'

you can only conclude that

exitSuccess' >> m = Free (ExitSuccess m)

Of course, you might suspect that—far from the blog post being in error—in fact, it's the analysis that you're reading right now that's wrong!

Fact is: the free monad translation is totally a turn-the-crank procedure. We select the fragment of the monadic space. Then we gather the type signatures in that fragment. And presto! The encoding drops out just like that. No creative ingenuity needed.

And this is really what's the big use case of free monads: encoding the syntax of a mini-language.

If you remember LISP, the grand-daddy of functional programming languages, it had a concept of homoiconicity—namely, the identification of the syntax of the language with the syntax of data structures—that captivated the imagination of many who dreamed of infinite A.I. possibilities revolving around nonstop loops of programs writing more programs.

Now Haskell is not homoiconic. Moreover, it's typed, unlike LISP. Still, an incredibly productive use of Haskell—engineering a Domain-Specific Language (DSL)—often involves capturing language syntax in a data structure. Dan "sigfpe" Piponi once expressed the folk wisdom behind DSLs like this: Write someone a program and you solve their problems for a day. Write them a DSL and you get them off your back for good cuz they can solve their own damn problems.

So how do we represent typed syntax in a type-respecting manner? Cue free monads.

Here's a summary of the capture process in 3 steps:

Gather the type signatures of the IO fragment:

fooIO :: A -> B -> C -> IO X
barIO :: D -> E -> IO Y
quuxIO :: IO Z

Declare the functorial datatype. Obtain the actual free monad by applying the least-fixed point operator to the functor.
```
data BaseF x
   = FooIO A B C (X -> x)
   | BarIO D E (Y -> x)
   | QuuxIO (Z -> x)
type SubIO = Free BaseF
```

Define the syntactic replacements of the IO fragment:

fooIO' :: A -> B -> C -> SubIO X
fooIO' A B C = liftF $ FooIO A B C id

barIO' :: D -> E -> SubIO Y
barIO' D E = liftF $ BarIO D E id

quuxIO' :: SubIO Z
quuxIO' = liftF $ QuuxIO id

So given a function foo of type IO (), it should now be obvious why the free monad encoding should obey

foo' >> m = Free (Foo m)

All the equation's saying is that a foo' command followed by m is represented by a Foo datum attaching the rest of the program m. Duh.

But this is the same equation we saw earlier:

exitSuccess' >> m = Free (ExitSuccess m)

So what's going on with the "Purify code" blog post?

My guess is that the blog fell into a circular reasoning fallacy (but with a hidden twist, see below).

Here's the "Purify code" story Done Right: We—who, unlike the compiler, do understand English and the semantics of the action—know that exitSuccess halts the program. In other words, we know that the native exitSuccess >> m = exitSuccess, and we want it expressly reflected in the free monadic stub exitSuccess' >> m = exitSuccess'. And it turns out that we can perturb the free monad encoding to get this result. We do that by dropping the x parameter in

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

But these perturbations are ad-hoc. Unlike the plug-and-chug of the standard encoding, these detours off the beaten track aren't documented. In fact, I can't recall off the top of my head any other known perturbation.

Most likely, the blog post goofed in the plug-and-chug of the free monad encoding. It stumbled on a useful tweak but didn't recognize it as such.

Even if there were a host of well-documented and well-understood tweaks to choose from—and there isn't—the industry best practice is to keep syntax and semantics separate. The names and their types go into the data structure of the base functor. Their meaning, on the other hand, strictly belong in the interpreter.

Let's reiterate: Sans tweaks, it is correct that the type of exitSuccess' only guarantees that

exitSuccess' >> m = Free (ExitSuccess m)

To ensure that exitSuccess' means exactly what it says on the tin, we must make it so in the interpreter and only in the interpreter:

type SubIO = Free TeletypeF
runInterp :: SubIO r -> IO r
runInterp (Free (ExitSuccess _)) = exitSuccess

Note how the rest of the program—represented by the underscore—is discarded.

If instead, gremlins (see below) burrowed up from the netherworld to cause havoc, the line of code would then read:

runInterp (Free (ExitSuccess m)) = runInterp m

where m stands for the rest of the program. Where the free monadic stub exitSuccess' used to mean halt, it now means no-op. The situation is flipped. This time round, it's the stub that's discarded and the rest of the program that's on the right of the equal sign.

Regardless of gremlins, notice how the interpreter is the El Duce of meaning.

The foregoing also gives the lie to certain egregious claims in "Purify code," namely that

We can't reason about anything in IO; hence,
We can't prove anything in IO.

Of course we can!

Here's how a Haskell programmer does equational reasoning when writing imperative code:

First, we think about what the native IO function exitSuccess means. Well, it stops the program, yes?
To say exitSuccess stops the program is the same as saying: anything that follow exitSuccess is ignored.
So we formalize this understanding into an equation. Namely, regardless of whatFollows, we must have exitSuccess >> whatFollows = exitSuccess.

With this equation, we can prove that the native echo program exhibited in "Purify code":

import System.Exit

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

will never output "Finished". Why? Because the program halts at exitSuccess.

"Purify code" alleges that we cannot prove this because the System.Exit definition of exitSuccess could be changed to a no-op: exitSuccess = return ().

Well, that changes the semantics then, and instead of

exitSuccess >> m = exitSuccess

we get

exitSuccess >> m = m

With the new equation, we can instead prove that

import System.Exit

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

is equivalent to

import System.Exit

main = do
   x <- getLine
   putStrLn x
   -- exitSuccess -- no-op, so commented out
   putStrLn "Finished"

All of these proofs take place expressly in the IO monad, albeit in a small subset. Who says you can't prove things about IO?

Another curious case of circular reasoning occurs later on in "Purify code." It's alleged that we cannot prove that the program prints the same string it receives as input. Just like earlier, the reason given is that putStrLn could be redefined to be a no-op. Then the blog post gives an interpreter of the free monad that avoids IO entirely and has the [String]->[String] function type to show that the interpreter provably produces output same as input.

There are two flaws of reasoning here. The first is the circular one. Correctly coding the interpreter predicates on an imperative understanding of putStrLn and getLine. The blog post ignores the presence of that imperative understanding, and so the interpreter teleports into existence, correct and fully-formed, deus ex machina.

But that's just silly. The hidden hand of imperative understanding is what guides the blog post to a correct interpreter in the first place.

You'll recall that a circular argument assumes its conclusion. Here the argument builds on the opposite of its conclusion. Rare.

The second flaw is an apples-to-oranges comparison. A parallel universe where gremlins redefine putStrLn to be no-op will also see them throw a homomorphic wrench in the free monad interpreter.

The correct interpreter denotes putStrLn' this way:

runPure :: Teletype r -> [String] -> [String]
runPure (Free (PutStrLn y t)) xs = y:runPure t xs

Just like version 1.0 of the gremlins we saw earlier, an interpreter wrecked by a no-op putStrLn' blithely discards the PutStrLn stub:

runPure (Free (PutStrLn y t)) xs = runPure t xs

That's what an apples-to-apples comparison would look like.

It's unfortunate that these errors ruin what is otherwise a decent intro to free monads. For instance, the final part in "Purify code" about QuickCheck-ing the [String] -> [String] interpreter is definitely worth expanding. The immense leverage afforded by QuickCheck—whether or not applied to free monads—deserves to be more widely known.

So are free monads really about purity?

"Pure" is an overloaded adjective with multiple meanings. On the one hand, the academic literature uses it in a technical sense with no value judgments whatsoever. On the other hand, it's heavily connotative of "good" and these connotations skew our apprehension of what is called "pure."

What should be obvious is that free monads don't automagically purify your code and clean them free of bugs.

Free monads don't give you additional type safety over what you already get in unreified Haskell. Although you've just seen a perturbation on the free monad encoding that gains you additional leverage, the fact remains that there's no known theory to guide you in such customizations.

What free monads do is that they allow you to DSL-ize portions of your code into manipulable data structures. This comes at a cost. Neither building the data structure in client code nor unpacking them in the interpreter comes for free. Just like how building a singly-linked list using append operations is inefficient, you would need to learn the Coyoneda transformation to ensure that you don't pay a similar quadratic-time cost for free monads.

Worst of all, you lose out on compiler optimizations. For instance, if you capture the syntax of State-monadic code but don't reimplement in your interpreter any of GHC's advanced transformations that pure, lazy code enjoy; your code will end up slower. Roman Cheplyaka has benchmarked a free monadic encoding of State to be two orders of magnitude slower than native effects (emphasis his).

When considering whether you need free monads, ask yourself, "Do I need a deep DSL? Am I ready to roll—and maintain, and optimize, and debug—my own interpreter for the DSL?"

But you can bet your bottom dollar that free monads aren't some magical cleaning solution. And they definitely won't detox your colon, although whatever the following ad is selling just might:

Kim-Ee Yeoh hacks Haskell for fun, profit, and greater good by reading, writing, learning, and teaching.

No shilling, no snake oil. Your colon will never be harmed. Just advice on how to get good at Functional Programming. There's no risk at all to you if you'd like to receive The Haskell Courant.