1

我试图在这个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]：

  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]，编译器怎么知道呢？

4

1 回答 1

4

它不会“减少”任何东西。它只知道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]与 type 相同<Succ[_0], Succ[_1]，所以它需要一个隐式<[_0, _1]的。然后它会开始寻找那个。

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

于 2020-08-17T15:03:54.637 回答