在统一过程中，高级类型的实例化和包含如何交互？

Posted 2023-05-08

【中文标题】在统一过程中，高级类型的实例化和包含如何交互？

【英文标题】：How does instantiation of higher-rank types and subsumption interact during unification?

【发布时间】：2021-05-18 12:21:48

【问题描述】：

如果量词出现在逆变位置，则函数类型排名较高：f :: (forall a. [a] -> b) -> Bool

关于这种类型的统一，类型变量a 比b 更严格，因为适用以下实例化规则：

a 可以使用灵活的类型变量进行实例化，前提是这不允许 a 逃脱其范围 或使用另一个刚性类型变量 但不是非抽象类型，因为不是foo的调用者而是foo本身决定a是什么，而b已经由调用者确定

但是，一旦包容开始发挥作用，事情就会变得更加复杂：

-# LANGUAGE RankNTypes #-

f :: (forall a. [a] -> [a]) -> Int -- rank-2
f _ = undefined

arg1a :: a -> a
arg1a x = x

arg1b :: [Int] -> [Int]
arg1b x = x

f arg1a -- type checks
f arg1b -- rejected

g :: ((forall a. [a] -> [a]) -> Int) -> Int -- rank-3
g _ = undefined

arg2a :: (a -> a) -> Int
arg2a _ = 1

arg2b :: (forall a. a -> a) -> Int
arg2b _ = 1

arg2c :: ([Int] -> [Int]) -> Int
arg2c _ = 1

g arg2a -- type checks
g arg2b -- rejected
g arg2c -- type checks

h :: (((forall a. [a] -> [a]) -> Int) -> Int) -> Int -- rank-4
h _ = undefined

arg3a :: ((a -> a) -> Int) -> Int
arg3a _ = 1

arg3b :: ((forall a. a -> a) -> Int) -> Int
arg3b _ = 1

arg3c :: (([Int] -> [Int]) -> Int) -> Int
arg3c _ = 1

h arg3a -- rejected
h arg3b -- type checks
h arg3c -- rejected

立即引起注意的是子类型关系，它会随着每个额外的逆变位置而翻转。应用程序g arg2b 被拒绝，因为(forall a. a -> a) 比(forall a. [a] -> [a]) 更具多态性，因此(forall a. a -> a) -> Int 的多态性比(forall a. [a] -> [a]) -> Int 少。

我不明白的第一件事是为什么g arg2a 被接受。是否只有在两个项都处于较高级别时才起作用？

然而，g arg2c 类型检查的事实让我更加困惑。这不是明显违反了刚性类型变量a 不能用像Int 这样的单型实例化的规则吗？

也许有人可以为这两个应用程序制定统一流程..

【问题讨论】：

如果arg2c 可以接受[Int] -> [Int] 函数作为其第一个参数，那么它当然可以接受g 将提供给它的forall a. [a] -> [a] 函数，只需随后选择@ 987654344@。 （这应该给出一个高级别的直觉，但没有涉及到你所要求的统一细节，所以不是一个真正的答案。）

粗略地说，双逆变位置是协变位置，因为“双重否定”抵消了，这也可以看作是子类型关系被翻转两次的结果。实际上，在您的g arg2c 中，a 类型可以实例化为Int，因为如果我们计算所需的子类型检查，我们最终会得到([Int] -> [Int]) -> Int <: (forall a. [a] -> [a]) -> Int，然后翻转关系，使用forall a. [a] -> [a] <: [Int] -> [Int]，然后是实例化。

@chi 我得到了forall a. [a] -> [a] <: [Int] -> [Int] 的关系，但量词仍然存在。但是，现在它不再处于逆变位置了，对吧？如果a 在子类型检查后不是rank-1+n 而是rank-1，那么a 可以用Int 实例化，当然，因为a 是一个灵活的类型变量，可以用它实例化一个类型常量。简单地说，子类型检查的过程改变了嵌套，从而改变了所涉及量词的等级。这是对的吗？

@scriptum 是的，在最后一个 <: 中，forall 位于顶层，因此它是协变的。在此过程中，由于我们从较大的类型移至其组件，因此排名发生了变化。 IMO，考虑排名对理解这一点没有多大帮助。最后一个<: 只是一般规则(forall a.T) <: TU/a 的一个例子，其中U/a 表示将类型变量a 替换为类型U。这条规则和(a->b) <: (a'->b') iff b<:b' and a'<:a 是您对示例进行类型检查所需的全部内容。

【参考方案1】：

我们有

g :: ((forall a. [a] -> [a]) -> Int) -> Int
arg2c :: ([Int] -> [Int]) -> Int

在g arg2c中应用。

要进行类型检查，只需验证参数的类型是函数域类型的子类型即可。 IE。我们有

([Int] -> [Int]) -> Int <: ((forall a. [a] -> [a]) -> Int)

根据子类型规则，我们有(a->b) <: (a'->b')当且仅当b<:b'和a'<:a。所以上面等价于

Int <: Int
forall a. [a] -> [a] <: [Int] -> [Int]

第一个不等式是微不足道的。第二个成立，因为 foall 类型是每个实例的子类型。形式上，(forall a. T) <: TU/a 其中U/a 表示将类型变量a 替换为类型U。因此，

forall a. [a] -> [a] <: ([a] -> [a])Int/a = [Int] -> [Int]