Haskell STM Controlla funzione che restituisce indefinita

Question

C'è una buona ragione per cui il check funzione in Contol.Concurent.STM La libreria ha il tipo Bool -> STM a e ritorna undefined al successo piuttosto che avere il tipo Bool -> STM ()? Il modo in cui viene implementato il tipo di controllo che la politica compilerà un blocco do che termina con check foo solo per fallire in fase di esecuzione con *** Exception: Prelude.undefined.

Answer 1

Sembra che sia una definizione di segnaposto per a GHC Primop, come la "definizione" seq _ y = y Ciò viene sostituito dal compilatore con il codice di implementazione primitivo effettivo. Il Primop Implementation di check prende un'espressione e la aggiunge a un elenco globale di invarianti come descritto nel STM Invariants Paper.

Ecco un esempio super trattato modificato da quel documento per adattarsi al nuovo tipo di 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

Realisticamente, ciò sarebbe utile affermare gli invarianti sullo stato condiviso in cui il fallimento dell'affermazione potrebbe essere un segno di un'incoerenza temporanea. Potresti quindi voler riprovare con l'aspettativa che quella invariante diventa di nuovo vera alla fine, ma poiché questo esempio finisce permanentemente rompendo l'invariante, chiama solo retry per sempre e sembra appendere. Dai un'occhiata al documento per esempi molto migliori, ma tieni presente che il tipo è cambiato dalla sua pubblicazione.