Shapeless中Nat类型的限制

Question

在shapeless中，Nat类型表示一种在类型级别上编码自然数的方式。例如，这被用于固定长度列表。你甚至可以在类型级别上进行计算，比如将一个 N 元素的列表追加到一个 K 元素的列表中，得到一个在编译时已知具有 N+K 个元素的列表。

这种表示能否表示大的数字，比如 1000000 或 2⁵³？或者这会导致Scala编译器放弃编译？

- Rüdiger Klaehn

---

去年 Miles 在 NE Scala 演讲中谈到了这个问题，简单回答是在 Scala 中——至少在 2.10 版本中——使用 singleton types 可以表示大数，但这可能不值得（详见链接）。目前 Shapeless 2.0 仍然使用 Church 编码，在编译器放弃之前可以处理到大约 1,000。 - Travis Brown

我会尝试稍后写一篇更有上下文的答案。顺便说一句，如果需要更大的类型级数值，使用整数单例类型并不太难——例如，请参阅我的博客文章这里或Shapeless中的单例功能。 - Travis Brown

如果你想在类型级别的大数字上进行算术运算，你可以考虑将它们实现为一串位的链表。 - Karol S

@KarolS 我已经实现了那个策略！如果有人感兴趣，我很乐意为shapeless做出贡献，尽管它毫无价值，除非有人能帮助解决https://dev59.com/qo3da4cB1Zd3GeqP26dm。 - beefyhalo

看起来 https://dev59.com/qo3da4cB1Zd3GeqP26dm 的问题已经解决了，所以你可以贡献你的代码并用自己的答案关闭这个问题吗？ - Andriy Kuba

Answer 1

我会尝试自己翻译。我很乐意接受Travis Brown或Miles Sabin的更好答案。

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]执行位操作时，可以使用此方法来强制使用相同的数组大小。

- Rüdiger Klaehn

---

刚看到这个答案，点赞了，这是一个很好的例子。值得注意的是，您可以提供类型类，例如Shapeless的ops.nat.Sum，它将证明两个类型级整数具有特定的和等等（只需通过宏提供即可）。 - Travis Brown

这是一个Concat类型类的示例，它允许通过宏连接两个类型级别的字符串。用于对类型级别整数求和的类型类可能看起来非常相似。 - Frank S. Thomas

Answer 2

Shapeless的Nat使用Church编码将自然数编码为类型级别。另一种方法是将自然数表示为位的类型级别HList。请查看dense，它以shapeless风格实现了这个解决方案。 我已经有一段时间没有处理它了，并且需要在某些地方添加shapeless' Lazy，以便在scalac放弃时使用，但概念是稳定的 :)

- beefyhalo

---

我猜自然数的教堂编码是将它们编码为lambda f => x => x，f => x => f(x)，f => x => f(f(x))... https://en.wikipedia.org/wiki/Church_encoding 以Z，S(Z)，S(S(Z))的方式进行编码是通过Peano的 https://en.wikipedia.org/wiki/Peano_axioms - Dmytro Mitin