Rohit's Blog

Occasional writing on software engineering.

Making Music in Scala 3, Part 2: An Algebra of Music

scalamusic

Following Chapters 10 and 11 of The Haskell School of Music by Paul Hudak. Part 1 built a Music[A] type with two combinators and made it produce a MIDI file. This post asks the question that turns it from a data type into an algebra.

There’s a pleasing collision here. Hudak wrote this chapter in 2014 about music; Sandy Maguire wrote Algebra-Driven Design in 2020 about software design in general; and the first post in that series arrived at the same definition of equality by a completely different route. Two authors, two domains, no shared vocabulary, same idea. That convergence is the most interesting thing in this post.

🔗The question

Is tempo(2, tempo(3, m)) the same as tempo(6, m)?

Structurally, obviously not. One is a tree with two Modify nodes and the other has one. == says no. And yet if you play them, nobody on earth could tell the difference — so in every sense a musician cares about, they are the same piece of music.

Which means == is the wrong question. Hudak’s answer:

Two pieces of music are equivalent if they perform identically.

Formally, writing perform(ctx, m) for the list of timed events a piece produces in a given context:

m1 ≡ m2   iff   ∀ ctx. perform(ctx, m1) == perform(ctx, m2)

This is observational equivalence, and it’s the same move as the tile algebra’s “two tiles are equal iff they rasterize identically at every size”. The observation differs; the principle doesn’t. Equality is what you can’t distinguish by looking — and looking means running the one function that gets data out.

Everything below is a claim about this ≡, not about ==.

🔗The axioms

Hudak lists eight, which unpack to about twelve equations. I’ll give them in Scala notation, grouped by what they’re actually telling you.

Tempo is multiplicative, transposition is additive.

tempo(r1, tempo(r2, m))          ≡ tempo(r1 * r2, m)
transpose(p1, transpose(p2, m))  ≡ transpose(p1 + p2, m)

The first is the one that motivated the section. Note it also settles the awkwardness from part 1 — Tempo(2) means “twice as fast”, and this law is what makes that reading coherent. Rates compose by multiplication, which is why Dur has to be exact and floating point would be a slow leak.

They commute with each other.

tempo(r1, tempo(r2, m))      ≡ tempo(r2, tempo(r1, m))
transpose(p1, transpose(p2, m)) ≡ transpose(p2, transpose(p1, m))
tempo(r, transpose(p, m))    ≡ transpose(p, tempo(r, m))

The third is the interesting one: speeding up and transposing are independent. Obvious for MIDI, and worth noticing that it’s false for real recorded audio, where speeding up a tape raises the pitch. Our algebra has silently committed to a symbolic model of music rather than a signal-based one. Part 1 made that choice; this law is where it becomes visible.

Both distribute over both compositions.

tempo(r, m1 :+: m2)     ≡ tempo(r, m1) :+: tempo(r, m2)
tempo(r, m1 :=: m2)     ≡ tempo(r, m1) :=: tempo(r, m2)
transpose(p, m1 :+: m2) ≡ transpose(p, m1) :+: transpose(p, m2)
transpose(p, m1 :=: m2) ≡ transpose(p, m1) :=: transpose(p, m2)

Four laws, and every one of them is an optimisation waiting to happen — read right-to-left, they hoist a Modify node out of a composition, so you carry one instead of two. We’ll cash that in at the end.

Both compositions are associative; parallel is commutative.

m0 :+: (m1 :+: m2) ≡ (m0 :+: m1) :+: m2
m0 :=: (m1 :=: m2) ≡ (m0 :=: m1) :=: m2
m0 :=: m1          ≡ m1 :=: m0

rest(0) is the identity for both.

m :+: rest(0) ≡ m ≡ rest(0) :+: m
m :=: rest(0) ≡ m ≡ rest(0) :=: m
tempo(r, rest(0)) ≡ rest(0)
transpose(p, rest(0)) ≡ rest(0)

Put those two groups together and you have the punchline:

  • (Music, :+:, rest(0)) is a monoid.
  • (Music, :=:, rest(0)) is a commutative monoid.

Two monoids over the same carrier, sharing an identity. That’s not decoration — it means line and chord from part 1 were combineAll under two different Monoid instances all along, and it means we can rebalance, reassociate, and parallelise either one without changing what a program means.

A rest can pad a parallel composition. Given dur(m1) > dur(m2) and d ≤ dur(m1) - dur(m2):

m1 :=: m2 ≡ m1 :=: (m2 :+: rest(d))

Silence at the end of the shorter voice is unobservable, because Par takes the max duration anyway.

And the duality law. Given dur(m0) == dur(m2):

(m0 :+: m1) :=: (m2 :+: m3)  ≡  (m0 :=: m2) :+: (m1 :=: m3)

Two voices each split into two phrases, versus two chords played in sequence. Same music — provided the split happens at the same moment in both voices, which is what the side condition says. This is the law I’d never have found by staring at the code, and it’s the one that captures something real about music: it’s why you can read a score either as horizontal lines or as vertical slices, and why both readings are correct.

