haskell - 在统一过程中,高级类型的实例化和包含如何交互?
问题描述
如果量词出现在逆变位置,则函数类型是更高等级的: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
.
要对此进行类型检查,只需验证参数的类型是函数域类型的子类型即可。即我们有
([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}
where表示用 type{U/a}
替换类型变量。因此,a
U
forall a. [a] -> [a] <: ([a] -> [a]){Int/a} = [Int] -> [Int]
推荐阅读
- php - Laravel 5 - 尽管设置了通用会话域,但无法从子域获取经过身份验证的用户
- selenium - 如何处理没有 div 标签且没有信息来自 Selenium 的动态文本?
- c# - 基于正在使用的 mvvm 模式实现导航 Xamarin Forms
- visual-studio - Visual Studio 2017 SDK 位置不可更改
- c# - 使用 Appium C# 驱动程序时如何找到复选框值?
- python - 在 docker 上安装 pyminizip 时出错
- security - OWASPZAP 执行的扫描类型
- android - 如何防止在科尔多瓦的浏览器中打开外部链接?
- ios - Xcode 10 警告:陈旧文件“/path/to/file”位于允许的根路径之外
- bootstrap-4 - Bootstrap 下拉菜单添加水平滚动