Algebra-Driven Design, Part 2: Designing the Tile Algebra
This post works through the tile algebra from Chapter 2 of Algebra-Driven Design by Sandy Maguire, ported to Scala 3. Maguire credits the algebra itself to Peter Henderson’s Functional Geometry (1982) — the paper that recreates Escher’s Square Limit from a handful of combinators. So the design is Henderson’s, the method is Maguire’s, and the Scala is mine.
Part 1 laid out the method: constructors, observations, laws, and only then an implementation. That post used a retry policy — small enough to fit in one sitting. The next four use something bigger, and with pictures.
By part 5 we’ll be generating fractals. In this post we won’t write a single line of executable code.
🔗The scope
We want a library for building images by recursively subdividing space. Square tiles, which can be rotated, mirrored, and composed side by side or one above the other.
Two things to notice about that sentence, both of which Maguire flags as prerequisites for the method working at all:
The goal is usability-based, not implementation-based. We want to produce images, not PNGs. PNG is a lossy encoding of an image — save a half-size render and you can’t get the detail back. Keeping “image” as the thing we’re designing leaves the door open to resolution-independence, and in part 5 that door turns out to matter enormously.
We have no implementation in mind. This is harder than it sounds. My instinct, three
seconds in, was Array[Array[Int]]. Committing to that would have quietly decided several
design questions for me, and — as we’ll see in part 5 — decided them wrong.
🔗Terminal constructors
Start with the ability to get an image in at all:
// scala-check: skip
def fromImage(path: Path): Tile
And a solid colour:
// scala-check: skip
def colour(r: Double, g: Double, b: Double, a: Double): Tile
Nothing in the type stops you passing r = 17.4. So constrain it with a law:
colour(r, g, b, a) = colour(clamp(r), clamp(g), clamp(b), clamp(a))
That’s the first thing worth pausing on. In the normal workflow, “channels are clamped to [0,1]” is a sentence in a scaladoc comment that may or may not still be true. Here it’s an equation, and in part 4 it becomes an executable property test. The specification can’t drift from the code, because the specification is the test.
🔗Rotation, and where laws come from
Rotate a tile 90° clockwise:
// scala-check: skip
def cw(t: Tile): Tile
Now: what makes this “rotate by 90°” rather than “rotate by some amount”? Do it four times and you’re back where you started:
cw(cw(cw(cw(t)))) = t
That’s the defining characteristic. If it took five applications to get home, cw would
be a 72° rotation. The law isn’t documentation of the behaviour — it’s the closest thing we
have to a definition of it.
And this is the part of Maguire’s framing that shifted how I think. This law was not a design decision. Once I said the word “rotate”, geometry handed me the equation and I had no say in it. The design work is choosing the vocabulary; the laws are then forced, and finding them is closer to discovery than invention.
Counter-clockwise, and its relationship to cw:
// scala-check: skip
def ccw(t: Tile): Tileccw(cw(t)) = t
cw(ccw(t)) = t
We don’t strictly need ccw — three clockwise turns is a counter-clockwise turn. But
ccw(t) reads better than cw(cw(cw(t))), and offering both is safe precisely because we
wrote the law down. Two ways to say the same thing is normally two places for a bug; with an
equation connecting them, it’s just convenience.
Here’s the first derivation. We never stated ccw(t) = cw(cw(cw(t))), but it follows:
ccw(t)
= ccw(cw(cw(cw(cw(t))))) -- cw⁴ = id, applied right-to-left
= cw(cw(cw(t))) -- ccw ∘ cw = id
Grade-school algebra: substitute equals for equals, cancel. In part 4 this derivation becomes
the implementation of ccw.
🔗Mirroring
// scala-check: skip
def flipH(t: Tile): Tile
Horizontal mirroring — flip about the vertical axis, so left and right swap.
It’s its own inverse:
flipH(flipH(t)) = t
Now the interesting one. Picture mirroring a tile, rotating it 180°, and mirroring it back. The two mirrors cancel out around a rotation that’s symmetric in both axes:
flipH(cw(cw(flipH(t)))) = cw(cw(t))
And a little more mental geometry gives the law I find genuinely surprising every time — mirroring a rotation is the same as rotating a mirror the other way:
flipH(cw(t)) = ccw(flipH(t))
Maguire calls this x-symmetry. It’s the law that does the most work later on, because
it’s what lets you push a flipH through a stack of rotations and out the other side.
Vertical flip we get for free — rotate, flip horizontally, rotate back:
// scala-check: skip
def flipV(t: Tile): TileflipV(t) = ccw(flipH(cw(t)))
Is flipV its own inverse? We don’t have to assert it. We can derive it:
flipV(flipV(t))
= ccw(flipH(cw(flipV(t)))) -- flipV
= ccw(flipH(cw(ccw(flipH(cw(t)))))) -- flipV again
= ccw(flipH(flipH(cw(t)))) -- cw ∘ ccw = id
= ccw(cw(t)) -- flipH ∘ flipH = id
= t -- ccw ∘ cw = id
Five lines, no code, no tests, no compiler. And here’s the one I like best — flipping both ways is a half-turn:
flipV(flipH(t))
= ccw(flipH(cw(flipH(t)))) -- flipV
= ccw(ccw(flipH(flipH(t)))) -- x-symmetry
= ccw(ccw(t)) -- flipH ∘ flipH = id
= cw(cw(t)) -- ccw² = cw² , from cw⁴ = id
I did not know that when I started writing this section. The algebra told me.
🔗Composition, and the swap that catches everyone
Now the interesting part — putting tiles together.
// scala-check: skip
def beside(left: Tile, right: Tile): Tile
Tiles are square, and two squares side by side make a rectangle, which isn’t a tile. So we close the operation by subdividing: split the square into two half-width halves and squash a tile into each. Every operation must take valid inputs to valid outputs; that closure requirement is what forces the design, not an arbitrary choice.
What law relates beside to what we have? beside works along the x-axis, so look for
laws that involve the x-axis. flipH also works along the x-axis. Mirror a
side-by-side pair, and:
flipH(beside(t1, t2)) = beside(flipH(t2), flipH(t1))
The arguments swap. Of course they do — mirroring the whole thing puts the right tile on
the left. But I’d have written beside(flipH(t1), flipH(t2)) without thinking, shipped it,
and found out from a screenshot.
This is my second-favourite thing about the method, after the derivations. Writing the law forces you to actually think about the semantics of the operation for thirty seconds, and thirty seconds is usually enough.
Vertical composition:
// scala-check: skip
def above(top: Tile, bottom: Tile): Tileabove(t1, t2) = cw(beside(ccw(t1), ccw(t2)))
And the law connecting the two — a stack of pairs is a pair of stacks:
above(beside(a, b), beside(c, d)) = beside(above(a, c), above(b, d))
Four tiles in a square is common enough to name:
// scala-check: skip
def quad(a: Tile, b: Tile, c: Tile, d: Tile): Tilequad(a, b, c, d) = above(beside(a, b), beside(c, d))
And a quad where one tile rotates a quarter-turn at each position, producing a pinwheel:
// scala-check: skip
def swirl(t: Tile): Tileswirl(t) = quad(t, cw(t), ccw(t), cw(cw(t)))
An aside on the source. The book gives
swirltwo different definitions —quad(t, cw t, cw(cw t), ccw t)in Chapter 2 andquad(t, cw t, ccw t, cw(cw t))in Chapter 5. Only the second produces an actual pinwheel: readingquadas (top-left, top-right, bottom-left, bottom-right), you want the rotation to increase as you travel around the square, which means the bottom-left getsccwand the bottom-right gets the half-turn. I’ve used the Chapter 5 version. Mentioning it because “the book contradicts itself and here’s how I decided” is the sort of thing I’d have wanted someone to tell me.
Finally, layering:
// scala-check: skip
def behind(back: Tile, front: Tile): Tilebehind(t, colour(r, g, b, 1.0)) = colour(r, g, b, 1.0) -- fully opaque front hides all
behind(t, colour(r, g, b, 0.0)) = t -- fully transparent front does nothing
That second law says colour(_, _, _, 0) is a right identity for behind. An identity
element is always worth naming:
// scala-check: skip
val empty: Tilecolour(r, g, b, 0.0) = empty
File that away. In part 3 it turns into something much bigger than a convenience.
🔗Observations, and what equality means
We have a pile of constructors and no way to get anything out. That’s an observation — a function out of the algebra:
// scala-check: skip
def rasterize(width: Int, height: Int, t: Tile): Vector[Vector[Colour]]
Row-major grid of pixels, at whatever resolution you ask for. And now the definition that makes the whole thing work:
∀ w h. rasterize(w, h, t1) == rasterize(w, h, t2) ⟹ t1 = t2
Two tiles are equal if and only if they rasterize identically at every size.
We can’t use structural equality — t and cw(cw(cw(cw(t)))) are different trees and the
same tile. Observational equality is what lets flipV ∘ flipH and cw ∘ cw be genuinely
the same value while being built completely differently. It’s also what will let us throw
away our entire implementation in part 5 and replace it with something unrecognisable.
Note the two quantifiers. Equality has to hold at every size, not some size — otherwise pick zero, and two empty rasters agree about nothing at great length. Maguire flags this as the ever-present trivial solution to an algebra’s system of equations, and it’s worth watching for: a law that’s satisfiable by making everything degenerate isn’t pinning down what you think it is.
🔗Constraining the observation
The laws so far relate constructors to each other. Nothing yet says which way cw turns —
swap cw and ccw everywhere and every law still holds. Since these equations will
generate our tests, that ambiguity has to go. So: laws relating constructors to the
observation.
rasterize(w, h, flipV(t)) = rasterize(w, h, t).reverse
rasterize(w, h, flipH(t)) = rasterize(w, h, t).map(_.reverse)
rasterize(w, h, cw(t)) = rasterize(h, w, t).transpose.map(_.reverse)
rasterize(w, h, above(t1, t2)) =
rasterize(w, h / 2, t1) ++ rasterize(w, h - h / 2, t2)
rasterize(w, h, colour(r, g, b, a)) =
Vector.fill(h)(Vector.fill(w)(Colour(r, g, b, a)))
Three notes.
flipV reverses the order of rows; flipH reverses within each row. Row-major ordering
makes those different operations, which is the first hint of something wrong.
above splits the height, and the bottom half absorbs the odd pixel. Arbitrary, but it has
to be decided, and now it’s decided in writing rather than in whoever’s implementation
ships first.
cw swaps width and height in the recursive call, because rotating changes which dimension
you call “width”. I’ll be honest: I got transpose.map(_.reverse) by trying combinations
until one worked. Maguire admits the same. That’s the second hint.
And beside? Symmetric to above in the algebra, but not in the observation — you have to
transpose to column-major, glue, and transpose back, because we picked row-major and rows
aren’t columns:
rasterize(w, h, beside(t1, t2)) =
( rasterize(w / 2, h, t1).transpose ++
rasterize(w - w / 2, h, t2).transpose ).transpose
Third hint. beside and above are perfect mirrors of one another in the algebra and look
nothing alike in the observation.
Hold that thought for three posts.
🔗What we have
Fourteen constructors, one observation, about twenty laws, zero lines of executable code.
What that bought:
- A definition of correctness. Any implementation satisfying every law is right. Any implementation violating one is wrong. No judgement calls.
- A specification that can’t go stale, because in part 4 it becomes the test suite.
- Three or four facts about the domain — the
beside/flipHargument swap,flipV ∘ flipH = cw ∘ cw— that I’d otherwise have found from a wrong-looking image. - A pile of unease about
rasterizethat I can’t yet name.
That last one is the most valuable thing here, and it’s the subject of part 5.
Next: Part 3 — Generalisation, and finding the Applicative, in which noticing that most of these constructors don’t care about colour makes the library dramatically more powerful.
🔗Sources
- Maguire, Sandy. Algebra-Driven Design. 2020. Chapter 2 (Tiles) and Chapter 3 (What Makes a Good Algebra?). https://leanpub.com/algebra-driven-design — the algebra, its laws, the observational-equality framing, and the worked derivations are his. This series is a signpost to the book, not a replacement for it.
- Henderson, Peter. Functional Geometry. ACM Symposium on Lisp and Functional Programming, 1982 (revised 2002) — the original tile algebra, and the Escher Square Limit reconstruction that Maguire’s chapter is built on.
- Dijkstra, Edsger W. The Humble Programmer (EWD340), 1972 — for the definition of abstraction underpinning the method.
The Scala 3 translation, the derivation of flipV ∘ flipH = cw ∘ cw in the form given, and
the note on the book’s conflicting swirl definitions are mine.