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

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.我也添加了一个明确的quatifier 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固定(to Int),并且我不能对类型进行任何限制y.此外:

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

在这里,我没有固定a提前,但我想选择a=s.我不允许这样做:runFoo允许选择s在以下方面a(见part3上文),因此a必须事先确定.

现在,举个例子.问题在于

runST (newSTRef ...)

在这里,newSTRef返回a ST s (STRef s Int),所以它试图选择a = STRef s Int.由于a依赖s,这种选择无效.

STmonad 使用这个"技巧" 来阻止对monad的"逃避"的引用.也就是说,保证在runST返回之后,现在不再可以访问所有引用(并且可能它们可以被垃圾收集).因此,在ST计算过程中使用的可变状态已被丢弃,结果runST确实是纯值.毕竟,这是STmonad 的主要目的:它意味着允许(临时)可变状态用于纯计算.