Type-Level Programming in Scala, Part 4d: Peano arithmetic

Now we will use Nat#FoldR to define arithmetic on type-level natural numbers.

Our type level functions and folds will follow the form of these value level functions. (In most cases, we are really just applying a function n times and not doing anything with the current iteration value.)

val list(n: Int) = (n to 1 by -1).toList

// like Succ[N]
def succ(a: Int) = a+1

// like Add[A <: Nat, B <: Nat]
def add(a: Int, b: Int) =
   ( list(a) :\ b) { (n, acc) => succ(acc) }

def mult(a: Int, b: Int) =
   ( list(a) :\ 0) { (n, acc) => add(acc, b) }

def exp(a: Int, b: Int) =
   (list(b) :\ 1 ) { (n, acc) => mult(acc, a) }

def fact(a: Int) =
   (list(a) :\ 1) { (n, acc) => mult(n, acc) }
   
def mod(a: Int, b: Int) =
   (list(a) :\ 0 ) { (n, acc) => if(acc+1 == b) 0 else acc+1 }

For reference, the Fold type was defined as:

trait Fold[-Elem, Value] {
   type Apply[N <: Elem, Acc <: Value] <: Value
}

Addition looks like:

   type Add[A <: Nat, B <: Nat] = A#FoldR[B, Nat, Inc]
   type Inc = Fold[Nat, Nat] {
      type Apply[N <: Nat, Acc <: Nat] = Succ[Acc]
   }

Multiplication is defined in terms of addition:

   type Mult[A <: Nat, B <: Nat] = A#FoldR[_0, Nat, Sum[B]]
   type Sum[By <: Nat] = Fold[Nat, Nat] {
      type Apply[N <: Nat, Acc <: Nat] = Add[By, Acc]
   }

Factorial is defined in terms of multiplication. For whatever reason, it only worked with a fold left:

   type Fact[A <: Nat] = A#FoldL[_1, Nat, Prod]
   type Prod = Fold[Nat, Nat] {
      type Apply[N <: Nat, Acc <: Nat] = Mult[N, Acc]
   }

Exponentiation is also in terms of multiplication:

   type Exp[A <: Nat, B <: Nat] = B#FoldR[_1, Nat, ExpFold[A]]
   type ExpFold[By <: Nat] = Fold[Nat, Nat] {
      type Apply[N <: Nat, Acc <: Nat] = Mult[By, Acc]
   }

Mod uses Compare#eq:

   type Mod[A <: Nat, B <: Nat] = A#FoldR[_0, Nat, ModFold[B]]
   type ModFold[By <: Nat] = Fold[Nat, Nat] {
      type Wrap[Acc <: Nat] = By#Compare[Acc]#eq
      type Apply[N <: Nat, Acc <: Nat] = Wrap[Succ[Acc]]#If[_0, Succ[Acc], Nat]
   }

We can define:

   def toInt[N <: Nat] : Int

similar to toBoolean. However, it is not very usable for large integers, so we will mainly use:

  type Eq[A <: Nat, B <: Nat] = A#Compare[B]#eq
  toBoolean[ Eq[ A, B ] ]

Some examples:

   type Sq[N <: Nat] = Exp[N, _2]

   val true = toBoolean[ Eq[ Sq[_9], Add[_1,Mult[_8,_10]] ] ]

   val true = toBoolean[ Eq[ Sq[Sq[_9]], Sq[Add[_1,Mult[_8,_10]]] ] ]

   val true = toBoolean[ Eq[ Mod[ Exp[_9,_4], _6], _3] ]

   val true = toInt[ Mod[ Sq[_9], _6] ] == 81 % 6

Operations on Nat are simple to implement using our folds, but don’t work well for reasonably large numbers or more complicated expressions. Around 10,000, the compilation time increases a lot or the stack overflows. Next, we’ll look at representing unsigned integers in binary and (sort of) solve Euler problem #4.