Shapeless 中 Nat 类型的限制

Posted 2023-02-14

【中文标题】Shapeless 中 Nat 类型的限制

【英文标题】：Limits of Nat type in Shapeless

【发布时间】：2014-02-13 06:55:13

【问题描述】：

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

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

【问题讨论】：

Miles 去年的 NE Scala presentation 解决了这个问题，简短的回答是，可以使用 singleton types 在 Scala 或至少在 2.10 中的类型级别表示大数，但它might not be worth it。 Shapeless 2.0 目前仍在使用 Church 编码，这将使您在编译器放弃之前达到 1,000 左右。

我将在今天晚些时候尝试写一个带有更多上下文的答案。附带说明一下，如果您需要更大的类型级别数字，使用整数单例类型并不难——例如，请参阅我的博客文章 here 或 singleton functionality in Shapeless。

如果您想对大型类型级别的数字进行算术运算，您可以考虑将它们实现为位的链表。

@KarolS 我已经实施了该策略！如果有人感兴趣，我很乐意将它贡献给 shapeless，尽管它毫无价值，除非有人可以帮助解决 ***.com/questions/31768203/…

看来***.com/questions/31768203/… 已经解决了，你能贡献你的代码并用你自己的答案结束问题吗？

【参考方案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] 进行位操作时强制使用相同的数组大小。

【讨论】：

刚看到这个答案，+1，这是一个很好的例子。值得注意的是，您可以提供类型类，例如Shapeless 的 ops.nat.Sum 将见证两个类型级别的整数具有特定的总和等（它们只需要由宏提供）。

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

【参考方案2】：

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

查看dense，它以无形的风格实现了这个解决方案。

我已经有一段时间没有研究它了，当 scalac 放弃时，它需要在这里和那里洒一些无形的'Lazy，但这个概念是可靠的 :) p>