如果量词出现在逆变位置,则函数类型更高: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
type 是每个实例的子类型。正式,(forall a. T) <: T{U/a}
哪里{U/a}
表示替换类型变量a
带类型 U
.因此,forall a. [a] -> [a] <: ([a] -> [a]){Int/a} = [Int] -> [Int]
关于haskell - 在统一过程中,更高级别类型的实例化和包含如何交互?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/66211000/