scala – 总结“大型”Nat’s

让我们从一个较小的数字开始.当你要求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],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并且我们已经完成了.

所以很明显,对于nn,我们将不得不进行n次隐式搜索,并且在每次编译期间,编译器将进行类型相等性检查和其他事情(更新：请参阅Miles的答案以解释最大问题这里是需要遍历Nat类型的结构,因此我们处于指数范围.编译器真的,实际上并不是设计用于有效地使用这样的类型,这意味着即使是小数字,这个操作也需要很长时间.

附注1：在Shapeless中实现

在我的头顶,我不完全确定为什么sum2没有像这样定义：

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

这个速度要快得多,至少在我的机器上,Sum [_18,_18]在4秒内编译而不是7分钟计数.

旁注2：诱导启发式

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

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]时,编译器在表示结果类型时不会遇到任何问题(即在_0周围有44个Succ),即使它没有_44类型的别名.