如何编译器找到正确的隐式？答案

【问题标题】：How to compiler find the right implicit?如何编译器找到正确的隐式？
【发布时间】：2020-12-06 16:16:18
【问题描述】：

我正在尝试借助 https://www.youtube.com/watch?v=qwUYqv6lKtQ 了解 Scala 中的类型级编程。让我们考虑提供的代码：

trait Nat
class _0 extends Nat
class Succ[A <: Nat] extends Nat

type _1 = Succ[_0]
type _2 = Succ[_1] // = Succ[Succ[_0]]
type _3 = Succ[_2] // = Succ[Succ[Succ[_0]]]
type _4 = Succ[_3] // ... and so on
type _5 = Succ[_4]

sealed trait <[A <: Nat, B <: Nat]
object < {
    def apply[A <: Nat, B <: Nat](implicit lt: <[A, B]): <[A, B] = lt
    implicit def ltBasic[B <: Nat]: <[_0, Succ[B]] = new <[_0, Succ[B]] {}
    implicit def inductive[A <: Nat, B <: Nat](implicit lt: <[A, B]): <[Succ[A], Succ[B]] = new <[Succ[A], Succ[B]] {}
}

sealed trait <=[A <: Nat, B <: Nat]
object <= {
    def apply[A <: Nat, B <: Nat](implicit lte: <=[A, B]): <=[A, B] = lte
    implicit def lteBasic[B <: Nat]: <=[_0, B] = new <=[_0, B] {}
    implicit def inductive[A <: Nat, B <: Nat](implicit lt: <=[A, B]): <=[Succ[A], Succ[B]] = new <=[Succ[A], Succ[B]] {}
}

作者描述了定义val invalidComparison: _3 < _2 = <[_3, _2]的编译步骤：

apply 方法需要 <[_2, _3] 的隐式实例
要找到该实例，编译器可以选择运行这两个中的任何一个隐式方法 - 它将尝试调用 inductive 方法，但它将需要<[_1, _2] 的隐式实例
同理，编译器标记它可以调用inductive 方法，但它需要 <[_0, _1] 类型的隐式实例
在这种情况下，ltBasic 的方法签名表明编译器可以构建<[_0, _1] 的实例，因为_1 = Succ[0]
现在，给定<[_0, _1] 的实例，编译器可以构建一个 <[_1, _2] 的实例
以相同的风格，给定<[_1, _2] 的实例，编译器可以构建<[_2, _3] 的实例
给定<[_2, _3]的实例，它可以安全地传递给 apply 方法并返回

问题是，编译器在哪里知道如何递减 <[_2, _3] 直到达到 <[_0, _1] 才能获得正确的隐式？

给定<[_0, _1]的实例，编译器可以构建<[_1, _2]的实例，编译器是怎么知道的？

【问题讨论】：

您可以手动解决这个问题，采用与编译器相同的非常机械的方法。你需要_2 < _3，你有两个选项_0 < Succ[B]，在这种情况下它不适用因为_2 =!= _0和Succ[A] < Succ[B]如果A < B所以_2 _1 < _2并且它继续向下直到它到达_0 < Succ[_0] 所以一切都解决了。

标签： scala functional-programming scala-cats type-level-computation

【解决方案1】：

它不会“减少”任何东西。它只知道inductive 如果具有正确的隐式参数，则可以找到正确的隐式。它还不知道它会找到那些，但无论如何它都会尝试。

给定<[_0, _1]的实例，编译器可以构建<[_1, _2]的实例，编译器是怎么知道的？

来自inductive的方法签名：

implicit def inductive[A <: Nat, B <: Nat](implicit lt: <[A, B]): <[Succ[A], Succ[B]]

如果给定一个隐含的<[A, B]，它将提供<[Succ[A], Succ[B]] 类型的值。 -- 寻找的<[_1, _2] 类型与<Succ[_0], Succ[_1] 类型相同，因此它需要一个隐式<[_0, _1]。然后它会开始寻找那个。

它不知道它减少了任何东西，它只是去寻找它需要的隐式和它需要找到它们的隐式。

【讨论】：