scala - Shapeless 中 Nat 类型的限制

Question

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

这种表示法是否能够表示大数，例如1000000 或 2⁵³，或者这会导致 Scala 编译器放弃吗？

Answer 1

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

Nat 目前不能用于表示大数

在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] 上执行位操作时强制使用相同的数组大小。