范围型变量的重要性代表类型变量而不是类型

ech*_*ata 22 haskell types ghc

在ScopedTypeVariables扩展的GHC 文档中,概述将以下内容说明为设计原则:

范围类型变量代表类型变量,而不代表类型.(这是GHC早期设计的变化.)

我知道范围类型变量扩展的一般目的,但我不知道这里区分类型变量和代表类型之间的区别的含义.从语言用户的角度来看,差异的意义是什么?

上述评论暗示两种设计以不同方式处理此决策并做出不同的权衡.什么是替代设计,它与目前实施的设计相比如何?

K. *_*uhr 5

tl;dr: 文档说了什么是因为 GHC 中作用域类型变量的旧实现是不同的,而新文档(过度)强调了旧行为和新行为之间的对比。事实上,你在ScopedTypeVariables扩展中使用的作用域类型变量只是普通的旧(刚性)类型变量,这些与你在没有作用域的常规 Haskell 类型签名中使用的类型变量相同(即使你没有意识到它们是“刚性的”)。确实,作用域类型变量不只是“代表类型”,但常规的无作用域类型变量也不简单地“代表类型”。

更长的答案:

首先,撇开作用域类型变量的问题,考虑以下几点:

pluralize :: [a] -> [a]
pluralize x = x ++ "s"
Run Code Online (Sandbox Code Playgroud)

如果a,作为一个类型变量,只是“代表一个类型”,那就没问题了。GHC 会确定a代表 type Char,并且生成的签名[Char] -> [Char]将确定为 的正确类型pluralize,所以不会有问题。事实上,如果我们推断类型:

pluralize x = x ++ "s"
Run Code Online (Sandbox Code Playgroud)

在普通的老式 Hindley-Milner (HM) 类型系统中,这可能正是会发生的情况。作为打字时的中间步骤(++)的应用中,类型检查器将分配x的类型[a]为“新鲜的” HM型变量a,它会分配pluralize类型[a] -> [a]统一之前[a]与该类型的"s" :: [Char]统一aChar

取而代之的是,这是由GHC类型检查被拒绝,因为a这种类型的签名不是HM-风格类型的变量,因此也不能简单地代表一个类型。相反,它是一个严格的(即用户指定的)Haskell 类型变量,并且类型检查器不允许这样的变量在定义pluralize.

同样,以下内容被拒绝:

pairlist :: a -> b -> [a]
pairlist x y = [x,y]
Run Code Online (Sandbox Code Playgroud)

即使,如果ab刚刚主张类型,这将是罚款(因为它适用于任何ab*提供只ab属于同一类型)。相反,它是由类型检查遭到拒绝,因为两个刚性哈斯克尔类型变量ab不统一。

现在,您可能会尝试证明问题在于类型变量是“刚性的”并且无法与具体类型(如Char)或彼此统一,而是在 Haskell 类型签名中存在隐式量化,所以签名pluralize实际上是:

pluralize :: forall a . [a] -> [a]
Run Code Online (Sandbox Code Playgroud)

所以当a决定“代表”时Char,正是与这种forall a量化的矛盾引发了错误。这个论点的问题在于,这两种解释实际上或多或少是等价的。正是因为 Haskell 类型变量是刚性的(即,因为 Haskell 中的类型签名是隐式普遍量化的),类型无法统一(即,统一与量化相矛盾)。然而,事实证明,“刚性类型变量”解释比“隐式量化”解释更接近 GHC 类型检查器中实际发生的情况。那'

现在,让我们回到作用域类型变量的问题。在过去,GHC 的-fscoped-type-variables扩展实施方式完全不同。特别是,对于模式类型签名,您可以编写如下内容(取自GHC 6.0文档):

f :: [Int] -> Int -> Int
f (xs::[a]) (y::a) = (head xs + y) :: a
Run Code Online (Sandbox Code Playgroud)

文档接着说:

左侧的模式类型签名f表示xs必须是某种类型的事物列表a;并且y必须具有相同的类型。表达式(head xs) [sic]上的类型签名指定此表达式必须具有相同的类型a不要求以“ a”命名的类型实际上是类型变量。 实际上,在这种情况下,以“ a”命名的类型是Int. (这是对原始相当复杂的规则的轻微自由化,该规则指定模式绑定类型变量应该被普遍量化。)

它继续提供了一些使用作用域类型变量的其他示例,例如:

g (x::a) (y::b) = [x,y]       -- a unifies with b

k (x::a) True    = ...        -- a unifies with Int
k (x::Int) False = ...
Run Code Online (Sandbox Code Playgroud)

2006 年,Simon Peyton-Jones 做出了一个重大承诺 ( ac10f840),为类型系统添加不可预测性,这也最终大大改变了词法作用域类型变量的实现。提交文本包含更改的详细说明,包括新设计的要求。

一个关键的设计选择是词法范围的类型变量现在被命名为严格的(即用户指定的多态)Haskell 类型变量,而不是更像 HM 风格的变量,它仅仅代表一个类型并受制于统一。

这使得上面的例子 ( f, g, 和k) 是非法的,因为模式匹配中的作用域类型变量现在表现得更像常规的刚性类型变量。

Soooo... 旧的设计可能是一个奇怪的 hack,它使作用域类型变量更像 HM 类型变量,因此与“普通”Haskell 类型变量完全不同,而新系统使它们更符合无作用域类型变量的行为方式。

然而,更复杂的是,@duplode 在评论中的链接引用了在模式匹配的签名上下文中部分“撤销”这个“限制”的提议。我认为可以公平地说,将范围类型变量更像是一种特殊情况的旧设计不如新设计更好地统一范围和非范围类型变量的处理,并且没有回头的愿望到旧的实现。然而,新的、更简单的实现具有对模式签名不必要的限制的副作用,这可能应该被视为允许非刚性类型变量的特殊情况。