3

我已经阅读了 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>

你可以在这里看到它使用的源代码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.

4

3 回答 3

5

首先，忘记存在主义。它们有点麻烦——我个人从不使用那个扩展，只有-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

当您看到这样的显式签名时，原因通常与or∀没有任何关系。相反，他们要么只是发现明确说明什么是类型变量更清楚，要么定义可以使用. 例如，这两个定义实际上是不同的：-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'我们只量化一次，并且a来自全局定义的类型也是在本地使用的类型.

在 的示例中spock，他们甚至不使用范围类型变量，但我怀疑他们在调试期间使用了，然后就离开了∀那里。

于 2021-03-15T10:17:10.750 回答
3

类型声明，如

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

是隐含的普遍量化的，即与

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

两者都意味着：f具有多态类型，其中a和b可以是任何东西（即范围涵盖所有类型）。在这种情况下， 的范围forall是整个类型表达式，它通常被忽略，但它总是隐含地存在。在您的示例中，它是明确编写的，可能是为了巧妙地枚举类型变量。

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

在你看到函数的STmonad中使用了一个众所周知的例子：

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

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

于 2021-03-15T08:20:53.673 回答
3

一个直接的实用程序是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

于 2021-03-15T11:41:12.463 回答