Rohit's Blog

The last of four, following “Data Types à la Carte” by Wouter Swierstra (JFP 2008). Parts 1, 2 and 3 assembled a data type and its interpreters from independent pieces.

The paper’s final movement applies the same machinery to monads, and it’s the part with the longest afterlife. If you have written Scala with Free, or seen EitherK and wondered what it was for, you have been using this pearl. Most people using it don’t know that.

🔗One small change to the data type

Recall the expression type: a layer of signature F, recursively.

Add one case — a way to stop and return a value:

enum Term[F[_], A]:
  case Pure(a: A)
  case Impure(fa: F[Term[F, A]])

A term is either a finished value, or one layer of effect wrapping the rest of the computation.

That’s the whole change, and it’s enough to get a monad. When F is a functor, Term[F, *] is one: pure is Pure, and flatMap walks down to the leaves and grafts the continuation on:

given [F[_]](using F: Functor[F]): Monad[[A] =>> Term[F, A]] with
  def pure[A](a: A): Term[F, A] = Term.Pure(a)
  def flatMap[A, B](t: Term[F, A])(f: A => Term[F, B]): Term[F, B] = t match
    case Term.Pure(a)    => f(a)
    case Term.Impure(fa) => Term.Impure(F.map(fa)(flatMap(_)(f)))

These are free monads — free in the technical sense of being left adjoint to the forgetful functor from monads to their underlying functors.

The consequence that matters for this series is one line of category theory with an immediate practical payoff: left adjoints preserve coproducts. So the coproduct of two free monads is the free monad of the coproduct of their signatures — which is exactly the thing we already know how to build.

Monads are famously awkward to combine. Free monads are the special case where combining them is just combining functors, and we did that in part 1.

The paper is careful to say the trick doesn’t generalise: most monads aren’t free. Lists aren’t; state isn’t. Identity, Maybe and error monads are.

🔗A calculator with a memory cell

The example is a calculator with a memory: increment it, or read it.

final case class Incr[T](by: Int, next: T)
final case class Recall[T](next: Int => T)

Incr carries the amount and the rest of the computation. Recall carries a function from the memory’s contents to the rest — because what happens next depends on what was read. That asymmetry is the shape of every effect signature you’ll ever write: outputs are arguments, inputs are functions.

Smart constructors, in the style of part 1:

def incr[F[_]](i: Int)(using ev: Incr[Term[F, Unit]] <:< F[Term[F, Unit]]): Term[F, Unit] =
  Term.Impure(ev(Incr(i, Term.Pure(()))))

def recall[F[_]](using ev: Recall[Term[F, Int]] <:< F[Term[F, Int]]): Term[F, Int] =
  Term.Impure(ev(Recall(Term.Pure(_))))

And now the payoff — a program in for-notation, exactly as if it were ordinary state:

def tick[F[_]](using ...): Term[F, Int] =
  for
    y <- recall
    _ <- incr(1)
  yield y

tick reads the memory, bumps it, and returns the old value. It reads like State, and it isn’t: it’s an inert value describing a computation.

🔗Running it

Interpretation is a fold, same as part 2 — one function for the pure case, one algebra for the effect layer:

def foldTerm[F[_]: Functor, A, B](t: Term[F, A])(pure: A => B)(alg: F[B] => B): B =
  t match
    case Term.Pure(a)    => pure(a)
    case Term.Impure(fa) => alg(summon[Functor[F]].map(fa)(foldTerm(_)(pure)(alg)))

The target is a state transition, so the algebra turns a layer of state-transitions into a state-transition:

opaque type Mem = Int

trait Run[F[_]]:
  def alg(fa: F[Mem => (A, Mem)]): Mem => (A, Mem)   // for a fixed A

given Run[Incr] with
  def alg(fa: Incr[Mem => (A, Mem)]) = m => fa.next(m + fa.by)

given Run[Recall] with
  def alg(fa: Recall[Mem => (A, Mem)]) = m => fa.next(m)(m)

Incr bumps the memory and continues; Recall passes the current value to the continuation and leaves the memory alone. Plus the coproduct case, with all of part 2’s caveats about how that’s spelled in Scala.

Run tick starting from 4 and you get back 4, with the memory now 5.

🔗Why bother, when `State` exists?

The obvious objection, and the paper answers it in a sentence I keep coming back to: once the program is a value, its type says something about its behaviour.

A Term[Recall, *] computation cannot modify memory — not by convention, not by review, but because Incr isn’t in its signature. A Term[Incr, *] computation produces the same answer regardless of the starting memory. Write the same logic directly in State[Mem, *] and both distinctions vanish; every computation has the same type and could do anything.

That’s the argument, and it generalises immediately.

🔗Structuring IO

The application the paper closes on, and the reason this pearl mattered.

Haskell’s IO had become — the paper’s phrase — a sin bin, holding every side effect there is. The type IO () tells you a program does something. It doesn’t tell you whether that something is printing a character or deleting your home directory.

So: signatures per family of effect.

