Scala Level Programming
I wanted to get deeper into level programming in Scala and started doing some small exercises. I started by implementing Peano numbers at the type level. Here's 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 have happened in this project? How can I use it?
source to share
As long as you need to create these types yourself, it doesn't get you much. But, once you make the compiler, do it for you, it will be much more useful.
Before I show it, let me change the way Peano arithmetic is represented to something shorter:
sealed trait Num
case object Zero extends Num
case class Succ[N <: Num](num: N) extends Num
Then you can create a 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 sth created with the sych list it will have the 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))))
The next thing you might try to do is use implications to test something, for example.
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 this, you can ensure that some operation can only be performed if implicit evidence could be provided:
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, the true power of type-level programming in Scala comes when you start using implicits to create new types: the ones you could use for implicit proofs, type inference, and the removal of some structural templates.
A library that helps a lot to generate is Shaeless. I find you will be fun to work with once you do an exercise or two with some derived type class with implicits.
Coming back to your code: you can provide some implications that will generate and provide you with instances of your class. Also, besides creating a new class, this code will also do something else, eg. concatenate lists of elements that you would add to these classes, or provide a conversion from PeanoNumType to Int, or add some compile-time predicates, etc. Sky is the limit.
source to share