Haskell STM check function returning undefined

Question

Is there a good reason why the check function in the Contol.Concurent.STM library has type Bool -> STM a and returns undefined on success rather then having the type Bool -> STM ()? The way it is implemented the type checker will polity compile a do block ending with check foo only to fail at runtime with *** Exception: Prelude.undefined.

Dian

This is a good question; it seems like the check described in the STM invariants paper is now called alwaysSucceeds. It's not clear to me what the current check does. – Lasalle

Yeah, I have no idea what the purpose of having it like that might be. Kinda curious now. – Introductory

check b = if b then return undefined else retry I claim it should read check b = if b then return () else retry – Dian

Answer 1

It looks like it's a placeholder definition for a GHC PrimOp, like the "definition" seq _ y = y that gets replaced by the compiler with the actual primitive implementation code. The PrimOp implementation of check takes an expression and adds it to a global list of invariants as described in the STM invariants paper.

Here's a super-contrived example modified from that paper to fit the new type of 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

Realistically, this would be useful to assert invariants on shared state where failing the assertion might be a sign of a temporary inconsistency. You might then want to retry with the expectation of that invariant becoming true again eventually, but since this example winds up permanently breaking the invariant, it just calls retry forever and appears to hang. Check out the paper for much better examples, but keep in mind that the type has changed since its publication.

Lasalle

I understand how check works. I don't understand why it is written in such a way that check True >>= writeTVar t will pass type checking, but cause a runtime error. I assert that the above code should fail type check unless t is the rather useless type TVar (). – Dian

Ahhh, I thought the question was more in the direction of, "if this is all the code is, what's the point?" I agree that it seems like the type should be Bool -> STM (). – Lasalle