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

Question

我试图借助这个 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] 的实例，编译器如何知道？

Answer 1

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

Given the instance of <[_0, _1] the compiler can build an instance of <[_1, _2], how the compiler knows that?

来自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]。然后它会开始寻找那个。

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

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

How to compiler find the right implicit?

functional-programming

scala

type-level-computation

scala-cats