通用量化和统一，一个例子

给出运行 monad 的以下签名ST

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

和功能

newVar  :: a -> ST s (MutVar s a) 
readVar :: MutVar s a -> ST s a

那么Haskell编译器将拒绝以下错误类型的表达式

let v = runST (newVar True)
in runST (readVar v)

因为为了评价runST，要求类型

readVar v :: ST s Bool 

必须概括为

∀s . ST s Bool 

我的问题是，通用量词的唯一作用是确保类型变量s在评估避免泛化的情况下总是免费的，对吗？或者这里还有更多关于全称量词的信息吗？

我们来读一下类型runST。我添加了一个显式限定符a以及。

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

其内容如下：

1. 调用者选择固定类型a
2. 调用者提供一个参数x
3. 论证x必须是类型ST s a对于任何选择s。换句话说，s将被选择runST，不是由调用者发出的。

让我们看一个类似的例子：

runFoo :: forall a . (forall s. s -> [(s,a)]) -> [a]
runFoo x =
    let part1 = x "hello!"          -- here s is String
        -- part1 has type [(String, a)]
        part2 = x 'a'               -- here s is Char
        -- part2 has type [(Char, a)]
        part3 = x (map snd part2)   -- here s is [a]   (!!!)
        -- part3 has type [([a],a)]
    in map snd part1 ++ map snd part2 ++ map snd part3

test1 :: [Int]
test1 = runFoo (\y -> [(y,2),(y,5)])   -- here a is Int

test2 :: [Int]
test2 = runFoo (\y -> [("abc" ++ y,2)])       -- ** error
-- I can't choose y :: String, runFoo will choose that type!

上面，请注意a是固定的（至Int），并且我不能对类型进行任何限制y。而且：

test3 = runFoo (\y -> [(y,y)])    -- ** error

我在这里not fixing a提前，但我正在尝试选择a=s。我不被允许这样做：runFoo被允许选择s按照a (see part3上），所以a必须提前固定。

现在，以你的例子为例。问题在于

runST (newSTRef ...)

Here, newSTRef返回一个ST s (STRef s Int)，所以它试图选择a = STRef s Int. Since a依赖于取决于s，该选择无效。

这个“伎俩”被使用STmonad 以防止从 monad 中引用“escape”。也就是说，保证之后runST返回，所有引用现在都不再可访问（并且可能它们可以被垃圾收集）。因此，在ST计算已被丢弃，并且结果runST确实是一个pure价值。毕竟，这才是该项目的主要目的。STmonad：它的目的是允许在纯计算中使用（临时）可变状态。