[Haskell-cafe] A Finally Tagless Pi Calculus

9 Jun 2010

      Keegan McAllister gave a very nice talk at Boston Haskell last night about
"First Class Concurrency". His slides are available online at

http://t0rch.org/

His final few slides covered the Pi calculus:

http://en.wikipedia.org/wiki/Pi_calculus

I took a few minutes over lunch to dash out a finally tagless version of the
pi calculus interpreter presented by Keegan, since the topic of how much
nicer it would look in HOAS came up during the meeting.

For more information on finally tagless encodings, see:

http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdfhttp://www.cs.rutgers.edu/%7Eccshan/tagless/jfp.pdf

Of course, Keegan went farther and defined an encoding of the lambda
calculus into the pi calculus, but I leave that as an exercise for the
reader. ;)

-Edward Kmett
...
{-# LANGUAGE Rank2Types, TypeFamilies, FlexibleInstances #-}
module Pi where
...
import Control.Applicative
import Control.Concurrent
A finally tagless encoding of the Pi calculus. Symantics is a portmanteau of
Syntax and Semantics.
...
class Symantics p where
    type Name p :: *
    new :: (Name p -> p) -> p
    out :: Name p -> Name p -> p -> p
    (|||) :: p -> p -> p
    inn :: Name p -> (Name p -> p) -> p
    rep :: p -> p
    nil :: p
    embed :: IO () -> p
Type level fixed points
...
newtype Nu f = Nu { nu :: f (Nu f) }
...
fork :: IO () -> IO ()
fork a = forkIO a >> return ()
...
forever :: IO a -> IO a
forever p = p >> forever p
Executable semantics
...
instance Symantics (IO ()) where
    type Name (IO ()) = Nu Chan
    new f = Nu <$> newChan >>= f
    a ||| b = forkIO a >> fork b
    inn (Nu x) f = readChan x >>= fork . f
    out (Nu x) y b = writeChan x y >> b
    rep = forever
    nil = return ()
    embed = id
A closed pi calculus term
...
newtype Pi = Pi { runPi :: forall a. Symantics a => a }
...
run :: Pi -> IO ()
run (Pi a) = a
...
example = Pi (new $ \z -> (new $ \x -> out x z nil
                                   ||| (inn x $ \y -> out y x $ inn x $ \
y -> nil))
                  ||| inn z (\v -> out v v nil))
A pretty printer for the pi calculus
...
newtype Pretty = Pretty { runPretty :: [String] -> Int -> ShowS }
instance Symantics Pretty where
    type Name Pretty = String
    new f = Pretty $ \(v:vs) n ->
        showParen (n > 10) $
            showString "nu " . showString v . showString ". " .
            runPretty (f v) vs 10
    out x y b = Pretty $ \vs n ->
        showParen (n > 10) $
            showString x . showChar '<' . showString y . showString ">. "
.
            runPretty b vs 10
    inn x f = Pretty $ \(v:vs) n ->
        showParen (n > 10) $
            showString x . showChar '(' . showString v . showString "). "
.
            runPretty (f v) vs 10
    p ||| q = Pretty $ \vs n ->
        showParen (n > 4) $
            runPretty p vs 5 .
            showString " | " .
            runPretty q vs 4
    rep p = Pretty $ \vs n ->
        showParen (n > 10) $
            showString "!" .
            runPretty p vs 10
    nil = Pretty $ \_ _ -> showChar '0'
    embed io = Pretty $ \_ _ -> showString "{IO}"
...
instance Show Pi where
    showsPrec n (Pi p) = runPretty p vars n
        where
            vars = fmap return vs ++
                   [i : show j | j <- [1..], i <- vs] where
            vs = ['a'..'z']
Pi> example
nu a. (nu b. (b<a>. 0 | b(c). c<b>. b(d). 0) | a(b). b<b>. 0)