具有协方差的交叉点类型

Intersection types with Covariance

考虑以下:

trait AA {
    def children: List[AA]
}

trait BB {
    def children: List[BB]
}

class CC extends AA, BB {
    override def children: List[AA] & List[BB] = ???
}

当我们在CC中覆盖children时,被覆盖的方法是顶级方法的合并实体。因此 return 类型 List[AA] & List[BB] 是有道理的。

我不明白的是,下面是如何编译的?

class DD extends AA, BB {
    override def children: List[AA & BB] = ???
}

List 是协变的,因此(这里是 proof 的来源):

List[AA & BB] <: List[AA] & List[BB]

DD只有在List[AA] & List[BB] <: List[AA & BB]的情况下才能编译。是真的吗? 如果是这样,那么就不是 List[AA] & List[BB] =:= List[AA & BB]。请推荐


在我看来 List[AA & BB] =:= List[AA] & List[BB]。考虑一下:

    val xx: List[AA & BB] = ???
    val yy: List[AA] & List[BB] = ???
    
    val z1: List[AA] & List[BB] = xx
    val z2: List[AA & BB] = yy

你写的要让 DD 编译,List[AA] & List[BB] 必须是 List[AA & BB] 的子类型。我不明白你为什么这么想,事实上你错了。方法 return 类型是协变的,因此反过来说:List[AA & BB] 必须是 List[AA] & List[BB] 的子类型。而且确实是这样,所以代码没问题。

Matthias Berndt 已经回答说 List[AA] & List[BB] <: List[AA & BB] 不需要编译您的代码。但是,另外一点是它实际上是正确的(List[AA] & List[BB] =:= List[AA & BB] 也是如此)。为什么?

  1. 考虑类型 List[AA] & List[BB] 的值 x
  2. 它必须是 List[AA]List[BB]
  3. AA的列表和BB的列表。
  4. 因此此列表的任何元素 y 必须是 AA,因为 xAA 的列表,而 BB 因为 xBB 的列表。
  5. 所以 y 必须是 AA & BB.
  6. 因为 x 的每个元素的类型都是 AA & BB,所以 x 的类型是 List[AA & BB].

此推理特定于 List,但它概括了 and not just to covariant types

If C is a type constructor, then C[A] & C[B] can be simplified using the following three rules:

  • If C is covariant, C[A] & C[B] ~> C[A & B]
  • If C is contravariant, C[A] & C[B] ~> C[A | B]
  • If C is non-variant, emit a compile error