当我们说T1比T2更具多态性时,我们的意思是什么？

Question

我正在学习用任意级别类型的实用类型推断的类型推断,我陷入了困境.我基本上对关于更多多态的概念感到困惑,因此无法继续.

在其第3.3节中,它指出:

如果函数的类型比函数的参数类型更具多态性,则该函数可以接受该参数.

在我的理解中,要说T1比T2具有类型的任何实例T2必须满足类型更具多态性T1.所以根据我的定义,forall a. a比多态更多Int.forall a b. a -> b -> b比forall a. a -> a -> a.更多态.

据我了解,存在冲突.鉴于:

f :: (forall a. a) -> Int
k :: (forall a. a -> a)

(f k)显然是有效的[1].然后根据文章的引文,forall a. a -> a应该比多态多forall a. a.然而,举一个例子,文字1将满足,forall a. a而显然它不是一个forall a. a -> a,因此根据我的定义,forall a. a应该更多态forall a. a -> a.这与文章中关于多态性而非关系性的描述相矛盾.

我正在寻找一个明确的解释,并举例说明这种关系到底是什么.谢谢.

更新:

[1]:如评论中的d8d0d65b3f7cf42注意到我与之(forall a. a)不兼容(forall a. a -> a).应该有我理解的问题.而且我注意到(forall a. a -> Int)可以接受带有类型的参数(forall a. a -> a)但(forall a. a) -> Int不能.我不知道为什么这个案子会那样.

无论我的错误理解是什么,我仍然期待一个很好的解释,即多态性比关系更多.谢谢 :)

Answer 1

正如对OP的评论中所指出的那样,(undefined :: (forall a . a) -> Int) ( undefined :: (forall a. a -> a) )不是类型检查,实际上forall a. a -> a并不是多态的forall a. a,所以这里没有矛盾.

另一方面,(undefined :: (forall a. a -> Int)) (undefined :: (forall a. a -> a))typechecks,所以forall a. a -> a必须包含a在函数类型中,对吧？这可能看似违反直觉,但事实恰恰如此.让我解释.

包容和类型变量

包容(或者说:多态子类型)意味着"至少是多态的",所以它更像是一个类比<=而不是<.在校正的OP示例中,a包含forall a. a -> a因为在该上下文 a中是非刚性类型变量,并且它可以与其他类型统一.因此,forall a. a -> a <= typeVar b被认为是正确的,同时也产生约束typeVar b = forall a. a -> a(或者可能是不同的约束,取决于我们对类型推理系统的选择.实际步骤可能与我在下面的示例中的草图有很大不同).

一个简单的分步示例:

-- goal 
(forall a. a -> Int) <= (Int -> Int)
-- instantiate variable on the left hand side with a fresh type variable.
(tvar a' -> Int) <= (Int -> Int)
-- check return type subsumption
Int <= Int -- OK
-- check argument type subsumption
Int <= tvar a' -- OK, add "tvar b = Int" to the set of constraints.
-- Done.

在一般情况下,如果我们有forall a. P <= Q一些P和Q,我们必须找到一些特定实例的a满足包含关系.这意味着我们a使用灵活的类型变量进行实例化,然后从那里开始.在这种情况下,我们执行特定类型的搜索,并且我们可以继续细化类型变量.

另一方面,如果我们有P <= forall a. Q,那么包含必须适用于右手边的所有可能的实例化a.在这种情况下,我们通常将实例a化为刚性(或skolem)类型变量.刚性类型变量并非真正"可变"; 相反,它代表一些任意(未知)固定类型,我们无法改进它.带有刚性变量的示例:

-- goal
(forall a. a -> Int) <= (forall b. b -> Int)
-- instantiate variable on the left
(tvar a' -> Int) <= (forall b. b -> Int)
-- instantiate variable on the right
(tvar a' -> Int) <= (skolem b' -> Int)
-- check return types
Int <= Int -- OK
-- check argument types
skolem b' <= tvar a' -- OK, record the "tvar a' = skolem b'" constraint 
-- Done. 

基本上,我们只能用skolem变量做两件事:

1. 我们可以自由地总结skolem a <= skolem a,即它们包含自己.
2. 我们可以用灵活的变量来统一它们,即我们可以拥有 skolem a <= tvar b或tvar b <= skolem a.

旋转函数类型

我们已经在示例中看到(a -> b) <= (a' -> b')iff b <= b'和a' <= a.该<=翻转的参数类型.这是为什么？

假设我们的输入上下文需要一些类型的函数a -> b.此函数 - 通常作为函数 - 消耗类型的a值并生成类型的值b.有点比喻,上下文有需求的b-s,它也能够提供 a -s我们的功能.如果函数返回一个更通用的类型b,那很好,从那以后它也可以满足上下文的需求b.但是,如果函数期望的类型比一般更普遍a,则上下文就会失败.不良背景只有b库存,它可以专门化它们,但不能概括它们.如果只有函数对它接受的类型不那么挑剔!

根据行话,函数类型构造函数在参数类型中是逆变(或负),在返回类型中是协变(或正).有关维基百科的差异的讨论很好.它更关注OOP类层次结构的子类型而不是多态子类型,但它也应该提供对后者的有用见解.

让我们看一下包含翻转更为突出的示例:

-- goal 
((forall a. a -> a) -> Int) <= ((forall a. a -> Int) -> Int)
-- remember: the context can supply "forall a. a -> Int"-s and demands "Int"-s. 
-- check return types
Int <= Int -- OK
-- check argument types
(forall a. a -> Int) <= (forall a. a -> a)
-- instantiate on the left
(tvar a' -> Int) <= (forall a. a -> a)
-- instantiate on the right
(tvar a' -> Int) <= (skolem a'' -> skolem a'')
-- check return types
Int <= skolem a'' -- FAIL: this clearly does not hold.
-- Abort.

排名-1与较高排名设置中的函数类型方差

我的前两个例子没有嵌套forall-s,即它们只有rank-1类型.你可能已经注意到翻转的包含没有任何区别!如果我们假设(a -> b) <= (a' -> b') iff b <= b' and a <= a'那么两个例子都会很好地检查,因为我们只需要检查类型变量,skolems和单态类型的包含.

因此,协方差 - 逆差区分仅与更高级别的类型相关(这也在OP的引文第3.3节中暗示过).虽然,如果我没记错的话,HMF系统也忽略了函数方差自旋,尽管它是更高级别的.