Skip to content

mmirman/forward-chan

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

13 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

Haskell channels with the forwarding primitive

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published