🔗Commutativity is a constraint on the implementation

m0 :=: m1 ≡ m1 :=: m0 looks free. It isn’t.

perform on a Par has to merge two time-ordered event streams into one. The obvious merge compares start times:

// scala-check: skip
def merge(a: Performance, b: Performance): Performance = (a, b) match
  case (e1 :: es1, e2 :: es2) =>
    if e1.time < e2.time then e1 :: merge(es1, b) else e2 :: merge(a, es2)
  case (Nil, es) => es
  case (es, Nil) => es

Now take two events at the same time in different voices. Merging a, b puts b’s event first; merging b, a puts a’s first. The lists differ. Commutativity fails, and with it several proofs that depend on it.

Hudak’s fix is one character: compare whole events rather than just their start times, so ties break the same way regardless of argument order.

// scala-check: skip
    if e1 < e2 then ...     // Ordering[Event], not just Ordering[Rational]

I love this detail. A law we wanted to hold about the algebra dictated a specific choice in the implementation of something three layers down. That’s the whole argument for writing laws first, made in one line of code — and it’s the same dynamic as the tile algebra’s zippy-versus-cartesian applicative, where the invariant forced the instance.

🔗One proof

Most of these are direct calculations from perform. Here’s one that actually needs induction, and it ties back to part 1’s line:

Claim: line(xs ++ ys) ≡ line(xs) :+: line(ys)

Base case, xs = Nil:

line(Nil ++ ys)
  = line(ys)                        -- definition of ++
  ≡ rest(0) :+: line(ys)            -- rest(0) is a left identity
  = line(Nil) :+: line(ys)          -- definition of line

Inductive case, xs = x :: rest, assuming the claim for rest:

line((x :: rest) ++ ys)
  = line(x :: (rest ++ ys))              -- definition of ++
  = x :+: line(rest ++ ys)               -- definition of line
  ≡ x :+: (line(rest) :+: line(ys))      -- induction hypothesis
  ≡ (x :+: line(rest)) :+: line(ys)      -- associativity of :+:
  = line(x :: rest) :+: line(ys)         -- definition of line

Two identity laws, one associativity law, and structural induction. No compiler involved.

That’s a small result but a useful one: it says you can build a long melody in pieces and concatenate, and it doesn’t matter where you cut. Anyone writing a music generator relies on that constantly without ever stating it.

🔗Turning the axioms into a test suite

Prose proofs are good; executable ones are better, and the definition of ≡ tells us exactly how to write them. Two pieces are equal if they perform identically — so compare performances.

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

def observationallyEqual[A](m1: Music[A], m2: Music[A]): Boolean =
  perform(Context.default, m1) == perform(Context.default, m2)

given Arbitrary[Music[Pitch]] = Arbitrary(genMusic)

def genMusic: Gen[Music[Pitch]] = Gen.sized { size =>
  if size <= 1 then genPrim
  else
    def smaller = Gen.resize(size / 2, genMusic)
    Gen.frequency(
      3 -> genPrim,
      6 -> Gen.zip(smaller, smaller).map(_ :+: _),
      6 -> Gen.zip(smaller, smaller).map(_ :=: _),
      2 -> Gen.zip(genRate, smaller).map(tempo),
      2 -> Gen.zip(Gen.choose(-12, 12), smaller).map(transpose)
    )
}

The generator has the same shape as every recursive generator: a size check for termination, a halved budget for sub-terms, and weights that favour the structural constructors. If that shape is unfamiliar, part 4 of the algebra series walks through why each part is there.

One detail specific to music: genRate must never produce zero. tempo(0, m) divides durations by zero, which is not slow music, it’s a crash.

Then the axioms, transcribed:

// scala-check: skip
class MusicLaws extends munit.ScalaCheckSuite:

  property("tempo is multiplicative") {
    forAll { (m: Music[Pitch], r1: Rational, r2: Rational) =>
      observationallyEqual(tempo(r1, tempo(r2, m)), tempo(r1 * r2, m))
    }
  }

  property("transpose is additive") {
    forAll { (m: Music[Pitch], p1: Int, p2: Int) =>
      observationallyEqual(transpose(p1, transpose(p2, m)), transpose(p1 + p2, m))
    }
  }

  property("tempo and transpose commute") {
    forAll { (m: Music[Pitch], r: Rational, p: Int) =>
      observationallyEqual(tempo(r, transpose(p, m)), transpose(p, tempo(r, m)))
    }
  }

  property("tempo distributes over :+:") {
    forAll { (m1: Music[Pitch], m2: Music[Pitch], r: Rational) =>
      observationallyEqual(tempo(r, m1 :+: m2), tempo(r, m1) :+: tempo(r, m2))
    }
  }

  property(":=: is commutative") {
    forAll { (m1: Music[Pitch], m2: Music[Pitch]) =>
      observationallyEqual(m1 :=: m2, m2 :=: m1)
    }
  }

  property("rest(0) is a two-sided identity for :+:") {
    forAll { (m: Music[Pitch]) =>
      observationallyEqual(m :+: rest(0), m) && observationallyEqual(rest(0) :+: m, m)
    }
  }

  property("duality, when the split times agree") {
    forAll { (m0: Music[Pitch], m1: Music[Pitch], m3: Music[Pitch]) =>
      val m2 = padTo(dur(m0), m3)   // force the side condition
      observationallyEqual((m0 :+: m1) :=: (m2 :+: m3), (m0 :=: m2) :+: (m1 :=: m3))
    }
  }

