范围类型变量的意义代表类型变量而不是类型

Posted 2023-03-28

【中文标题】范围类型变量的意义代表类型变量而不是类型

【英文标题】：Significance of scoped type variables standing for type variables and not types

【发布时间】：2018-08-08 04:28:25

【问题描述】：

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

作用域类型变量代表类型变量，而不代表类型。 （这与 GHC 早期的设计有所不同。）

我知道作用域类型变量扩展的一般用途，但我不知道这里区分代表类型变量和代表类型的含义。从语言用户的角度来看，这种差异有什么意义？

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

【问题讨论】：

有an accepted GHC proposal for lifting this restriction。它的“动机”部分很好地解释了这个问题。

问好问题，我完全不知道这个限制。

【参考方案1】：

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

更长的答案：

首先，抛开作用域类型变量的问题，考虑以下几点：

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

如果a，作为一个类型变量，简单地“代表一个类型”，这样就好了。 GHC 将确定a 代表Char 类型，而生成的签名[Char] -> [Char] 将被确定为pluralize 的正确类型，因此没有问题。事实上，如果我们推断以下类型：

pluralize x = x ++ "s"

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

相反，这被 GHC 类型检查器拒绝，因为此类型签名中的 a 不是 HM 样式的类型变量，因此 not 仅代表一个类型。相反，它是一个刚性的（即用户指定的）Haskell 类型变量，并且类型检查器在定义pluralize 时不允许这样的变量与除自身之外的任何东西统一。

同样，以下内容被拒绝：

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

即使，如果 a 和 b 只代表类型，这也可以（因为它适用于任何类型的 a 和 b *，只要 a 和 @987654350 @ 是同一类型）。相反，它会被类型检查器拒绝，因为两个刚性 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

文档接着说：

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 = ...

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

一个关键的设计选择是词法范围的类型变量现在命名为刚性（即用户指定的多态）Haskell 类型变量，而不是更像 HM 风格的变量，只是代表一个类型并服从统一。

这使得上述示例（f、g 和 k）非法，因为模式匹配中的作用域类型变量现在表现得更像常规刚性类型变量。

太棒了...旧设计可能是一种奇怪的 hack，它使作用域类型变量更像 HM 类型变量，与“普通”Haskell 类型变量完全不同，而新系统使它们更符合无作用域类型变量的行为。

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

【参考方案2】：

我正在添加这个答案（对我自己的问题），以便在 cmets 中扩展 duplode 的参考。目前正在更改 ScopedTypeVariables 以允许作用域类型变量代表类型，而不仅仅是类型变量。对此的讨论改变了新旧设计的动机。但是，这不解决了问题和 K. A. Buhr 的回答中提到的更早的设计。

在当前状态下，在即将发生的变化之前，定义

prefix :: a -> [[a]] -> [[a]]
prefix (x :: b) yss = map xcons yss
    where xcons ys = x : ys

有效（使用 ScopedTypeVariables），其中b 是新引入的类型变量，代表与a 相同的东西。另一方面，如果prefix 专门用于

prefix :: Int -> [[Int]] -> [[Int]]
prefix (x :: b) yss = map xcons yss
    where xcons ys = x : ys

然后程序被拒绝：b 被禁止代表Int，因为Int 不是类型变量。 Simon Peyton Jones 评论了为什么它被设计成 b 不能代表 Int：

当时我担心有一个类型会令人困惑 变量只是 Int 的别名；那不是类型变量 一点也不。但是在这些 GADT 和类型平等的日子里，我们都习惯了 到那个。今天我们会做出不同的选择。

在 GHC 维护者的当前共识中，限制 b 代表 Int 被认为是不自然的，特别是考虑到类型相等 (a ~ Int) => ... 的可能性。这种约束的存在模糊了“绑定到类型变量”的真正含义。应该举例

f1 :: (a ~ Int) => Maybe a -> Int
f1 (Just (x :: b)) = ...

f2 :: (a ~ Int) => Maybe Int -> Int
f2 (Just (x :: a)) = ...

被允许？根据新提案，上述四个例子都是允许的。

---

在我自己看来，张力最终来自于两种截然不同的类型注释系统的共存。其中之一具有防止您为同一类型赋予不同名称的效果（例如，您不能写(\x -> x) :: a -> b 或(\x -> x) :: Int -> b 并期望b 与a 统一或Int)。另一个启用并鼓励您为事物赋予新名称（模式类型签名，如foo (x :: b) = ...），该功能使您能够命名否则无法命名的类型。剩下的问题是模式类型签名是否应该允许您对已经可命名的类型进行别名。其核心答案取决于您认为这两个先例中的哪一个更引人注目。

---

参考资料：

Joachim Breitner “nomeata”（2018 年 4 月至 8 月）。功能请求票“ScopedTypeVariables 可以允许更多程序”，https://ghc.haskell.org/trac/ghc/ticket/15050 nomeata（2018 年 4 月至 8 月）。拉取请求“允许 ScopedTypeVariables 引用类型”，https://github.com/ghc-proposals/ghc-proposals/pull/128 Richard A. Eisenberg、Joachim Breitner 和 Simon Peyton Jones（2018 年 6 月）。 “在模式中键入变量”，https://www.microsoft.com/en-us/research/uploads/prod/2018/06/tyvars-in-pats-haskell18-preprint.pdf，尤其是第 3.5 和 4.3 节 nomeata（2018 年 8 月）。 GHC 提案“允许 ScopedTypeVariables 引用类型”，https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0029-scoped-type-variables-types.rst