11

按照这个答案，我在我的程序中实现了一个通用的提升功能：

liftTupe :: (x -> c x) -> (a, b) -> (c a, c b) --This will error
liftTuple :: (forall x. x -> c x) -> (a, b) -> (c a, c b)

我了解，在这种情况下，forall可以x成为任何类型（[]等Maybe）。

我现在正在研究>>=Monads 中的定义：

class Applicative m => Monad m where
   (>>=) :: forall a b. m a -> (a -> m b) -> m b

我无法理解 thisforall在函数定义中的作用？因为，不像liftTuple，它没有绑定到特定的函数（x -> c x）？

4

4 回答 4

6

基本上，当你不使用时forall，所有类型在函数定义中都是全局的，这意味着它们都是在调用函数时推导出来的。forall你可以放弃这个功能，直到x它被自己调用。

因此，在第一个中，您有一个接受x和给出的函数c x，然后您有一个带有aand的元组，b并且您期望一个带有c aand的元组c b。既然您已经说过第一个函数接受x，您可以使x成为 与 相同a，但不会那样，b因为x为整个声明定义了一次。所以你不能让函数同时接受a和b。

但是，在第二种情况下，x范围仅限于函数获取x。我们基本上是在说有一个函数接受某物并c用该物生成，它可以是任何类型。这使我们能够先喂它a然后喂它b，它就会起作用。x现在在外面不必是奇异的东西。

您在Monad定义中看到的是“ExplicitForAll”语言扩展。Haskell Prime上有关于这个扩展的描述

ExplicitForAll 允许使用关键字“forall”来显式声明一个类型在其自由类型变量中是多态的。它不允许写入任何无法写入的类型；它只允许程序员显式声明（当前隐含的）量化。

这个语言扩展是纯粹的可视化的，允许你显式地写出你以前不能写的变量。您可以简单地forall a b.从Monad声明中省略，程序将在功能上保持完全相同。

说，有了这个扩展，你可以重写liftTupeas forall a b x. (x -> c x) -> (a, b) -> (c a, c b)。定义相同，功能相同，但读者现在会清楚地看到类型变量都是在最顶层定义的。

于 2017-02-05T09:15:33.587 回答
5

您编写的每个函数都隐含地对其类型变量进行了普遍量化：

id :: a -> a           -- this is actually universally quantified over a
id :: forall a. a -> a
id x = x

ExplicitForall您实际上可以使用语言编译指示打开此行为。

此属性非常有用，因为它限制您编写仅适用于某些类型的代码。想想这个id函数能做什么：它要么返回它的参数，要么永远循环。这是它唯一能做的两件事，你可以根据它的类型签名来弄清楚。

强制多态函数的所有实例以相同的方式运行，而不管参数类型如何，这称为参数化， Bartosz Milewski在这篇博文中对此进行了解释。TL;DR 是：使用参数化，我们可以保证程序结构中的某些重新排序不会影响其行为。有关对此的数学上更严格的处理，请免费参阅定理！菲利普·瓦德勒。

于 2017-02-05T09:23:50.843 回答
3

Haskell 类型系统中的所有类型变量都由forall. 但是，GHC 可以在许多情况下推断出量化，因此您无需将它们编写在源代码中。

例如，显式的liftTuple类型forall是

liftTuple :: forall c a b. (forall x. x -> c x) -> (a, b) -> (c a, c b)

对于>>=情况也是如此。

于 2017-02-05T09:22:04.850 回答
2

monad 定义中的 forall 只是为了使全称量化更加明确。如果你有一个没有进一步限制的类型变量，它默认是通用的，即可以是任何东西。

因此，让我们看看 forall 的两种用法之间的区别以及 haskell 如何看待它们：

隐式：

foo ::  (x -> f x) -> a -> b -> (f a, f b)
-- same as
foo :: forall f x a b . (x -> f x) -> a -> b -> (f a, f b)
-- our function is applied to a, so x is equal to a
foo :: forall f x a b . (x ~ a) => (x -> f x) -> a -> b -> (f a, f b)
-- our function is also applied to b, so x is equal to b
foo :: forall f x a b . (x ~ a, x ~ b) => (x -> f x) -> a -> b -> (f a, f b)

哦，(x ~ a, x~ b) 需要 (a ~ b)。这将在没有注释的情况下推断出来，但是由于我们明确使用了不同的类型变量，所以一切都爆炸了。为了解决这个问题，我们需要 f 在我们的函数中保持多态性。

标准的 haskell 无法表达这一点，所以我们需要 rank2types 或 rankntypes。有了它，我们可以写：

foo ::  (forall x . x -> f x) -> a -> b -> (f a, f b)

请注意，forall 是函数类型的一部分。这样，它在我们的函数中保持多态，我们可以将它应用于不同的类型，而不会发生任何事情！

请注意，我们也可以这样做：

foo :: Monad m => a -> b -> (m a, m b)
foo a b = (return a, return b)
于 2017-02-05T15:40:11.120 回答