Shapeless 中 Nat 类型的限制

在无形中，Nat 类型代表了一种在类型级别对自然数进行编码的方法。例如，这用于固定大小的列表。您甚至可以在类型级别上进行计算，例如附加一个列表N列表中的元素K元素并返回一个在编译时已知的列表N+K元素。

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

我自己也尝试一下。我很乐意接受特拉维斯·布朗或迈尔斯·萨宾的更好答案。

纳特目前可以not用于表示大数

在 Nat 当前的实现中，该值对应于嵌套的 shapeless.Succ[] 类型的数量：

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

因此，为了表示数字 1000000，您需要一个嵌套 1000000 层的类型，这肯定会破坏 scala 编译器。根据实验，当前限制似乎约为 400，但为了合理的编译时间，最好保持在 50 以下。

但是，有一种方法可以在类型级别对大整数或其他值进行编码，前提是您不想对它们进行计算。据我所知，你唯一能做的就是检查它们是否相等。见下文。

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

这可以用于例如对 Array[Byte] 执行位操作时强制使用相同的数组大小。