Haskell STM检查函数返回undefined

Question

Haskell STM检查函数返回undefined

9

< p >在Contol.Concurent.STM库中，check函数的类型为Bool -> STM a，成功时返回undefined，而不是具有Bool -> STM ()类型的原因是否充分？实现方式使得类型检查器只能编译以check foo结尾的代码块，但最终会在运行时失败并显示：*** Exception: Prelude.undefined。 < / p >

- John F. Miller

这是一个好问题。似乎在STM不变量论文中所描述的check现在被称为alwaysSucceeds。我不清楚当前的check具体作用是什么。 - acfoltzer

是的，我不知道这样做的目的是什么。现在有点好奇。 - C. A. McCann

检查 b = 如果 b，则返回未定义，否则重试。我认为它应该是“检查 b = 如果 b，则返回()，否则重试”。 - John F. Miller

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- acfoltzer · Accepted Answer

看起来这是一个占位符定义，用于GHC PrimOp，类似于“定义”seq _ y = y，编译器会将其替换为实际的基本实现代码。 check 的 PrimOp 实现接受一个表达式，并将其添加到全局不变量列表中，如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并似乎挂起。请查看论文以获取更好的示例，但请记住，自其出版以来类型已经发生了变化。