当我们说T1比T2更多态时，意味着什么？

Question

我正在学习类型推理的论文任意秩类型的实用类型推理和我坚持在非常开始。我基本上混淆了多态多于关系的概念，因此不能继续下去。

它在第3.3节中指出：

如果参数的类型比函数的参数类型更具多态性，则该参数是可以接受的。

根据我的理解，如果说T1比T2更具多态性，那就是说任何具有T2类型的实例都必须满足T1类型。因此，按照我的定义，forall a. a比Int更具多态性。forall a b. a -> b -> b比forall a. a -> a -> a更具多态性。

根据我的理解，这是一场冲突。给予：

f :: (forall a. a) -> Int
k :: (forall a. a -> a)

(f k)显然是valid1。然后根据文章的引文，forall a. a -> a应该比forall a. a更具多态性。但是，举个例子，文字1将满足forall a. a，而显然它不是forall a. a -> a，因此根据我的定义，forall a. a应该比forall a. a -> a更多态。这与文章中关于多态多于关系的描述是矛盾的。

我正在寻找一个明确的解释与例子，这一关系到底是什么。谢谢。

更新

1:正如在评论中所述，d8d0d65b3f7cf42注意到(forall a. a)与(forall a. a -> a)不兼容。我的理解应该有问题。我注意到(forall a. a -> Int)可以接受(forall a. a -> a)类型的参数，而(forall a. a) -> Int不能接受。我不知道为什么这个案子会这样。

不管我的错误理解，我仍然期待一个很好的解释，什么是多态比关系是。谢谢您:)

Answer 1

正如在OP的注释中所指出的，(undefined :: (forall a . a) -> Int) ( undefined :: (forall a. a -> a) )并不是打字机，实际上，forall a. a -> a并不比forall a. a更多态，所以这里没有矛盾。

另一方面，(undefined :: (forall a. a -> Int)) (undefined :: (forall a. a -> a))类型选择，所以forall a. a -> a必须将a包含在函数类型中，对吗？这似乎违反了直觉，但事实恰恰如此。让我解释一下。

包含变量和类型变量

包含(或者是:多态子类型)意味着“至少是多态的”，所以它更像是<=而不是<。在经过修正的OP示例中，a包含在forall a. a -> a中，因为在该上下文中，a是一个非刚性类型变量，可以与其他类型统一。因此，forall a. a -> a <= typeVar b被认为是正确的，同时也产生约束typeVar b = forall a. a -> a (或者可能产生不同的约束，这取决于我们对类型推理系统的选择)。实际步骤可能与我在下面的示例中所描述的有很大不同)。

一个简单的逐步示例：

-- goal 
(forall a. a -> Int) <= (Int -> Int)
-- instantiate variable on the left hand side with a fresh type variable.
(tvar a' -> Int) <= (Int -> Int)
-- check return type subsumption
Int <= Int -- OK
-- check argument type subsumption
Int <= tvar a' -- OK, add "tvar b = Int" to the set of constraints.
-- Done.

一般情况下，如果对于某些forall a. P <= Q和Q，我们必须找到满足包含关系的a的一些特殊的实例化。这意味着我们用一个灵活的类型变量实例化a，然后从那里开始。在这种情况下，我们执行对特定类型的搜索，并且我们可以在继续的过程中细化类型变量。

另一方面，如果我们有P <= forall a. Q，那么P <= forall a. Q的所有可能的实例化都必须包含在右侧。在本例中，我们通常将a实例化为刚性(或skolem)类型变量。刚性类型变量并不是真正的“变量”；相反，它代表着某种任意的(未知的)固定类型，我们不能对其进行细化。使用刚性变量的示例：

-- goal
(forall a. a -> Int) <= (forall b. b -> Int)
-- instantiate variable on the left
(tvar a' -> Int) <= (forall b. b -> Int)
-- instantiate variable on the right
(tvar a' -> Int) <= (skolem b' -> Int)
-- check return types
Int <= Int -- OK
-- check argument types
skolem b' <= tvar a' -- OK, record the "tvar a' = skolem b'" constraint 
-- Done. 

基本上，我们只能用skolem变量做两件事：

1. 我们可以自由地得出skolem a <= skolem a的结论，即他们自以为是。
2. 我们可以用一个灵活的变量将它们统一起来，即我们可以有skolem a <= tvar b或tvar b <= skolem a.

自旋函数类型

我们已经在例子中看到，(a -> b) <= (a' -> b')，当且仅当，b <= b'和a' <= a。<=被翻转到参数类型上。为什么会这样呢？

假设我们的类型上下文需要一些a -> b类型的函数。此函数--与函数通常所做的一样--使用a类型的值，并生成b类型的值。在某种程度上，上下文对b-s有一个需求，它还能够为我们的功能提供a-s。如果函数返回一个比b更通用的类型，那很好，因为它还可以满足上下文对b的需求。但是，如果函数期望的类型比a更通用，那么上下文就会很糟糕。糟糕的上下文中只存储了b-s，它可以对它们进行专门化，但不能将它们泛化。如果该函数对它接受的类型不那么挑剔就好了！

根据行话，函数类型构造函数在参数类型中是反变(或负)，在返回类型中是协变(或正)。关于维基百科上的差异有一个很好的讨论。它更关注OOP类层次结构的子类型，而不是多态子类型，但它也应该对后者提供有用的洞察。

让我们看一个示例，其中包含翻转更显着：

-- goal 
((forall a. a -> a) -> Int) <= ((forall a. a -> Int) -> Int)
-- remember: the context can supply "forall a. a -> Int"-s and demands "Int"-s. 
-- check return types
Int <= Int -- OK
-- check argument types
(forall a. a -> Int) <= (forall a. a -> a)
-- instantiate on the left
(tvar a' -> Int) <= (forall a. a -> a)
-- instantiate on the right
(tvar a' -> Int) <= (skolem a'' -> skolem a'')
-- check return types
Int <= skolem a'' -- FAIL: this clearly does not hold.
-- Abort.

等级1与高等级设置中的函数类型差异

我的前两个示例没有嵌套的forall-s，即它们只有秩-1类型。而且你可能已经注意到，翻转的包含没有任何区别！如果我们假设(a -> b) <= (a' -> b') iff b <= b' and a <= a'在那里，那么这两个例子都会很好，因为我们只需要检查类型变量、skolems和单形类型的包含性。

因此，协方差-逆方差的区分只与高阶类型相关(这也在OP的引文3.3节中有所暗示)。不过，如果我没记错的话，HMF系统也会忽略函数的方差自旋，尽管它的排名更高。