Rohit's Blog

Following “Data Types à la Carte” by Wouter Swierstra (JFP 2008). Part 1 built expressions as fixed points of a signature functor, and found that Scala 3’s union types make the paper’s injection machinery unnecessary — :≺: becomes <:<, and the injections become identity.

That was the win. This is the bill.

🔗Folding over a fixed point

Both signatures are functors: you can map a function over the sub-expression slots.

trait Functor[F[_]]:
  def map[A, B](fa: F[A])(f: A => B): F[B]

given Functor[Val] with
  def map[A, B](fa: Val[A])(f: A => B): Val[B] = Val(fa.n)

given Functor[Add] with
  def map[A, B](fa: Add[A])(f: A => B): Add[B] = Add(f(fa.l), f(fa.r))

Val ignores the function because it has no sub-expressions; Add applies it to both.

And the coproduct of two functors is a functor — map over whichever side you have.

Once a signature is a functor, you get a fold for free:

def fold[F[_], A](e: Fix[F])(alg: F[A] => A)(using F: Functor[F]): A =
  alg(F.map(e.unfix)(fold(_)(alg)))

Recurse into the children, then apply alg to the resulting layer. That function is a catamorphism, and its argument is an algebra: a function F[A] => A saying how one layer contributes to the answer, with the recursion already done.

The important property is that an algebra is not recursive. Add’s case receives two Ints, not two expressions. So an algebra for a signature is genuinely independent of the rest of the language — which is what makes assembling them possible at all.

🔗Assembling algebras in Haskell

The paper’s approach is a type class per function you want to write:

a class whose method is the algebra for evaluation — one layer of Ints to an Int;
an instance for Val, returning the literal;
an instance for Add, adding the two already-evaluated children;
and one recursive instance for the coproduct, which simply dispatches to whichever side the value came from.

That last instance is the whole trick, and it’s four words long: if you can evaluate f and you can evaluate g, you can evaluate f :+: g. Evaluation is then a fold with that algebra, and it works for any signature built from pieces that have instances.

It’s a beautiful piece of design. Note especially that the coproduct instance doesn’t distinguish Inl from Inr — the paper leans on this later to argue that the ambiguity in its overlapping injection instances is harmless, because nothing downstream can observe which injection was chosen.

🔗In Scala: the shape is fine, the resolution is the question

The typeclass translation is mechanical:

trait Eval[F[_]]:
  def alg(fa: F[Int]): Int

given Eval[Val] with
  def alg(fa: Val[Int]): Int = fa.n

given Eval[Add] with
  def alg(fa: Add[Int]): Int = fa.l + fa.r

Now the coproduct instance. Our coproduct is a type lambda, so:

given [F[_], G[_]](using F: Eval[F], G: Eval[G]): Eval[[A] =>> F[A] | G[A]] with
  def alg(fa: F[Int] | G[Int]): Int = fa match
    case f: F[Int] @unchecked => F.alg(f)
    case g: G[Int] @unchecked => G.alg(g)

And here we hit the two problems that make this post’s title what it is.

🔗Problem one: you can’t match on an untagged union

Part 1 sold untagged unions as pure upside — no wrappers, no injections, subtyping does the work. The flip side arrives now. To dispatch, you must recover which side you have, and an untagged union carries no tag to tell you.

At the call site for concrete signatures this is fine, because Val and Add are distinct classes and a runtime type test distinguishes them:

fa match
  case v: Val[Int] => v.n
  case a: Add[Int] => a.l + a.r

But in the generic instance above, F and G are abstract. There is no class to test against, and erasure means case f: F[Int] cannot compile into anything meaningful — hence the @unchecked, which is a promise you cannot keep.

The principled fix is a TypeTest, threaded as another constraint:

given [F[_], G[_]](using
  F: Eval[F], G: Eval[G], tt: TypeTest[F[Int] | G[Int], F[Int]]
): Eval[[A] =>> F[A] | G[A]] with
  def alg(fa: F[Int] | G[Int]): Int = fa match
    case tt(f) => F.alg(f)
    case other => G.alg(other.asInstanceOf[G[Int]])

which is honest but now demands a TypeTest at every signature, for every algebra, at every result type. The paper’s four-word instance has become a constraint-threading exercise.

Haskell doesn’t have this problem because its coproduct is tagged. Inl and Inr are runtime evidence. Scala’s union threw that evidence away in exchange for making injection free.

🔗Problem two: will the given even be found?

The deeper question, and the one I want to be straight about: given a required Eval[[A] =>> Val[A] | Add[A]], will Scala’s given resolution match it against a given declared for Eval[[A] =>> F[A] | G[A]]?

