Rohit's Blog

Occasional writing on software engineering.

Algebra-Driven Design, Part 1: Design the Algebra Before You Write the Code

scalaapi-design

This post works through the design method from Chapter 1 and Chapter 3 of Algebra-Driven Design by Sandy Maguire, ported to Scala 3. The method is entirely his. The worked example — a retry policy — is mine, and I picked it precisely because I wanted to find out whether the method survives contact with something boring and industrial.

The Scala 3 type system series was about what the language can express. This is the start of a different strand: I read books written for Haskell programmers, and I ask what survives the trip to Scala 3. Sometimes the answer is “all of it, and it’s cleaner here.” Sometimes it’s “none of it, and here’s the exact language feature that’s missing.” Both are worth writing down.

🔗Three things we call abstraction, and a fourth

Ask a room of working programmers what abstraction means and you’ll get some blend of three answers. Maguire lists them in his opening chapter, and I recognised all three as things I’ve said in code review:

  1. Refactoring — pulling duplicated code into a shared function.
  2. Indirection — a thin wrapper around a call, so we can swap the thing behind it later.
  3. Parameterisation — adding knobs, solving the more general problem.

Each of these is a fine thing to do. None of them is what the book is about. Maguire reaches past all three for Dijkstra’s definition, from his 1972 Turing Award lecture:

The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise.

That’s the fourth answer, and it’s a much higher bar. A refactored helper doesn’t create a new semantic level; it just moves code. An abstraction in Dijkstra’s sense gives you a new vocabulary in which you can say true things — and, crucially, in which you cannot say false ones.

The test Maguire proposes for whether you’ve cleared that bar is the one I find genuinely useful: a good abstraction doesn’t need an escape hatch. You never have to reach past it to the thing underneath. You don’t disable instruction pipelining to get your program working. You don’t drop from logic gates to transistors. When a system hands you a back door, it’s admitting the abstraction failed — and now you have to hold two models in your head at once, plus the question of which one is currently lying to you.

🔗Escape hatches in Scala

It would be cheap to make this point with only Haskell examples, so let me name some in the language I actually write. To be clear about the claim: these are all useful and I use them. They’re leaky in Maguire’s narrow, specific sense — the implementation shows through the interface in a way that changes how you have to use them.

Iterator. It has map, filter, foreach, toList. It looks like a collection. It is not a collection — it’s a mutable cursor, and it’s one-shot. Traverse it twice and the second traversal sees nothing. The abstraction says “sequence of values”; the reality is “stateful pointer”, and the type doesn’t tell you which one you’re holding.

Future. The abstraction is “a value that will be available later.” The reality is that it’s already running — construction is the trigger. So you can’t retry a Future, you can only retry the function that makes one. Anyone who has tried to write a generic retry combinator over Future[A] has discovered this the hard way, usually in production. This is exactly why IO and ZIO exist: they close the hatch by making the description of the effect a separate thing from running it.

Effects that don’t appear in types at all. def getUser(id: UserId): User can throw, block, log, write to a database, and return null. The signature admits none of it. This is the largest escape hatch in the language, and every equational argument I make for the rest of this post quietly depends on my not using it.

Hold onto that last one. It comes back at the end.

🔗The vocabulary: constructors, laws, observations

Here’s the machinery, in the book’s terms.

Constructors build values of your type. Some are terminal — they make a value out of nothing. Some are inductive — they make a new value from existing ones.

Observations are the only way information gets out. They’re functions whose argument is your type and whose result isn’t.

Laws are equations relating constructors to each other and to the observations. Not tests — equations. Maguire is emphatic on this distinction and I’ve come around to it: a test implies the possibility of failure, but these are meant to be facts about the domain that you have no power to change. If you decide cw means “rotate 90° clockwise”, then cw ∘ cw ∘ cw ∘ cw = id is forced on you. You didn’t choose it. Geometry did.

The payoff of setting things up this way is a definition of equality that costs nothing and buys a lot:

Two values are equal if and only if no observation can tell them apart.

This is observational equality, and it’s the load-bearing idea in the whole method. It means your implementation is free to represent things however it likes — two structurally different values are the same value as long as every observation agrees. Which in turn means you can replace the implementation wholesale, later, without anyone noticing.

🔗A worked example: retry policies

Enough theory. Let’s design something small.

I want a retry policy: the thing that sits between “this call failed” and “try it again in 400 milliseconds.” Every backend codebase has one. Most of them are a tangle of maxAttempts, initialDelay, multiplier, and maxDelay fields with implicit rules about how they interact that live only in the author’s head.

The method says: don’t start there. Start with the observation.

