如果不使用类型类约束，forall 有啥用处？

Posted 2023-03-28

【中文标题】如果不使用类型类约束，forall 有啥用处？

【英文标题】：What's the utility of forall if not using type class constraint?如果不使用类型类约束，forall 有什么用处？

【发布时间】：2021-03-15 05:56:05

【问题描述】：

我已经读完了the Existential Types Wikibook，它比较了使用forall 和使用小写字母来定义泛型类型。然后它说forall 的真正用处在于将它与类型类一起使用。也就是说，forall 使您的函数适用于许多符合某个类型类的类型。

例子：

 data ShowBox = forall s. Show s => SB s

好吧，我找到了一个真正的世界用法：

spock :: forall conn sess st. SpockCfg conn sess st -> 
                               SpockM conn sess st () -> IO Middleware
<Source>

你可以在source 中看到它使用forall 但没有类型类约束：

spock :: forall conn sess st. SpockCfg conn sess st -> 
                               SpockM conn sess st () -> IO Wai.Middleware
spock spockCfg spockAppl =
    do connectionPool <-
           case poolOrConn of
             PCNoDatabase ->
             - ... -

我对 Haskell 很陌生，并试图理解 forall。

【问题讨论】：

有问题吗？

@SimonShine 问题在标题中。

大概当 Existential Types Wikibook 声称使用 forall 时，它专门谈论使用 forall 来声明存在类型。所以我不会过多解读这个说法——它只是说，对于存在主义，需要类约束才能做任何有趣的事情。

【参考方案1】：

首先，忘记存在主义。它们有点麻烦 - 我个人从不使用该扩展名，只在需要时使用更通用的 -XGADTs。另外，请允许我使用 ∀ 符号进行通用量化，我发现更多可读。 （请注意，它看起来有点像 \ lambda，它是 ∀ 的值级类似物。）这需要 -XUnicodeSyntax。

所以，签名

spock :: ∀ conn sess st. SpockCfg conn sess st -> SpockM conn sess st () -> IO Middleware

就所有外部目的而言，与

完全相同

spock :: SpockCfg conn sess st -> SpockM conn sess st () -> IO Middleware

或

spock :: SpockCfg c s t -> SpockM c s t () -> IO Middleware

当您看到这样一个带有显式∀ 的签名时，原因通常与-XExistentialQuantification 或-XRankNTypes 无关。相反，他们要么只是发现明确说明什么是类型变量更清楚，要么定义可以使用-XScopedTypeVariables。比如这两个定义其实是不一样的：

-# LANGUAGE ScopedTypeVariables, UnicodeSyntax #-

foo :: a -> a
foo x = xAgain
 where xAgain :: a
       xAgain = x

foo' :: ∀ a . a -> a
foo' x = xAgain
 where xAgain :: a
       xAgain = x

foo 无法编译，因为全局和本地签名都被解释为隐式量化，即作为

foo :: ∀ a . a -> a
foo x = xAgain
 where xAgain :: ∀ α . α
       xAgain = x

但这不起作用，因为现在xAgain 必须具有独立于您传入的x 类型的多态类型。相比之下，在foo' 中，我们只量化一次，而不是@全局定义的 987654342@ 也是本地使用的类型。

在spock 的示例中，它们甚至不使用作用域类型变量，但我怀疑它们是在调试期间使用的，然后就将∀ 留在了那里。

【讨论】：

问题中的source 有-# LANGUAGE ScopedTypeVariables #- 所以你的怀疑似乎是合理的

使用forall 的第三个理由：您希望函数的使用者使用TypeApplications，并且您希望修复类型参数的顺序。

...我现在看到它会打败我！

【参考方案2】：

一个直接的实用程序是TypeApplications 扩展，它允许我们显式选择类型变量的顺序：

 > foo :: forall a b. a -> b -> b ; foo x y = y
 > :t foo @ Int 1 2
foo @ Int 1 2 :: Num b => b    -- Int goes to the first argument

 > foo :: forall b a. a -> b -> b ; foo x y = y
 > :t foo @ Int 1 2
foo @ Int 1 2 :: Int           -- Int goes to the second argument

我在链接中找不到具体提到的，但是上面的交互是在repl.it中测试的。

嗯，实际上，链接上的一般描述确实适用：b 出现在forall b a. a -> b -> b 中首先，当它从左到右阅读时。

【参考方案3】：

类似的类型声明

f :: A a -> B b -> C

是隐含的普遍量化的，即意思相同

f :: forall a b . A a -> B b -> C

两者均表示：f 具有多态类型，其中 a 和 b 可以是任何类型（即范围超过 所有 类型）。在这种情况下，forall 的范围是 whole 类型表达式，它通常被忽略，但它总是隐含地存在。在您的示例中，它是显式编写的，可能是为了巧妙地枚举类型变量。

但是，在某些情况下，即使没有类型类，您也需要 forall：rank-N types，其中 forall 的范围不是整个类型表达式。

在ST monad 中使用了一个众所周知的示例，您可以在其中看到该函数：

runST :: forall a. (forall s. ST s a) -> a

请注意，可以省略第一个forall，如上例所示，但不能省略第二个。另请注意，runST 的类型中没有类型类约束。

【讨论】：

假设第一个多余的forall a. 被删除，那么删除forall s. 的后果/意义是什么（或至少尝试这样做）？

那么runST 将有一个依赖于s 的类型，这意味着s 类型的值可以从应用程序rumST st 中“逃脱”。使用forall，它们仍然完全不透明。