在统一期间，更高级别类型的实例化和包含如何交互？

如何解决在统一期间，更高级别类型的实例化和包含如何交互？

如果量词出现在逆变位置，则函数类型的等级更高：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 这样的单类型实例化的规则？

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

解决方法

我们有

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

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