Limits of Nat type in Shapeless

Question

In shapeless, the Nat type represents a way to encode natural numbers at a type level. This is used for example for fixed size lists. You can even do calculations on type level, e.g. append a list of N elements to a list of K elements and get back a list that is known at compile time to have N+K elements.

Is this representation capable of representing large numbers, e.g. 1000000 or 2⁵³, or will this cause the Scala compiler to give up?

Miles's NE Scala presentation last year addresses this question, and the short answer is that it would be possible to represent large numbers at the type level in Scala—or at least in 2.10—using singleton types, but it might not be worth it. Shapeless 2.0 currently still uses the Church encoding, which will get you to 1,000 or so before the compiler gives up. — Travis Brown
I'll try to write up an answer with a little more context later today. As a side note, it's not too hard to work with integer singleton types if you need larger type level numbers—see for example my blog post here or the singleton functionality in Shapeless. — Travis Brown
If you want to do arithmetic on large type-level numbers, you may consider implementing them as a linked list of bits. — Karol S
@KarolS I have an implementation of that strategy! And I'd be glad to contribute it to shapeless if anyone is interested, although it's worthless unless someone can help solve stackoverflow.com/questions/31768203/… — beefyhalo
It looks like stackoverflow.com/questions/31768203/… is solved, so can you contribute you code and close the question with your own answer ? — Andriy Kuba

Rüdiger Klaehn Rüdiger Klaehn · Accepted Answer · 2015-10-01T13:07:23

I will attempt one myself. I will gladly accept a better answer from Travis Brown or Miles Sabin.

Nat can currently not be used to represent large numbers

In the current implementation of Nat, the value corresponds to the number of nested shapeless.Succ[] types:

scala> Nat(3)
res10: shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]] = Succ()

So to represent the number 1000000, you would have a type that is nested 1000000 levels deep, which would definitely blow up the scala compiler. The current limit seems to be about 400 from experimentation, but for reasonable compile times it would probably be best to stay below 50.

However, there is a way to encode large integers or other values at type level, provided that you do not want to do calculations on them. The only thing you can do with those as far as I know is to check if they are equal or not. See below.

scala> type OneMillion = Witness.`1000000`.T
defined type alias OneMillion

scala> type AlsoOneMillion = Witness.`1000000`.T
defined type alias AlsoOneMillion

scala> type OneMillionAndOne = Witness.`1000001`.T
defined type alias OneMillionAndOne

scala> implicitly[OneMillion =:= AlsoOneMillion]
res0: =:=[OneMillion,AlsoOneMillion] = <function1>

scala> implicitly[OneMillion =:= OneMillionAndOne]
<console>:16: error: Cannot prove that OneMillion =:= OneMillionAndOne.
       implicitly[OneMillion =:= OneMillionAndOne]
                 ^

This could be used to e.g. enforce same array size when doing bit operations on Array[Byte].

Limits of Nat type in Shapeless

2 Answers