scala - 总结 "Large"Nat's

鉴于:

scala> import shapeless.nat.
_0   _10   _12   _14   _16   _18   _2    _21   _3   _5   _7   _9      natOps
_1   _11   _13   _15   _17   _19   _20   _22   _4   _6   _8   apply   toInt

scala> import shapeless.ops.nat._
import shapeless.ops.nat._

> 3 分钟后，以下代码尚未编译/运行。为什么？

scala> Sum[_22, _22]

另外，看看上面的 REPL 自动补全，_44 是否甚至存在于 shapeless 中？

最佳答案

为什么这么慢？

让我们从一个较小的数字开始。当你请求 Sum[_4, _4] 时，编译器会去寻找一个实例，它会找到 these two methods :

implicit def sum1[B <: Nat]: Aux[_0, B, B] = new Sum[_0, B] { type Out = B }
implicit def sum2[A <: Nat, B <: Nat](implicit
  sum: Sum[A, Succ[B]]
): Aux[Succ[A], B, sum.Out] = new Sum[Succ[A], B] { type Out = sum.Out }

第一个显然已经出局，因为 _4 不是 _0 。它知道 _4 与 Succ[_3] 相同(稍后会详细介绍)，因此它会尝试将 sum2 与 A 作为 _3 并将 B 作为 _4 。

这意味着我们需要找到一个 Sum[_3, _5] 实例。 sum1 与之前的原因类似，所以我们再次尝试 sum2，这次使用 A = _2 和 B = _5 ，这意味着我们需要一个 Sum[_2, _6] ，它让我们回到 sum2 ，带有 A = _1 和 B = _6 ，这让我们寻找 .Sum[_1, _7]这是我们最后一次使用 sum2 以及 A = _0 和 B = _7 。这一次，当我们去寻找 Sum[_0, _8] 时，我们会点击 sum1，我们就完成了。

所以很明显，对于 n + n 我们将不得不进行 n + 1 隐式搜索，并且在每个搜索过程中，编译器都将进行类型相等性检查和其他内容(更新:请参阅 Miles 的回答以了解这里最大的问题是什么是)这需要遍历 Nat 类型的结构，所以我们处于指数级。编译器真的，真的不是为了有效地处理这样的类型而设计的，这意味着即使对于小数字，这个操作也需要很长时间。

旁注 1:在 Shapeless 中实现

在我的头顶上，我不完全确定为什么 sum2 不是这样定义的:

implicit def sum2[A <: Nat, B <: Nat](implicit
  sum: Sum[A, B]
): Aux[Succ[A], B, Succ[sum.Out]] = new Sum[Succ[A], B] { type Out = Succ[sum.Out] }

这要快得多，至少在我的机器上，Sum[_18, _18] 在四秒内编译，而不是七分钟和计数。

旁注 2:归纳启发式

这似乎不是 Typelevel Scala 的 -Yinduction-heuristics 有帮助的情况——我只是尝试使用 @inductive 上的 Sum 注释编译 Shapeless，但它似乎仍然与没有它一样慢得可怕。

44呢？
_1 、 _2 、 _3 类型别名在 Shapeless 中由 this boilerplate generator 生成的代码中定义，该代码配置为仅生成最多 22 的值。具体而言，在这种情况下，这是一个完全任意的限制。例如，我们可以编写以下内容:

type _23 = Succ[_22]

我们做了与代码生成器完全相同的事情，但更进一步。

不过，Shapeless 的 _N 别名在 22 处停止并不重要，因为它们只是别名。 Nat 的重要之处在于它的结构，这与我们可能为它取的任何好名字无关。即使 Shapeless 根本没有提供任何 _N 别名，我们仍然可以编写如下代码:

import shapeless.Succ, shapeless.nat._0, shapeless.ops.nat.Sum

Sum[Succ[Succ[_0]], Succ[Succ[_0]]]

它与编写 Sum[_2, _2] 完全相同，只是打字更烦人。

因此，当您编写 Sum[_22, _22] 时，编译器在表示结果类型(即 Succ 周围的 44 个 _0 )时不会有任何问题，即使它没有 _44 类型别名。

关于scala - 总结 "Large"Nat's，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/42406467/