Функция проверки Haskell STM возвращает неопределенную

Question

Есть веская причина, почему check функция в Contol.Concurent.STM Библиотека имеет тип Bool -> STM a и возвращается undefined об успехе, а не иметь типа Bool -> STM ()? То, как он реализован, проверка типа будет компиляция блока DO check foo Только чтобы провалиться во время выполнения с *** Exception: Prelude.undefined.

Answer 1

Похоже, это определение заполнителя для GHC Primop, как «определение» seq _ y = y Это заменяется компилятором фактическим примитивным кодом реализации. А Primop реализация check принимает выражение и добавляет его в глобальный список инвариантов, как описано в 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 навсегда и, кажется, висит. Проверьте статью для гораздо лучших примеров, но имейте в виду, что тип изменился с момента ее публикации.