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

Question

给定以下运行 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 在避免泛化的评估上下文中始终是自由的，对吗？还是这里有更多关于通用量词的信息？

Answer 1

让我们看一下runST的类型。我还为 a 添加了一个显式限定符。

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

契约(Contract)内容如下:

1. 调用者选择一个固定类型a
2. 调用者提供一个参数x
3. 对于 s 的任何选择，参数 x 必须是 ST s a 类型。换句话说，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

这里我不是预先固定a，而是尝试选择a=s。我不允许这样做:runFoo 可以根据 a 选择 s(参见上面的 part3 ), 所以a必须提前固定。

现在，以您的示例为例。问题出在

runST (newSTRef ...)

此处，newSTRef 返回一个 ST s (STRef s Int)，因此它试图选择 a = STRef s Int。因为a依赖于s，所以这个选择是无效的。

ST monad 使用这个“技巧”来防止对 monad 的“转义”引用。也就是说，可以保证在 runST 返回后，所有引用现在都不再可访问(并且可能会被垃圾收集)。因此，在 ST 计算期间使用的可变状态已被丢弃，runST 的结果确实是一个纯值.毕竟，这是 ST monad 的主要目的:它旨在允许(临时)可变状态用于纯计算。