在统一过程中，高级类型的实例化和包含式是如何相互作用的？

Question

如果量词出现在与之相反的位置：f :: (forall a. [a] -> b) -> Bool，则函数类型是更高的级别。

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

可以使用灵活的类型变量实例化

• a，条件是这不允许a转义其作用域
• 或另一个刚性类型变量
• ，但不能使用非抽象类型，因为foo的调用方不是foo的调用方，而是foo本身决定a是什么，而b已经由调用方h 215f 216确定。

然而，一旦起作用，事情就变得更加复杂了：

{-# 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这样的单类型实例化的规则吗？

也许有人可以为两个应用程序规划统一的过程。

Answer 1

我们有

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

在g arg2c中得到了应用。

要键入“检查”，只需验证参数的类型是否为函数域类型的子类型。也就是说，我们有

([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) <: T{U/a}中{U/a}表示类型变量a的替换为U类型。因此，

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