🔗Step 1 — what is this thing, actually?

What does a retry policy mean? It means a sequence of delays. That’s all. Attempt, wait, attempt, wait, until you stop.

// scala-check: skip
def delays(p: RetryPolicy): LazyList[FiniteDuration]

That’s the observation, and it’s the only one. LazyList because a policy may retry forever, and an empty list means “don’t retry at all.” Everything I say from here has to be said in terms of delays.

Notice I’ve written no implementation. RetryPolicy is an abstract type. That’s deliberate, and per the book it should stay that way as long as possible — the moment you pick a representation, it starts making design decisions on your behalf.

🔗Step 2 — constructors

Two terminal constructors and one more to make it interesting:

// scala-check: skip
val never: RetryPolicy
def constant(d: FiniteDuration): RetryPolicy
def exponential(base: FiniteDuration): RetryPolicy

And some inductive ones — ways to build a policy from a policy:

// scala-check: skip
extension (p: RetryPolicy)
  def upTo(n: Int): RetryPolicy
  def cappedAt(max: FiniteDuration): RetryPolicy
  def andThen(q: RetryPolicy): RetryPolicy

upTo limits the number of retries. cappedAt limits the length of each delay. They sound like siblings. Keep an eye on them.

🔗Step 3 — laws

Now the actual work, and none of it involves a compiler.

Each constructor gets a law explaining it in terms of the observation:

delays(never)          = LazyList.empty
delays(constant(d))    = LazyList.continually(d)
delays(p.upTo(n))      = delays(p).take(n)
delays(p.cappedAt(m))  = delays(p).map(d => if d < m then d else m)
delays(p.andThen(q))   = delays(p) ++ delays(q)

And then — this is the part that pays — laws relating constructors to each other, with no observation in sight:

p.upTo(0)                 = never
p.upTo(m).upTo(n)         = p.upTo(min(m, n))
p.cappedAt(a).cappedAt(b) = p.cappedAt(min(a, b))

never.andThen(p)          = p
p.andThen(never)          = p
p.andThen(q).andThen(r)   = p.andThen(q.andThen(r))

Read those last three again. andThen is associative and never is its identity on both sides — which means RetryPolicy is a monoid under andThen, and I get that for free in a design I’ve spent fifteen minutes on. Practically, it means I can hand users a combineAll over a list of policies, and I can reassociate however I like when optimising, and neither can change what a program means.

Then there’s this one, which I did not see coming:

constant(d).andThen(p)    = constant(d)

An infinite policy annihilates whatever follows it. Obvious in hindsight — you never reach the second policy — but I’d never have thought to write it as a fact, and if I’d built this the normal way I’d have shipped an API where andThen silently does nothing in a case users will absolutely hit.

🔗Step 4 — the law that isn’t there

Now back to upTo and cappedAt. cappedAt distributes over andThen:

p.andThen(q).cappedAt(m) = p.cappedAt(m).andThen(q.cappedAt(m))

Does upTo? Try it:

p.andThen(q).upTo(n) ≠ p.upTo(n).andThen(q.upTo(n))

It doesn’t, and it isn’t close — the right-hand side can produce up to 2n delays. Two combinators that read like siblings in the API docs behave completely differently under composition, and the algebra found that before I wrote a line of implementation. In the normal workflow I’d have found it via a bug report about a service retrying twice as long as its configured budget.

That, for me, is the moment the method justified itself.

🔗Step 5 — and now the implementation writes itself

Here’s the punchline, and it’s Maguire’s recipe from the tile chapter applied verbatim: find the observation from which everything else follows, move your type to the first parameter, then delete it.

delays: RetryPolicy => LazyList[FiniteDuration]
                  ↓  drop the first parameter
        RetryPolicy = LazyList[FiniteDuration]

The denotation is the implementation:

import scala.concurrent.duration.FiniteDuration

opaque type RetryPolicy = LazyList[FiniteDuration]

object RetryPolicy:
  val never: RetryPolicy = LazyList.empty
  def constant(d: FiniteDuration): RetryPolicy = LazyList.continually(d)
  def exponential(base: FiniteDuration): RetryPolicy = LazyList.iterate(base)(_ * 2L)

extension (p: RetryPolicy)
  def delays: LazyList[FiniteDuration] = p
  def upTo(n: Int): RetryPolicy = p.take(n)
  def cappedAt(max: FiniteDuration): RetryPolicy = p.map(d => if d < max then d else max)
  def andThen(q: RetryPolicy): RetryPolicy = p #::: q

Every law becomes a fact about LazyList that I already knew: xs.take(m).take(n) = xs.take(min(m, n)). And the missing distributive law becomes obvious on sight — (xs ++ ys).take(n) is plainly not xs.take(n) ++ ys.take(n).