enum Teletype[A]:
  case GetChar(next: Char => A)
  case PutChar(c: Char, next: A)

enum FileSystem[A]:
  case ReadFile(path: String, next: String => A)
  case WriteFile(path: String, contents: String, next: A)

Interpret them by an algebra mapping each constructor to the real primitive — a natural transformation from your signature into IO, or Future, or a test harness that returns canned input.

And now a program’s type is a manifest:

def cat(path: String): Term[Teletype :+: FileSystem, Unit]

This program reads files and writes to the terminal. It cannot delete anything, open a socket, or read the clock, and you know that from the signature without reading the body. A Term[Teletype, *] provably will not touch your disk.

Swierstra adds a second benefit that’s easy to miss: the terms are ordinary pure values, which means you can inspect them, test them against a fake interpreter, log them, or serialise them. An effectful program becomes a data structure you can do arithmetic on.

🔗You have been using this paper

Here’s the part I most wanted to write.

Open cats and look at what’s there:

The paper	cats
`Term f a` (free monad)	`cats.free.Free[S[_], A]`
`f :+: g` (coproduct of signatures)	`cats.data.EitherK[F[_], G[_], A]`
`sub :≺: sup` (injection class)	`cats.InjectK[F[_], G[_]]`
the algebra passed to `foldTerm`	`cats.arrow.FunctionK`, written `~>`
`foldTerm`	`Free#foldMap`

The entire paper is in the standard Typelevel library, under different names, and has been for a decade. EitherK is the tagged coproduct from part 1 — tagged, note, which is precisely the pragmatic choice part 2 concluded you’d end up making. InjectK is the subtyping class, overlapping instances and all, transliterated into givens.

Every Scala tutorial that builds a free-monad DSL — define an algebra as a sealed trait, lift it with liftF, combine two DSLs with EitherK, interpret with a ~> into IO — is reproducing this pearl. I’d used all of it without ever having read the source, and I suspect that’s common.

Which reframes the value of reading the paper. Not to learn a technique you’ll implement, but to understand why the library is shaped the way it is — why InjectK has the instances it has, why coproducts nest to the right, why the interpreter is a natural transformation rather than an ordinary function.

🔗Free monads, tagless final, and `ZIO[R, E, A]`

Worth closing on, because Scala has three answers to “make the type say which effects you use” and this paper is the ancestor of one of them.

Free monads. The program is a data structure; the interpreter is separate. You can inspect, transform and optimise programs before running them. The costs are real: allocation per step, and — the reason most Scala shops moved away — the types get unwieldy fast once you have four or five effects in one coproduct.

Tagless final. Abstract over the effect type, constrain it with capability traits. This is what Lava was doing in 1998, and it’s cheaper at runtime because there is no intermediate structure. You give up the ability to inspect the program, because the program is the calls.

ZIO[R, E, A]. Put the requirements in a type parameter and let the environment carry capabilities. Different trade again: no free structure, no typeclass plumbing, and a concrete runtime.

All three are answers to the question this paper asked, which is the point I’d leave you with. The paper didn’t propose an effect system; it observed that a monolithic IO type is a design failure and showed that coproducts of functors can fix it. Everything after is engineering on that observation.

🔗Where the series landed

I started this series expecting a clean “Scala 3 wins”, and got something better.

Part 1 was the win. Union types make the paper’s injection machinery unnecessary. :≺: becomes <:<, discharged by the subtype checker; no overlapping instances, no extension, and the paper’s documented limitation about left-nested coproducts simply doesn’t arise.

Part 2 was the bill. The same untagged-ness that makes injection free makes algebra assembly hard, because dispatch needs a tag and induction needs a structure, and a union is a set rather than a pair. Injection wants subtyping; algebra wants structure; no one encoding gives you both.

Part 4 is the epilogue, which is that the Scala ecosystem worked this out years ago and shipped the tagged version. EitherK isn’t a failure of imagination — it’s the right answer to the trade-off part 2 identified, arrived at by people building things rather than writing blog posts about them.

And the standing caveat: none of this series has been compiled. The <:< argument in part 1 is ordinary subtyping and I’m confident in it. The given-resolution question in part 2 is genuinely open, and it’s the first thing I’d check. As ever, I’d rather flag the gap than present reasoning as a result.

🔗Sources

Swierstra, Wouter. Data Types à la Carte. Journal of Functional Programming 18(4), 423–436, 2008. The Term free monad and its instances, the observation that left adjoints preserve coproducts, the calculator with Incr/Recall, foldTerm and the Run algebra, the Teletype/FileSystem signatures, and the argument that a program’s type should constrain its effects are all his. Available from the author.
Awodey, Steve. Category Theory. Oxford, 2006 — cited by the paper for free constructions.
Lüth, Christoph & Neil Ghani. Composing monads using coproducts. 2002 — on why the general case is hard.
cats (Typelevel) — Free, EitherK, InjectK, FunctionK: this paper, shipped.

The Scala 3 translation, the mapping onto cats, and the comparison with tagless final and ZIO are mine.