9

ライブラリ内のcheck関数に型があり、型を持つのではなく成功時に返される正当な理由はありますか? 型チェッカーが実装されている方法では、実行時にのみ失敗する で終わる do ブロックをポリシー コンパイルします。Contol.Concurent.STMBool -> STM aundefinedBool -> STM ()check foo*** Exception: Prelude.undefined

4

1 に答える 1

5

コンパイラによって実際のプリミティブ実装コードに置き換えられる「定義」のように、 GHC PrimOpのプレースホルダー定義のように見えます。seq _ y = yPrimOp 実装は式を取り、 checkSTM 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れてハングしているように見えます。より良い例については論文をチェックしてください。

于 2011-12-03T02:54:48.973 に答える