forward-chan

Haskell channels with the forwarding primitive

Monthly Downloads: 3

Programming language: Haskell

License: LicenseRef-Apache

Tags: Concurrency    

README

forward-chan

• An more complete implementation of the forward primitive from the identity rule for the proof terms for the sequent caluclus formulation of linear logic

• The assurances of linear logic make the primitive stated in the paper above easy to implement - namely each channel can only be used once for input and once for output. Thus an implementation made entirely for linear logic need only read from one channel once and write the value to the forwarded channel. In a non linear context however, this is a woefully insufficient primitive. Ideally you'd want this to enable permanent (and retroactive) bidirectional forwarding, and not one time directional forwarding. The remaining question is then how to build it and what specification it needs. This package solves that problem.

• on hackage

Forward Specification

• Commutivity: forwardChan a b === forwardChan b a

• Behavioral Transitivity: (forwardChan a b >> forwardChan b c) === (forwardChan a b >> forwardChan a c)

• Equal Opportunity: For each of the following senarios (with c1 and c2 just created with newChan), there are possible executions which will print out "1" and possible executions which it will print "2", but it will never print both, and provided one of the threads isn't starved by an external thread, it will always print one of them.

writeChan () c1
forwardChan c1 c2
forkIO $ do
   readChan c1
   putStrLn "1"
readChan c2
putStrLn "2"

forwardChan c1 c2
writeChan () c1
forkIO $ do
   readChan c1
   putStrLn "1"
readChan c2
putStrLn "2"

forkIO $ do
   readChan c1
   putStrLn "1"
forkIO $ do
    readChan c2
    putStrLn "2"
forwardChan c1 c2
writeChan () c1

forkIO $ do
   readChan c1
   putStrLn "1"
forkIO $ do
    readChan c2
    putStrLn "2"
writeChan () c1
forwardChan c1 c2

• Early Bird Gets The Worm: The first thread to read from either channel will, after a forward, always recieve the next available item. Similarly, items written to either channel are read in the same order they were written in. The following examples will always print out "12"

writeChan "1" c1
writeChan "2" c2
forwardChan c1 c2
readChan c1 >>= putStr
readChan c2 >>= putStr

writeChan "1" c1
writeChan "2" c2
forwardChan c1 c2
readChan c1 >>= putStr
readChan c1 >>= putStr

forwardChan c1 c2
writeChan "1" c1
writeChan "2" c2
readChan c1 >>= putStr
readChan c2 >>= putStr

forwardChan c1 c2
writeChan "1" c1
writeChan "2" c2
readChan c2 >>= putStr
readChan c2 >>= putStr