普遍量化和统一，一个例子 [英] Universal quantification and unification, an example

问题描述

运行monad ST

  runST ::（全部.ST sa） - > a 
  

和函数

  newVar :: a  - > ST s（MutVar s a）
 readVar :: MutVar s a  - > ST sa 
  

然后Haskell编译器会拒绝下面的不良类型表达式

  let v = runST（newVar True）
 in runST（readVar v）
  

因为为了评估 runST ，需要类型

  readVar v :: ST s Bool 
  

必须推广到

 ∀s。 ST s Bool 
  

我的问题是，这里的Universal量词的唯一工作就是确保类型变量 s 在评估环境中总是免费的，以避免泛化，对吗？或者在这里有更多关于通用量词的信息？

C $ C>。我还为 a 添加了一个明确的分词符。

  runST ::全部（全部ST ST） - > a 
  

它读作以下合约：

1. 调用者选择一个固定类型 a


2. 调用者提供一个参数 x


3. 参数 x 必须是 ST sa 用于任何 s 的选择。换句话说， s 将由 runST 选择，而不是调用者。



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



  runFoo :: forall a 。 （全部s  - > [（s，a）]） - > [a] 
 runFoo x = 
 let part1 = xhello！ - 这里s是字符串
  -  part1有类型[（String，a）] 
 part2 = x'a' - 这里s是Char 
  -  part2有类型[（Char ，a）] 
 part3 = x（map snd part2） - 这里s是[a]（!!!）
  -  part3的类型是[（[a]，a）] 
 in map snd part1 ++ map snd part2 ++ map snd part3 
 
 test1 :: [Int] 
 test1 = runFoo（\y  - > [（y，2）， （y，5）]） - 这里a是Int 
 
 test2 :: [Int] 
 test2 = runFoo（\y  - > [（abc++ y， 2）]） -  **错误
  - 我不能选择y :: String，runFoo会选择这种类型！ 
  

请注意， a 是固定的到 Int ），并且我不能对 y 的类型设置任何限制。此外：



  test3 = runFoo（\y  - > [（y，y）]） -  ** error 
  

这里我是 not 修正 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中的escape。也就是说，保证在 runST 返回后，所有引用现在不再可访问（并且可能会被垃圾回收）。因此，在 ST 计算过程中使用的可变状态已被丢弃，并且 runST 确实是一个纯值。毕竟，这是 ST monad的主要目的：它意味着允许（临时）可变状态用于纯计算。

Given the following signature for running the monad ST

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

and the functions

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

Then the Haskell compiler will reject the following ill-typed expression

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

Because in order to evaluate runST, it's required that the type

readVar v :: ST s Bool 

must be generalized to

∀s . ST s Bool 

My question is then that the only job of the Universal quantifier here, is to ensure that the type variable s is always free in the context of evaluation avoiding generalization, am I right? or is there more about the universal quantifier here?

解决方案

Let's read the type of runST. I added an explicit quatifier for a as well.

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

It reads as the following contract:

1. the caller chooses a fixed type a
2. the caller provides an argument x
3. the argument x must be of type ST s a for any choice of s. In other words, s will be chosen by runST, not by the caller.

Let's see a similar example:

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!

Above, note that a is fixed (to Int), and that I can't put any restrictions on the type of y. Moreover:

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

Here I am not fixing a in advance, but I'm trying to choose a=s. I am not allowed to do that: runFoo is allowed to choose s in terms of a (see part3 above), so a must be fixed in advance.

Now, to your example. The problem lies in

runST (newSTRef ...)

Here, newSTRef returns a ST s (STRef s Int), so it's trying to choose a = STRef s Int. Since a depends on s, this choice is invalid.

This "trick" is used by the ST monad to prevent references to "escape" from the monad. That is, it is guaranteed that after runST returns, all the references are now no longer accessible (and potentially they can be garbage collected). Because of this, the mutable state which was used during the ST computation has been thrown away, and the result of runST is indeed a pure value. This is, after all, the main purpose of the ST monad: it is meant to allow (temporary) mutable state to be used in a pure computation.

这篇关于普遍量化和统一，一个例子的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！