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.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)