Converting integers to peano numbers using the type system

Question

This is a follow-up of a question I asked almost two years ago. I am still experimenting with the type system to write a small linear algebra library where the dimensions of vectors/matrices/tensors is encoded using the type system (with Peano numbering). This allows the compiler to restrict the binary operations to objects of corresponding dimensions.

It works well, but I must specify each dimension type manually. For example (using shapeless natural numbers):

type _1 = Succ[Nat._0]
type _2 = Succ[_1]
type _3 = Succ[_2]

It's ok for small sizes but it gets boring if I need to define the size _1024. I'm trying (without success) to find a way to convert (at compile time) an integer literal to the corresponding Peano-number type.

In Daniel Sobral answer comments, I was told that this was not possible because Scala did not support dependent types. Now, Scala 2.10 has both dependent types and macros. So is there a way to achieve it ?

Answer 1

This is possible right now with the macros in 2.10.0 (although the syntax will get cleaner with Paradise). I've posted an off-the-cuff complete working example here—I'm sure it could easily be made much more concise—which you can use like this:

val holder = NatExample.toNat(13)

And then:

scala> implicitly[holder.N =:= shapeless.Nat._13]
res0: =:=[holder.N,shapeless.Nat._13] = <function1>

It will fail with a reasonable compile-time error if you pass a non-literal integer, etc.