opaque type is doing real work here. It’s the final encoding with zero runtime cost and a genuinely sealed boundary: outside this file, RetryPolicy is not a LazyList, so nobody can reach past my algebra into the representation. No escape hatch. If I later decide this should be a state machine for performance reasons, no caller changes.

🔗Step 6 — machine-check the laws

The laws are the specification, so they should be executable. And observational equality tells me exactly how to compare two infinite policies — by observing a prefix:

// scala-check: skip
import org.scalacheck.*, Prop.forAll

def observationallyEqual(p: RetryPolicy, q: RetryPolicy): Prop =
  forAll(Gen.chooseNum(0, 100)) { n =>
    p.delays.take(n).toList == q.delays.take(n).toList
  }

property("upTo/upTo") = forAll { (p: RetryPolicy, m: Int, n: Int) =>
  observationallyEqual(p.upTo(m).upTo(n), p.upTo(m min n))
}

property("andThen is associative") = forAll { (p: RetryPolicy, q: RetryPolicy, r: RetryPolicy) =>
  observationallyEqual(p.andThen(q).andThen(r), p.andThen(q.andThen(r)))
}

== on two infinite LazyLists would hang forever. Observational equality is what makes the test terminate, and that’s not a testing trick — it’s the definition of equality falling out of the design and doing useful work.

🔗The workflow, and what it costs

The full method has three phases:

  1. Design the algebra. Constructors, observations, laws. No implementation. This is where you actually think.
  2. Initial encoding. A dumb, obviously-correct implementation — an ADT mirroring your constructors, interpreted by pattern matching. Slow and unquestionably right. Generate a property-test suite against it.
  3. Efficient encoding. Derive a fast implementation. The suite from phase 2 guarantees nobody can tell.

My retry example collapsed phases 2 and 3 because the denotation was already efficient. That won’t usually happen, and the rest of this series works through a case where it doesn’t — Henderson’s tile algebra, four posts, ending in fractals.

Now the honest part, because a manifesto post that only lists benefits isn’t worth much.

It’s slow at the start and it feels unproductive. I spent an afternoon on something I’d normally throw together before lunch. There is nothing to run and nothing to demo. If you work somewhere that measures progress in merged PRs, this is a hard sell, and Maguire’s suggested framing — that these are inconsistencies you’d hit anyway, only later and more expensively — is true but not always persuasive at 4pm on a Thursday.

It’s a library-design method, not an application-design method. The book is upfront about this. It works when you’re building something reusable with a real interface. It has little to say about wiring up an HTTP handler.

And the deepest caveat is Scala-specific. Every law I wrote assumes referential transparency. p.andThen(q).andThen(r) = p.andThen(q.andThen(r)) is only true if none of these expressions can throw, block, mutate, or log. Haskell’s type system enforces that precondition. Scala’s does not — it’s a matter of my discipline, and the compiler will not tell me when I break it. So the method transfers, but it transfers with a load-bearing assumption that in Haskell is free and in Scala is homework.

That’s the first entry in what I suspect will be a long list, and it’s why I’m reading these books at all. Not to write Haskell. To find out which of my Scala habits are choices and which are consequences.

Conal Elliott, whose work on denotational design underpins Maguire’s book, put the trade plainly back in 2009: the discipline costs you up-front effort in clarity of thinking, much as static typing does, and pays you back in designs that feel less invented than discovered.

After one afternoon and one retry policy, I think that’s about right.

Next: Part 2 — Designing the tile algebra, in which we spend an entire post writing equations about pictures and never once run the compiler.

🔗Sources

  • Maguire, Sandy. Algebra-Driven Design: Elegant Software from Simple Building Blocks. 2020. Chapters 1 and 3. https://leanpub.com/algebra-driven-design — the method, the constructor/observation/law vocabulary, the escape-hatch test, and the denotation-to-implementation recipe are all his. Buy the book; this post is a signpost, not a substitute.
  • Dijkstra, Edsger W. The Humble Programmer (EWD340), Turing Award lecture, 1972 — the definition of abstraction the book builds on.
  • Elliott, Conal. Denotational design with type class morphisms. 2009 — the “reason through the observations” method that Chapter 5 of Algebra-Driven Design develops, and the source of the closing observation about up-front effort.
  • Claessen, Koen & John Hughes. QuickCheck: a lightweight tool for random testing of Haskell programs. ICFP 2000 — the ancestor of ScalaCheck, used above.

The retry-policy algebra, its laws, and the Scala 3 code are mine, derived by following Maguire’s method.