Type Level Programming in Scala

Question

I wanted to get deeper into type level programming in Scala and I started doing some small exercises. I started with an implementation of Peano numbers at the type level. Here is the code below!

sealed trait PeanoNumType { // Type at the end indicates to the reader that we are dealing with types
  type plus[That <: PeanoNumType] <: PeanoNumType
}

sealed trait ZeroType extends PeanoNumType {
  type plus[That <: PeanoNumType] = That
}

sealed trait NextType[This <: PeanoNumType] extends PeanoNumType {
   type plus[That <: PeanoNumType] = NextType[This#plus[That]]
}

Now the question is, what would the above implementation buy me? How can I make use of it?

Answer 1

As long as you need to create those types yourself, it doesn't give you much. But, as soon as you make compiler do the stuff for you, it will be much more useful.

Before I show this, let's change a way of representing Peano aritmetic into something shorter:

sealed trait Num
case object Zero extends Num
case class Succ[N <: Num](num: N) extends Num

You could then create list with a size known at compile time:

sealed abstract class List[+H, N <: Num](val size: N) {
  def ::[T >: H](value: T): List[T, Succ[N]] = Cons(value, this)
}
case object Nil extends List[Nothing, Zero.type](Zero)
case class Cons[+H, N <: Num](head: H, tail: List[H, N]) extends List[H, Succ[N]](Succ(tail.size))
type ::[+H, N <: Num] = Cons[H, N]

If you check the type of sth created with sych list it will have size encoded in its type:

val list = 1 :: 2 :: 3 :: 4 :: Nil // List[Int, Succ[Succ[Succ[Succ[Zero.type]]]]] = Cons(1,Cons(2,Cons(3,Cons(4,Nil))))

Next thing you could try to do would be usage of implicits to check something, e.g.

trait EvenNum[N <: Num]
implicit val zeroIsEven = new EvenNum[Zero.type] {}
implicit def evenNPlusTwo[N <: Num](implicit evenN: EvenNum[N]) = new EvenNum[Succ[Succ[N]]] {}

With that you could enforce that some operation could only be done when implicit evidence could be supplied:

def operationForEvenSizeList[T, N <: Num](list: List[T, N])(implicit ev: EvenNum[N]) = {
  // do something with list of even length
}

operationForEvenSizeList(1 :: 2 :: Nil) // ok
operationForEvenSizeList(1 :: 2 :: 3 :: Nil) // compiler error

As far as I can tell true power of type-level programming in Scala appears when you start using implicits for creating new types: ones that you could use for implicit evidence, type-class derivation and removal of some structural boilerplate.

A library helping a lot with generic programming is Shapeless. I believe it will be a fun thing for you to work with, once you will do an exercise or two with some type-class derivation with implicits.

Getting back to your code: you could provide some implicits which would generate and provide instances of your class for you. Also, besides creating new class, this code would also do something else e.g. combine lists of elements you would add in those classes, or provide conversion from PeanoNumType to Int, or add some predicates working in compile time, etc. Sky is the limit.