Solving Type Equations for Type-Level Proofs of Peano Arithmetic in Scala 3

The Compiler Whisperer: Teaching Types to Dance in Scala 3

In the previous post I gave a tutorial on writing type-level programs in Scala 3. Type-level programming in Scala can solve nontrivial type equations at compile time using givens, type classes, and associated types. This approach lets you encode arithmetic over types, prove properties, and avoid runtime checks. The goal here is to show a compact pattern for Peano arithmetic and to trace how the compiler discovers a proof that 1 + 2 equals 3. Next, we explain in detail, how a type-level proof of greatest common divisor works when the compiler solves a chain of type equations. My implementation encodes Euclid’s algorithm at the type level, then relies on given and using search to assemble the necessary evidence.

Peano Encoding and Type-Level Sum

We start with a minimal encoding of natural numbers and a Sum type class that computes addition at the type level. The complete example is shown below and can be cloned from my Github repo.

object PeanoSumWithGiven:
  sealed trait Nat
  sealed trait _0 extends Nat
  sealed trait Succ[N <: Nat] extends Nat

  trait Sum[A <: Nat, B <: Nat]:
    type Result <: Nat

  object Sum:
    type Aux[A <: Nat, B <: Nat, R <: Nat] = Sum[A, B] { 
             type Result = R }

    // Base case: 0 + B = B
    given sum0[B <: Nat]: Sum.Aux[_0, B, B] =
      new Sum[_0, B]:
        type Result = B

    // Recursive case: Succ[A] + B = Succ[A + B]
    given sumSucc[A <: Nat, B <: Nat]
        (using sumAB: Sum[A, B]): 
       Sum.Aux[Succ[A], B, Succ[sumAB.Result]] =
         new Sum[Succ[A], B]:
              type Result = Succ[sumAB.Result]

  trait Proof[A <: Nat, B <: Nat, Expected <: Nat]

  object Proof:
    // If Sum[A, B] computes Expected, then a proof exists.
    given proofSum[A <: Nat, B <: Nat, Expected <: Nat]
       (using Sum.Aux[A, B, Expected]): Proof[A, B, Expected] =
           new Proof[A, B, Expected] {}

  def main(args: Array[String]): Unit =
    type _1 = Succ[_0]
    type _2 = Succ[_1]
    type _3 = Succ[_2]
    type _4 = Succ[_3]

    // Summon compile-time proofs.
    val proof1Plus2: Proof[_1, _2, _3] = summon[Proof[_1, _2, _3]]
    val proof2Plus2: Proof[_2, _2, _4] = summon[Proof[_2, _2, _4]]

    // either line would not compile, which is the desired effect.
    // val wrong1: Proof[_1, _2, _4] = summon[Proof[_1, _2, _4]]
    // val wrong2: Proof[_0, _3, _4] = summon[Proof[_0, _3, _4]]

What the Types Mean

Numbers live at the type level. _0 represents zero. Succ[N] represents the successor of N. The aliases _1, _2, _3, _4 abbreviate the nested Succ types. A value of type Proof[A, B, Expected] witnesses that adding A and B computes Expected by way of the Sum type class.

How the Proof Is Constructed

Consider the statement val proof1Plus2: Proof[_1, _2, _3] = summon[Proof[_1, _2, _3]]. The compiler tries to produce a Proof[_1, _2, _3]. It finds the given proofSum inside Proof, which requires Sum.Aux[_1, _2, _3]. The requirement shifts the task to computing the associated Result of Sum[_1, _2] and unifying it with _3.