Haskell STM检查函数返回undefined

Question

有没有一个很好的理由为什么库check中的Contol.Concurent.STM函数具有类型Bool -> STM a并且返回undefined成功而不是具有类型Bool -> STM ()？它实现的方式是类型检查器将polity编译一个do块结束,check foo只是在运行时失败*** Exception: Prelude.undefined.

Answer 1

看起来它是GHC PrimOp的占位符定义,就像seq _ 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永远地调用并且似乎挂起.查看该文章以获得更好的示例,但请记住,该类型自发布以来已发生变化.