Haskell-Join-Rules

What is Haskell-Join-Rules?

Haskell-Join-Rules is a proposed Haskell language extension that introduces join style patterns which are compiled into CHR rules. Join patterns is a concurrency abstraction based on join calculus, with implementations found in JoCaml and Polyphonic C#. An example of Polyphonic C# (Communication Buffers): 

   public class Buffer {
      public async Put(string s);
      public string Get() & Put(string s) { return s; }
   }

In Haskell-Join-Rules, we can write the join pattern above as: 

   Channel Buffer where
      sync  get :: Join Int
      async put :: Int -> Join ()

   Chord x@get & put(y) where
      x = return y

These declarations are essentially compiled into the Haskell codes + CHR rule: 

   get :: Join Int
   get = do { x <- newCont  -- create a new continuation
            ; sync $ Get(x) -- Add a predicate Get(x) and block
            ; runCont x     -- Run the continuation }

   put :: Int -> Join ()
   put y = async $ Put(y)   -- Add a predicate Put(y) and proceed

   Get(x),Put(y) <==> x is (return y)  -- CHR rule, binds continuation x when triggered.

Synchronous calls are blocked and synchronized by a simple continuation passing mechanism, similar to JoCaml. Join style patterns in the context of Haskell have already been explored earlier (In Satnam Singh's "Higher Order Combinators for Join Patterns using STM"), Haskell-Join-Rules is novel as join patterns are compiled into CHR, hence we can introduce unique CHR features (propagation and guards) to our join patterns.

The following lists some examples of Haskell-Join-Rule's novel features

Guarded Join-Patterns

In Haskell-Join-Rules, we can write join patterns with guards and non-linear patterns. For example: 

   Channels CondBuffer where
      sync  cget :: (Int -> STM Bool) -> Join Int
      async cput :: Int -> Join ()

   Chord x@get(f) & put(y) | f y where
      x = return y

This variant of the Buffer example allows selective cget operations that picks a cput depending on the higher order function f. Note that guards in the context of join patterns is a non-trivial extension:

By compiling Chords into CHRs and allowing a CHR solver to deal with the triggering of the chords (search for matching constraints and rewritings), we get for free an efficient way of handling guarded join-patterns. Further more the CHR operational semantics and various optimization techniques (eg. optimal join ordering, early guard scheduling) have already been intensively studied through out the decade.

Propagated Calls and Non-linear Patterns

Haskell-Join-Rules also introduces propagation and non-linear patterns to join-patterns. Consider the following: 

   Channels AuthBuffer where
      async auth :: String -> Join ()
      sync  aget :: String -> Join Int
      async aput :: Int -> Join ()

   Chord auth(id) / x@aget(id) & put(y) where
      x = return y

This variant of the Buffer example only allows successful aget operations from authorized sources, modelled naively with string matching. A async call auth(id) simply indicates that id is authorized (let's take for granted the privatization of such methods). Note that we do not want to remove the auth(id) 'token' upon successful triggering of the chord, hence the chord is defined with auth(id) coming before a '/'. Such calls are known as propagated calls and are not deleted when the chord triggers. Though we can alway write programs that do not require propagation (simply replace them in the body upon firing), propagation promotes better concurrency behaviour, as multiple calls can share the same propagated call, and we avoid pointless removal and reintroduction of the same calls.

Note that we have a non-linear pattern here too: id appears in 2 distinct positions of the chord head. We deal with non-linear patterns by renaming occurrences and inserting the relevant equally guards.

Combining the novel features

With these novel features we can write a lot more interesting and useful concurrent programs. For instance the following is a typical implementation union find described by most CHR sites, which efficiently maintains disjoint sets: 

Channels UnionFind where
   sync  make  :: Char -> Join ()
   async root  :: Char -> Join ()
   sync  union :: (Char,Char) -> Join ()
   sync  find  :: Char -> Join Char
   sync  link  :: (Char,Char) -> Join ()
   async edge  :: (Char,Char) -> Join ()

Chord o@make(a) where o = root(a)                 -- create a new singleton set

Chord o@union(a,b) where                          -- union the sets of a and b
   o = do { (x,y) <- find(a) .||. find(b)         -- execute both 'goals' in parallel
          ; link(x,y) }

Chord edge(a,b) / x@find(a) where x = find(b)     -- move up a step closer to root

Chord root(a) / x@find(a) where x = return a      -- root has been found

Chord x@link(a,a) where x = return ()             -- already in the same set, hence do nothing

Chord root(a) / x@link(a,b) & root(b) where x = edge(b,a) -- link two roots

Latest News

Downloads

Current Works in Progress and Future Works

Developer's Corner

Maintained by Edmund S. L. Lam, Email: lamsoonl@comp.nus.edu.sg

TaichiWiki: HaskellJoinRules (last edited 2007-11-27 02:02:47 by EdmundLam)