haskell - 作用域类型变量代表类型变量而不是类型的意义

Question

在ScopedTypeVariables扩展的GHC documentation中，概述将以下内容作为设计原则:

A scoped type variable stands for a type variable, and not for a type. (This is a change from GHC’s earlier design.)

我知道范围化类型变量扩展的一般用途，但是我不知道在区分类型变量和区分类型之间进行区分的含义。从语言使用者的 Angular 来看，差异的意义何在？

上面的评论暗示了两种设计，它们以不同的方式处理此决定并做出不同的权衡。什么是替代设计，它与当前实现的设计相比如何？

Answer 1

tl;博士:该文档说了它的意思，因为GHC中作用域类型变量的旧实现是不同的，而新文档(过度)则强调了旧行为与新行为之间的对比。实际上，您使用ScopedTypeVariables扩展名使用的作用域类型化变量只是普通的(刚性)类型变量，并且这些变量与您在常规Haskell类型签名中使用的类型变量相同，没有作用域(即使您没有意识到他们是“刚性的”)。的确，作用域类型变量并非简单地“代表类型”，但是常规的无范围类型变量也不是简单地“代表类型”。

更长的答案:

首先，撇开范围类型变量的问题，请考虑以下因素:

pluralize :: [a] -> [a]
pluralize x = x ++ "s"

如果将 a作为类型变量，简单地“了解类型”，就可以了。 GHC将确定 a代表类型 Char，并且将得到的签名 [Char] -> [Char]确定为 pluralize的正确类型，因此不会有问题。实际上，如果我们要推断以下类型:

pluralize x = x ++ "s"

在简单的老式Hindley-Milner(HM)类型系统中，这可能正是发生的情况。作为键入 (++)应用程序的中间步骤，类型检查器将为“新鲜” HM类型变量 x分配 [a]类型 a，并在将 pluralize与 [a] -> [a]类型统一之前将 [a]的类型为 "s" :: [Char]类型，以使 a和 Char统一。

相反，这将被GHC类型检查器拒绝，因为此类型签名中的 a不是HM风格的类型变量，因此不仅仅代表类型。相反，它是一个严格的(即用户指定的)Haskell类型变量，类型检查器不允许在定义 pluralize时将此类变量与自身以外的任何其他变量统一。

同样，以下内容也被拒绝:

pairlist :: a -> b -> [a]
pairlist x y = [x,y]

即使 a和 b仅代表类型，这也很好(因为只要 a和 b是同一类型，它就适用于 *类型的任何 a和 b，因为它可以工作。相反，它被类型检查器拒绝，因为两个刚性的Haskell类型变量 a和 b无法统一。

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

pluralize :: forall a . [a] -> [a]

因此，当 a被确定为“代表” Char时，正是这种 forall a量化的矛盾引发了错误。该论点的问题在于，两种解释实际上或多或少是等效的。因为Haskell类型变量是刚性的(即因为Haskell中的类型签名被隐式地普遍量化)，所以类型无法统一(即，统一与量化矛盾)。但是，事实证明，“刚性类型变量”的解释比“隐式量化”的解释更接近于GHC类型检查器中实际发生的情况。因此，以上定义所产生的错误消息表示无法匹配刚性类型变量，而不是与通用类型变量量化相矛盾。

现在，让我们回到范围类型变量的问题。在过去，GHC的 -fscoped-type-variables扩展的实现方式大不相同。特别是对于模式类型签名，您可以编写以下内容(取自 documentation for GHC 6.0):

f :: [Int] -> Int -> Int
f (xs::[a]) (y::a) = (head xs + y) :: a

文档继续说:

The pattern type signatures on the left hand side of f express the fact that xs must be a list of things of some type a; and that y must have this same type. The type signature on the expression (head xs) [sic] specifies that this expression must have the same type a. There is no requirement that the type named by "a" is in fact a type variable. Indeed, in this case, the type named by "a" is Int. (This is a slight liberalisation from the original rather complex rules, which specified that a pattern-bound type variable should be universally quantified.)

继续给出了使用范围类型变量的一些其他示例，例如:

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

k (x::a) True    = ...        -- a unifies with Int
k (x::Int) False = ...

在2006年，Simon Peyton-Jones做出了很大的 promise ( ac10f840 )，以增加对类型系统的隐含性，这最终也大大改变了词法作用域类型变量的实现。提交文本包含对更改的详细说明，包括新设计的要求。

一个关键的设计选择是现在将词法范围的类型变量命名为刚性(即用户指定的多态)Haskell类型变量，而不是像简单地代表一种类型并受统一约束的HM风格变量一样。

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

太糟糕了……旧的设计可能是一个怪异的破解方法，它使作用域类型变量更像HM类型变量，与“常规” Haskell类型变量有很大不同，而新系统使它们更加与无范围类型变量的行为保持一致。

但是，进一步使事情复杂化的是，注释中的@duplode链接引用了一个提议，该提议在模式匹配的签名上下文中部分“撤消”此“限制”。我认为可以这样说，旧的设计将作用域类型变量更像是一种特例，但不如新的设计更好地统一了作用域和非作用域类型变量的处理，并且没有回头路的愿望。到旧的实现。但是，新的，更简单的实现方式具有不必要的局限性，即对模式签名的限制，这种模式签名应被视为允许使用非刚性类型变量的特殊情况。