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 回答