相关疑难解决方法(0)

我开始理解forall关键字如何在所谓的"存在类型"中使用,如下所示:

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

然而,这仅仅是如何forall使用的一个子集,我根本无法将其用于这样的事情:

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

或解释为什么这些是不同的:

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

或整个RankNTypes东西......

我倾向于选择清晰,无术语的英语而不是学术环境中常见的语言.我尝试阅读的大部分解释(我可以通过搜索引擎找到的解释)存在以下问题:

1. 他们不完整.他们解释如何使用这个关键字(如"生存型")的一个组成部分这让我感到高兴,直到我读使用它在一个完全不同的方式代码(比如runST,foo和bar以上).
2. 他们密集地充满了假设,我已经阅读了最新的离散数学分类,类别理论或抽象代数本周流行.(如果我再也没有读过"请参阅论文的任何细节",那就太早了.)
3. 它们的编写方式经常将简单的概念转变为曲折的语法和语法.

所以...

关于实际问题.任何人都可以完全解释的forall清晰,简单的英语关键字(或者,如果它存在于某个地方,点到我已经错过了这样一个明确的解释),不承担我在行话悠久的数学家？

编辑添加:

下面有高质量的答案有两个突出的答案,但不幸的是我只能选择一个最好的答案. 诺曼的回答很详细的和有用的,解释的方式,表现出一定的理论基础的东西forall,并在同一时间向我展示了一些它的实际影响. yairchu的回答覆盖了其他人没有提到的范围(范围类型变量),并用代码和GHCi会话说明了所有概念.我愿意选择两者是最好的.不幸的是,我不能和上,俯瞰着两个答案后密切,我已经决定,yairchu的稍微挤掉了诺曼,因为说明性代码和附加的说明.这是一个有点不公平,但是,因为我真的需要这两个答案,了解这一点是一点forall没给我留下了恐惧的隐隐感觉,当我看到它在类型签名.

这里有一些pragma和一些导入:

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Monad.ST
import Data.Array.ST
import Data.Array

现在这是我的问题.以下代码类型检查:

foo :: forall a. a -> [a]
foo x = elems $ runSTArray $ do
    newListArray (1,10) (replicate 10 x) :: ST s (STArray s Int a)

但是,当我更换$组合物时:

foo :: forall a. a -> [a]
foo x = elems . runSTArray $ do
    newListArray (1,10) (replicate 10 x) :: ST s (STArray s Int a)

我收到此错误:

Couldn't match expected type `forall s. ST s (STArray s …