9

check库中的Contol.Concurent.STM函数有 typeBool -> STM a并返回undefined成功而不是type有充分的理由Bool -> STM ()吗？它的实现方式类型检查器将编译一个以 结尾的 do 块，check foo仅在运行时以*** Exception: Prelude.undefined.

4

1 回答 1

5

看起来它是GHC PrimOpseq _ y = y的占位符定义，就像编译器用实际的原始实现代码替换的“定义” 。PrimOp的实现check采用表达式并将其添加到不变量的全局列表中，如STM 不变量论文中所述。

这是从那篇论文修改的一个超级设计的例子，以适应新的类型check：

import Control.Concurrent.STM

data LimitedTVar = LTVar { tvar  :: TVar Int
                         , limit :: Int
                         }

newLimitedTVar :: Int -> STM LimitedTVar
newLimitedTVar lim = do 
  tv <- newTVar 0
  return $ LTVar tv lim

incrLimitedTVar :: LimitedTVar -> STM ()
incrLimitedTVar (LTVar tv lim) = do
  val <- readTVar $ tv
  let val' = val + 1
  check (val' <= lim)
  writeTVar tv val'

test :: STM ()
test = do
  ltv <- newLimitedTVar 2
  incrLimitedTVar ltv -- should work
  incrLimitedTVar ltv -- should work still
  incrLimitedTVar ltv -- should fail; we broke the invariant

实际上，这对于在共享状态上断言不变量很有用，其中断言失败可能是暂时不一致的标志。然后，您可能希望重试该不变量最终再次变为真的期望，但由于此示例最终会永久破坏该不变量，因此它只会retry永远调用并且似乎挂起。查看该论文以获得更好的示例，但请记住，该类型自发布以来已发生变化。

于 2011-12-03T02:54:48.973 回答