java - 在没有可变类型的情况下，是否有不变类型参数的情况？

Question

Java 数组不是完全类型安全的，因为它们是协变的:ArrayStoreException可以出现在别名数组上。另一方面，Java 集合的类型参数是不变的:例如，List<Thread>不是 List<Runnable> 的子类型(这可能有点违反直觉)。
动机似乎与 List 有关s 和其他集合是可变的，所以为了保持类型系统的健全，它们的类型参数必须是不变的。

如果编程语言只支持不可变类型，那么类型参数要么协变要么逆变(但从不不变)的类型系统可以工作吗？换句话说，要使用 Scala 的表示方差的方式，可以有 List[+E] , Function[-T, +R] , Map[+K, +V] ， 等等。
我知道有一些较旧的语言(例如， GNU Sather )似乎只支持协变/逆变参数类型。

我的一般问题是:在数据类型完全不可变的世界中，是否有一种情况会特别需要一个不变的参数类型(与协变或逆变相反)？是否有一些不可变数据结构的示例，这些示例仅适用于不变类型参数？

Answer 1

所以，每个类型系统要么允许一些不健全的程序，要么禁止一些健全的程序，或者两者兼而有之(这是 Rice's theorem 的结果)，所以一个好的工作假设是，是的，你提出的任何限制都必然会排除一些声音否则将被允许的程序。另一方面，人类是无限聪明的，所以从另一个意义上说，答案是否定的:如果你像你描述的那样添加一个限制，那没关系，人们会在需要的时候想办法解决它。 (当然，有时他们会提出您不喜欢的解决方法，例如放弃您的语言。)

但我认为您真正要求的是一个令人信服的案例:一个现实的例子，在直接支持该示例和坚持要求所有类型参数为协变或逆变的建议之间做出选择，您的直觉会告诉您放弃该提案，以便您可以直接支持该示例。

由于您已经确定了类型参数不能协变的各种情况以及类型参数不能逆变的各种情况(例如，Function[-T, +R] 很好，但反过来就完全相反了unsound)，一个好的方法是搜索相同类型参数被使用两次的情况，一次以不能协变的方式，一次以不能逆变的方式。一个简单的例子是 UnaryOperator[T] <: Function[T, T]，类似于 Java 的 java.util.function.UnaryOperator ，其 'apply' 方法返回与它接受的类型相同的类型。 UnaryOperator[String] 不能用作 UnaryOperator[Object](因为您不能将任意对象传递给它)，但 UnaryOperator[Object] 也不能用作 UnaryOperator[String](因为即使你传递给它一个字符串，它也可能返回一些不同的对象)。

对于更充实的现实示例。 . .想象一个二叉搜索树 TreeMap[K, +V] <: Map[K, V]，类似于 Java 的 java.util.TreeMap 。大概我们想要支持诸如 'firstKey' 和 'floorEntry' 和 'iterator' 等方法(或者至少是其中的一些)，所以我们不能使 K 逆变:一个 TreeMap[Object, Foo] 可以' t 用作 TreeMap[String, Foo]，因为当我们检索键时，键可能不是字符串。

由于它是一棵二叉搜索树，它在内部需要一个 Comparator[K]，这立即使 K 成为协变变得棘手:如果你使用 TreeMap[String, Foo] 作为 TreeMap[Object, Foo]，那么你'重新隐式地使用 Comparator[String] 作为 Comparator[Object]，这是行不通的。现在，由于映射肯定只包含字符串键，也许 'get' 方法可以通过在使用 Comparator[String]; 调用之前预先检查键的类型来解决这个问题。但是 'floorEntry' 和 'ceilingEntry' 方法仍然是一个问题:什么条目出现在无法与映射中的键进行比较的任意对象“之前”或“之后”？

即使您已经说过您的 map 是不可变的，您可能仍然需要某种“放置”方法，只是一个返回 map 修改副本的纯函数式方法。 (纯函数式红黑树支持与可变树相同的不变量和最坏情况渐近时间复杂度，所以撇开类型系统不谈，这当然是一个合理的做法。)但是如果 TreeMap[String, Foo] 可以用作TreeMap[Object, Foo]，那么它的 'put' 方法需要支持返回一个包含非字符串键的二叉搜索树——即使它的 Comparator[String] 没有定义这些键的排序。

(在评论中，您提到 Scala 实际上定义了 Map[K, +V] 具有不变的键类型。我从未使用过 Scala，但我敢打赌这正是原因。)