为什么我们需要为某些类型计算的输出指定一个精炼类型（或其等效的 Aux）？

In https://jto.github.io/articles/typelevel_quicksort :

我们接触到一个Sum键入谁的apply看起来像这样：

def apply[A <: Nat, B <: Nat](implicit sum: Sum[A, B]): Aux[A, B, sum.Out] = sum

现在，我们可以直接使用类型细化而不是 Aux，但问题仍然存在：为什么需要这样做（显式返回类型）？返回类型不是“显而易见”吗applySum#Out 类型是否等于 sum.Out？

如果我们删除它并且我们只使用val x = Sum[_0, _1]，看起来不错，除了添加val y = Sum[x.Out, _1]不起作用，说编译器找不到隐式 Sum。

为什么编译器似乎“忘记”了 x.Out 的确切类型？

Types Sum[A, B] and Sum.Aux[A, B, C] = Sum[A, B] { type Out = C }是不同的。后者是前者的子类型。还Sum[A, B]是存在主义类型Sum.Aux[A, B, _].

返回类型不是“显而易见”吗apply会有一个 Sum#Out 类型等于 sum.Out？

No,

def apply[A <: Nat, B <: Nat](implicit sum: Sum[A, B]) = sum

是相同的

def apply[A <: Nat, B <: Nat](implicit sum: Sum[A, B]): Sum[A, B] = sum

问题是，首先你定义隐式：或者归纳地sum1, sum2或者简单地

implicit val sum00: Aux[_0, _0, _0] = new Sum[_0, _0] { type Out = _0 }
implicit val sum01: Aux[_0, _1, _1] = new Sum[_0, _1] { type Out = _1 }
implicit val sum10: Aux[_1, _0, _1] = new Sum[_1, _0] { type Out = _1 }
implicit val sum11: Aux[_1, _1, _2] = new Sum[_1, _1] { type Out = _2 }
...

然后当你写的时候

def apply[A <: Nat, B <: Nat](implicit sum: Sum[A, B]): Aux[A, B, sum.Out] = sum

只知道A and B足以解决隐式问题。每个定义的隐式“知道”其特定的C。但如果你只是回来Sum[A, B] this C将会被遗忘。

你可以定义

def apply[A <: Nat, B <: Nat, C <: Nat](implicit sum: Aux[A, B, C]): Aux[A, B, C] = sum

但随后你将不得不调用它并指定C手动：Sum[_2, _3, _5].

如果我们删除它并且我们只使用val x = Sum[_0, _1]，看起来不错， 除了添加val y = Sum[x.Out, _1]不会工作，说 编译器找不到隐式 Sum。

Sure. x.Out不再是_1，这只是一些抽象的x.Out，并且隐式无法解析。