That last one is worth noticing. The duality law has a precondition, so you can’t state it as a naive forAll — you either filter (and throw away most generated cases, which ScalaCheck will eventually complain about) or you construct inputs that satisfy it. I’ve padded m2 to match dur(m0). Conditional laws are the fiddliest part of turning an axiom set into a suite, and they’re where I’d expect a first attempt to quietly test nothing.

And the monoids come free from cats:

// scala-check: skip
  checkAll("Music.seq",  MonoidTests[Music[Pitch]](using seqMonoid).monoid)
  checkAll("Music.par",  CommutativeMonoidTests[Music[Pitch]](using parMonoid).commutativeMonoid)

🔗Cashing the laws in

Laws are nice. Laws that make your program faster are nicer. Read the distributive and multiplicative axioms right-to-left and they become rewrite rules:

// scala-check: skip
def normalise[A](m: Music[A]): Music[A] = m match
  // tempo is multiplicative — collapse the stack
  case Modify(Tempo(r1), Modify(Tempo(r2), m)) => normalise(tempo(r1 * r2, m))
  case Modify(Transpose(p1), Modify(Transpose(p2), m)) => normalise(transpose(p1 + p2, m))

  // identity — a scaling that does nothing
  case Modify(Tempo(r), m) if r == 1     => normalise(m)
  case Modify(Transpose(0), m)           => normalise(m)

  // rest(0) is the identity for both compositions
  case Seq(Prim(Rest(z)), m) if z == 0   => normalise(m)
  case Seq(m, Prim(Rest(z))) if z == 0   => normalise(m)
  case Par(Prim(Rest(z)), m) if z == 0   => normalise(m)
  case Par(m, Prim(Rest(z))) if z == 0   => normalise(m)

  // distributivity, read backwards — hoist a shared modifier out
  case Seq(Modify(Tempo(a), x), Modify(Tempo(b), y)) if a == b =>
    normalise(tempo(a, normalise(x) :+: normalise(y)))

  case Seq(m1, m2)     => Seq(normalise(m1), normalise(m2))
  case Par(m1, m2)     => Par(normalise(m1), normalise(m2))
  case Modify(c, m)    => Modify(c, normalise(m))
  case p @ Prim(_)     => p

Every case is an axiom. The correctness argument is not “I tested it” but “each rewrite is a law, and the laws are observational equalities, therefore normalise(m) ≡ m by construction.” The test suite above is then a check on my transcription, not on my reasoning — which is a much smaller thing to get wrong.

And it does nothing for hand-written music. I want to be straight about that. Nobody writes tempo(2, tempo(3, m)) by hand. Run normalise over the Frère Jacques canon from part 1 and you’ll save nothing, because there’s nothing to save.

Where it earns its keep is generated music — a composition built by recursive transformation, where each level of recursion wraps another Modify node around the same subtree. That’s precisely what part 4 constructs. Depth 6 of a self-similar piece accumulates Modify nodes exponentially, and normalise collapses them before perform ever walks the tree.

So the honest measurement is: run it on part 4’s output, and quote the number there rather than inventing one here.

🔗What this bought

The same three things the tile algebra bought, in a domain with no geometry to lean on:

  • A definition of correctness. Any change to perform that breaks one of these laws is a bug, whatever it does to the sound.
  • A constraint that propagated downward. Commutativity of :=: forced merge to compare whole events. Without the law, the naive merge would have shipped and worked almost always.
  • A set of provably-correct optimisations, obtained by reading laws backwards rather than by testing an optimiser.

And one thing the tile algebra didn’t: a reason to notice that our model of music is symbolic rather than acoustic, visible in the single law saying tempo and transposition commute.

Next: Part 3 — Interpretation, Performance, and Players, in which we take the hacked-together MIDI conversion from part 1 seriously, and find a case where a typeclass is the wrong tool.

🔗Sources

  • Hudak, Paul. The Haskell School of Music. Cambridge University Press. Chapter 10 (Proof by Induction) and Chapter 11 (An Algebra of Music). The definition of musical equivalence, all eight axioms, and the observation about merge needing to compare whole events for commutativity are Hudak’s.
  • Maguire, Sandy. Algebra-Driven Design. 2020. https://leanpub.com/algebra-driven-design — for the general framing of observational equality, which this chapter arrives at independently.
  • ScalaCheck (Rickard Nilsson), cats-laws and discipline (Typelevel).

The Scala 3 translation, the line(xs ++ ys) induction in the form given, the normalise function, and the observation about the tempo/transpose commutativity law implying a symbolic rather than acoustic model are mine.