Haskell STM检查函数返回未定义

为什么有充分的理由使check库中的Contol.Concurent.STM函数具有Bool -> STM a类型，并在成功时返回undefined而不是具有Bool -> STM ()类型？类型检查器的实现方式将通过polity编译一个以check foo结尾的do块，仅在运行时使用*** Exception: Prelude.undefined失败。

最佳答案

看起来这是GHC PrimOp的占位符定义，例如“definition” seq _ y = y被编译器替换为实际的原始实现代码。 PrimOp implementation of check 接受一个表达式并将其添加到STM invariants paper中描述的不变量的全局列表中。

这是从该论文修改而来的新示例，以适应新的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

实际上，这对于在共享状态下声明不变式很有用，因为如果声明失败，则可能表示暂时的不一致。然后，您可能希望重试该不变量最终最终变为true的期望，但是由于此示例永久性地破坏了该不变量，因此它只会永久调用retry并似乎挂起。请查看本文以获取更好的示例，但请记住，自发布以来，该类型已发生变化。

关于Haskell STM检查函数返回未定义，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/8364903/