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

问题描述

我试图借助此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]): <[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]的编译步骤：

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

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

给定<[_0,_1]的实例，编译器可以构建<[_1,_2]的实例，编译器如何知道呢？

解决方法

它不会“减少”任何东西。它只是知道inductive可以找到正确的隐式参数（如果它具有正确的隐式参数）。它尚不知道会找到这些，但还是会尝试。

给定<[_0,_1]的实例，编译器可以构建<[_1,_2]的实例，编译器如何知道呢？

根据inductive的方法签名：

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

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

它不知道它会递减什么，它只是去寻找它所需要的隐式和寻找它们所需的隐式。