scala - 求和 "Large"Nat 的

Question

给定:

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 是否存在于无形中？

Answer 1

为什么这么慢？

让我们从一个较小的数字开始。当您询问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隐式搜索，并且在每次搜索期间，编译器将进行类型相等性检查和其他需要遍历 Nat 结构的内容(更新:请参阅 Miles 的回答以了解这里最大问题是什么)类型，所以我们正处于指数​​领域。编译器实际上并不是为了有效地处理这样的类型而设计的，这意味着即使对于很小的数字，此操作也将花费很长时间。

旁注 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 编译 Shapeless Sum 上的注释而且看起来仍然和没有它时一样慢得可怕。

44 怎么样？

_1 , _2 , _3类型别名在 this boilerplate generator 生成的代码中定义在 Shapeless 中，它被配置为仅生成最多 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 。输入别名。