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 ?

Since 2.10 only supports def macros, I think you should have a look at type macros in macro paradise: http://docs.scala-lang.org/overviews/macros/paradise.html — Kim Stebel, Jan 07 '13 at 09:30
Scala supports dependent types? Can I have some background on that? — Bill, Jan 13 '13 at 01:22
@Bill have a look at macros examples. The macro result type is a dependent type. — paradigmatic, Jan 13 '13 at 07:30
Huh, I never thought of it that way. That's very cool. Thanks, @paradigmatic. — Bill, Jan 13 '13 at 13:11

score 8 · Accepted Answer · answered Jan 07 '13 at 12:31

8

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.

answered Jan 07 '13 at 12:31

Travis Brown

138,631
12
375
680

What does the =:= operator mean in this context? – Dominic Bou-Samra Jan 07 '13 at 13:52
2

It's a [standard library type class](http://www.scala-lang.org/api/current/index.html#scala.Predef$) that provides evidence that the compiler knows that two types are the same. It was around before 2.10—see for example [this answer](http://stackoverflow.com/a/3427759/334519) for a discussion of how it's used. – Travis Brown Jan 07 '13 at 15:12

Converting integers to peano numbers using the type system

1 Answers1