That requires the compiler to unify a concrete type lambda with an abstract one, solving F := Val and G := Add by decomposing a union inside a lambda body. Scala 3 can unify type lambdas in some circumstances; higher-kinded unification is deliberately restricted, and matching structurally through a union is exactly the sort of thing I’d expect to be brittle.

I don’t know whether this resolves, and I couldn’t check. There’s no JVM on the machine I drafted this on. Everything in part 1 was reasoned from subtyping, which I’m confident about; this is a question about the implementation of given resolution, which is not the kind of thing you should take on trust from someone who hasn’t run it.

If you try it, this is the first thing to try, and I’d genuinely like to know the answer. My expectation is that it fails or requires enough coaxing to defeat the purpose — but I’ve been wrong about Scala 3’s inference in both directions before.

🔗The thesis

Assume the pessimistic answer. What’s the actual lesson?

Look at what each encoding is good at.

Injection wants subtyping. “Is this signature somewhere in that one?” is a question about containment, and a subtype lattice answers it directly, associatively, and without search. That’s why part 1 went so well: <:<, no instances, no nesting limitation.

Algebra assembly wants structure. “Build an interpreter for F | G from interpreters for F and G” is induction over the shape of the type. It needs the type to have a shape you can recurse on, and it needs values to carry evidence of which branch they took.

A tagged coproduct is a two-element structure: it has a left and a right, at the type level and at the value level. Induction over it is trivial and dispatch is free. An untagged union is a set — idempotent, commutative, associative — and those are exactly the properties that make containment easy and induction impossible. Val | Add doesn’t have a left and a right any more than {1, 2} does.

So the two halves of the paper want opposite things, and no single encoding gives you both. Haskell picks structure and pays for injection with an extension and a documented limitation. Scala’s unions pick subtyping and get injection for free — and now have to find structure somewhere else.

That’s a more interesting result than “Scala wins”, and I’d rather have it.

🔗Where the structure could come from

If unions can’t be inducted over, put the induction somewhere that can be. Scala 3 has a type-level list with exactly the right shape — Tuple, with *: and EmptyTuple:

type Sig = (Val, Add, Mul)     // the menu, as a tuple of signatures

A tuple is structurally recursive, so an Eval instance can be derived by induction over it — head and tail, base case at EmptyTuple — which is the same machinery behind typeclass derivation via Mirror.

The hybrid that suggests itself: use a Tuple of signatures as the type-level menu (so algebras can be assembled by induction), and a union as the value-level representation (so injection stays free), with a function from the tuple to the corresponding union type. Containment becomes tuple membership, which is a match type; interpretation becomes induction over the tuple.

I think that’s the right shape and I want to be clear it’s a sketch, not a result — I haven’t built it, and the interesting difficulties would all be in the details. Someone has probably already done it; the Scala ecosystem has had shapeless and then Mirror-based derivation solving adjacent problems for years.

🔗Meanwhile, the pragmatic answer

If you wanted this working in Scala today, the boring option is to stop being clever and use the tagged coproduct, exactly as the paper does:

enum :+:[F[_], G[_], A]:
  case Inl(fa: F[A])
  case Inr(ga: G[A])

Now everything from the paper ports directly. The recursive Eval instance is four words again, because Inl and Inr are real constructors you can match on. Given resolution has an ordinary ADT to work with, not a type lambda over a union.

And you’re back to needing the injection machinery — a Sub[F, G] typeclass with the same three instances. Scala’s given prioritisation by specificity handles the overlap more gracefully than Haskell’s OverlappingInstances flag, which is a small consolation.

That’s the trade in one sentence: untagged unions make part 1 free and part 2 hard; tagged coproducts make part 1 work and part 2 free.

🔗Next

Whichever encoding you pick, once evaluation is assembled from pieces you get the thing the paper is actually selling: adding multiplication to the language, with a new interpreter case, without touching a single existing line.

That’s the payoff, and it’s worth seeing in full.

Next: Part 3 — Adding cases without touching code.

🔗Sources

Swierstra, Wouter. Data Types à la Carte. JFP 18(4), 423–436, 2008. The fold over fixed points, the algebra-as-type-class technique, the instances for Val and Add, and the recursive instance for coproducts are all his. Available from the author.
Meijer, Fokkinga & Paterson (1991) for catamorphisms; Liang, Hudak & Jones (1995) on modular interpreters, which the paper credits as the ancestor of its subtyping class.

The Scala 3 translation, the analysis of why untagged unions defeat algebra assembly, and the Tuple-as-menu sketch are mine — and the given-resolution question is genuinely open, not rhetorical.