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?

Answer 1

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].

Answer 2

Shapeless's Nat encodes natural numbers at the type level using Church encoding. An alternate method is to represent the naturals as a type level HList of bits.

Check out dense which implements this solution in a shapeless style.

I haven't worked on it in a while, and it needs a sprinkling of shapeless' Lazy here and there for when scalac gives up, but the concept is solid :)