Friday, April 28, 2006

Some examples from E

I had ten minutes before lunch, and decided to code up a couple of examples from E in Haskell:

type Cont a = a -> STM ()

-- Blocking caretaker - requests are blocked until the gate is open
-- Note that the gate can be opened/closed repeatedly.
makeCaretaker :: Cont a -> STM (Cont a, Cont Bool)
makeCaretaker target = do
enabled <- newTVar True
return (\m -> do {e <- readTVar enabled ; if e then target m else retry}, writeTVar enabled)

-- Overwritable promise.
makePromise :: STM (Cont a, Cont (Cont a))
makePromise = do
queue <- newTChan
target <- newTVar Nothing
return (\m -> do
t <- readTVar target
case t of
Nothing -> writeTChan queue m
Just r -> r m
, writeTVar target . Just)

Note that both caretaker and promise allow the controller to change its mind - either by repeatedly opening/closing the gate, or by re-resolving the reference. Also, when closed, the caretaker does not signal errors or swallow messages - it keeps the senders blocked. OTOH, promise stores messages in a queue.
Of course, this can be changed (I leave this as an exercise for readers :-) ).
I may consider creating a small library of such patterns and see whether something DSLish comes of it...
But before that I must decide on verification procedure - should I use unit tests or proofs...

No comments: