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



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

作用域内类型变量代表类型变量,而不是类型。(这与GHC早期的设计有所不同。

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

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

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)型系统中,这可能正是会发生的情况。 作为键入(++)应用程序的中间步骤,类型检查器将为"新鲜"HM 类型变量ax分配类型[a],并在将[a]"s" :: [Char]类型统一pluralize以统一aChar之前分配类型[a] -> [a]

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

同样,将拒绝以下内容:

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

即使,如果ab只代表类型,那也没问题(因为它适用于任何ab*前提是ab是同一类型)。 相反,它被类型检查器拒绝,因为两个刚性的 Haskell 类型变量ab无法统一。

现在,你可以尝试说明问题在于类型变量是"刚性的",不能与具体类型(如Char)或彼此统一,而是在Haskell类型签名中存在隐式量化,因此pluralize的签名实际上是:

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

因此,当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

文档接着说:

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风格的变量,它只是代表一个类型并受到统一的影响。

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

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

然而,使事情进一步复杂化的是,评论中@duplode的链接引用了一项建议,即在模式匹配中的签名上下文中部分"撤消"此"限制"。我认为可以公平地说,旧设计更像是将作用域类型变量视为特例,不如新设计更好地统一了作用域和非作用域类型变量的处理,并且不希望回到旧的实现。 然而,新的、更简单的实现具有对模式签名不必要限制的副作用,也许应该将其视为允许非刚性类型变量的特殊情况。

我添加这个答案(在我自己的问题中)是为了在评论中扩展 duplode 的引用。ScopedTypeVariables 当前正在更改,以允许作用域类型变量代表类型,而不仅仅是类型变量。对此的讨论改变了新旧设计的动机。然而,这并没有解决问题和K.A.布尔的回答中提到的更早的设计。

在当前状态下,在即将进行的更改之前,定义

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

是有效的(使用作用域类型变量),其中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并期望baInt统一)。另一个支持并鼓励你为事物命名新名称(模式类型签名,如foo (x :: b) = ...),该功能的存在使您能够命名否则无法命名的类型。剩下的问题是模式类型签名是否应该允许您对已经可命名的类型进行别名。答案的核心取决于你认为两个先例中的哪一个更有说服力。


引用:

  1. 约阿希姆·布莱特纳"nomeata"(2018年4月至8月)。功能请求票证"ScopedTypeVariables 可能允许更多程序",https://ghc.haskell.org/trac/ghc/ticket/15050
  2. 野肉(2018年4月至8月)。拉取请求"允许作用域类型变量引用类型",https://github.com/ghc-proposals/ghc-proposals/pull/128
  3. 理查德·艾森伯格、约阿希姆·布莱特纳和西蒙·佩顿·琼斯(2018 年 6 月)。"模式中的类型变量",https://www.microsoft.com/en-us/research/uploads/prod/2018/06/tyvars-in-pats-haskell18-preprint.pdf,特别是第 3.5 和 4.3 节
  4. 野肉(2018年8月)。GHC 提案"允许作用域类型变量引用类型",https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0029-scoped-type-variables-types.rst

相关内容

  • 没有找到相关文章

最新更新