Nat 类型在《无形》中的局限性

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

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

4480 次浏览
小开
最佳答案

我会自己尝试一下，我很乐意接受 Travis Brown 或者 Miles Sabin 的更好的回答。

Nat 目前可以用 没有来表示大数

在 Nat 的当前实现中，该值对应于嵌套的无形数量。 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 ]上执行位操作时强制执行相同的数组大小。

小开

无形的 Nat使用 Church 编码在类型级别对自然数进行编码。另一种方法是将自然数表示为位的类型级别 HList。

看看 密集，它以一种无形的方式实现了这个解决方案。

我已经有一段时间没有做这个了，当 scalac 放弃的时候，它需要一些无形的 Lazy，但是这个概念是可靠的


提交答案