Haskell STM检查函数返回未定义答案

【问题标题】：Haskell STM check function returning undefinedHaskell STM检查函数返回未定义
【发布时间】：2011-12-03 01:58:10
【问题描述】：

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

【问题讨论】：

这是个好问题；似乎STM invariants paper 中描述的check 现在称为alwaysSucceeds。我不清楚当前的check 做了什么。
是的，我不知道那样做的目的是什么。现在有点好奇。
check b = if b then return undefined else retry 我声称它应该是check b = if b then return () else retry

标签： haskell ghc stm

【解决方案1】：

它看起来像是GHC PrimOp 的占位符定义，就像“定义”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

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

【讨论】：

我了解检查的工作原理。我不明白为什么它以check True >>= writeTVar t 将通过类型检查的方式编写，但会导致运行时错误。我断言上面的代码应该无法通过类型检查，除非t 是相当无用的类型TVar ()。
啊，我认为问题更倾向于“如果这就是所有代码，那有什么意义？”我同意类型应该是Bool -> STM ()。