Limits of Nat type in Shapeless

Question

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

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 :)