总结"大"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],编译器将去寻找一个实例,它会找到这两个方法:

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]在4秒内编译,而不是7分钟.

旁注2:诱导启发式

这似乎不是Typelevel Scala -Yinduction-heuristics帮助的情况 - 我只是尝试使用@inductive注释编译Shapeless,Sum并且它似乎仍然非常像没有它一样非常慢.

44岁怎么样？

的_1,_2,_3类型别名在由产生的代码中定义的这个样板发生器在不成形,其配置为仅专门产生值高达22在这种情况下,这是一个完全任意的限制.我们可以写下面的内容,例如:

type _23 = Succ[_22]

我们完成了与代码生成器完全相同的功能,但更进了一步.

_N然而,Shapeless的别名在22处停止并不重要,因为它们只是别名.关于a的重要一点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]编译器时,即使它没有类型别名,也不会在表示结果类型(即Succa周围44 秒_0)时遇到任何问题_44.