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.

Pingback: Type-Level Programming in Scala « Apocalisp