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

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


haskell ghc stm
person John F. Miller    schedule 03.12.2011    source источник
comment
Это хороший вопрос; похоже на check, описанный в Документ по инвариантам STM теперь называется alwaysSucceeds. Мне непонятно, что делает текущий check.   -  person acfoltzer    schedule 03.12.2011
comment
Да я понятия не имею, для чего это может быть. Уже любопытно.   -  person C. A. McCann    schedule 03.12.2011
comment
check b = if b then return undefined else retry Я утверждаю, что следует читать check b = if b then return () else retry   -  person John F. Miller    schedule 03.12.2011

Ответы (1)


arrow_upward
5
arrow_downward

Похоже, это определение-заполнитель для 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 навсегда и, похоже, зависает. Ознакомьтесь с документом, чтобы найти гораздо лучшие примеры, но имейте в виду, что шрифт изменился с момента его публикации.

person acfoltzer    schedule 03.12.2011
comment
Я понимаю, как работает проверка. Я не понимаю, почему это написано так, что check True >>= writeTVar t пройдет проверку типов, но вызовет ошибку времени выполнения. Я утверждаю, что приведенный выше код не должен проверять тип, если только t не является довольно бесполезным типом TVar (). - person John F. Miller; 03.12.2011
comment
Аааа, я думал вопрос больше в сторону, если это весь код, то какой смысл? Я согласен, что тип должен быть Bool -> STM (). - person acfoltzer; 03.12.2011