Keegan McAllister gave a very nice talk at Boston Haskell last night about "First Class Concurrency". His slides are available online at <br><br><a href="http://t0rch.org/" target="_blank">http://t0rch.org/</a><br>
<br>His final few slides covered the Pi calculus:<br><br><a href="http://en.wikipedia.org/wiki/Pi_calculus">http://en.wikipedia.org/wiki/Pi_calculus</a><br><br>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. <br>
<br>For more information on finally tagless encodings, see: <br><br><a href="http://www.cs.rutgers.edu/%7Eccshan/tagless/jfp.pdf" target="_blank">http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf</a><br><br>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. ;)<br>
<br>-Edward Kmett<br>
<br>> {-# LANGUAGE Rank2Types, TypeFamilies, FlexibleInstances #-}<br>> module Pi where<br><br>> import Control.Applicative<br>> import Control.Concurrent<br><br>A finally tagless encoding of the Pi calculus. Symantics is a portmanteau of Syntax and Semantics.<br>
<br>> class Symantics p where<br>> type Name p :: *<br>> new :: (Name p -> p) -> p<br>> out :: Name p -> Name p -> p -> p <br>> (|||) :: p -> p -> p <br>> inn :: Name p -> (Name p -> p) -> p <br>
> rep :: p -> p <br>> nil :: p<br>> embed :: IO () -> p<br><br>Type level fixed points<br><br>> newtype Nu f = Nu { nu :: f (Nu f) }
<br><br>> fork :: IO () -> IO () <br>> fork a = forkIO a
>> return ()<br><br>> forever :: IO a -> IO a<br>>
forever p = p >> forever p<br><br>
Executable semantics<br>
<br>> instance Symantics (IO ()) where<br>> type Name (IO ()) =
Nu Chan<br>> new f = Nu <$> newChan >>= f<br>>
a ||| b = forkIO a >> fork b<br>> inn (Nu x) f = readChan x
>>= fork . f<br>> out (Nu x) y b = writeChan x y >> b<br>>
rep = forever <br>> nil = return ()<br>> embed = id<br><br>A closed pi calculus term<br><br>> newtype Pi = Pi { runPi :: forall
a. Symantics a => a }<br><br>>
run :: Pi -> IO ()<br>> run (Pi a) = a<br><br>> example = Pi
(new $ \z -> (new $ \x -> out x z nil <br>>
||| (inn x $ \y -> out y x $ inn x $ \ y -> nil))<br>>
||| inn z (\v -> out v v nil))<br>
<br>A pretty printer for the pi calculus<br><br>> newtype Pretty = Pretty { runPretty :: [String] -> Int -> ShowS } <br>> <br>> instance Symantics Pretty where<br>> type Name Pretty = String<br>> new f = Pretty $ \(v:vs) n -> <br>
> showParen (n > 10) $ <br>> showString "nu " . showString v . showString ". " . <br>> runPretty (f v) vs 10<br>> out x y b = Pretty $ \vs n -> <br>
> showParen (n > 10) $ <br>> showString x . showChar '<' . showString y . showString ">. " . <br>> runPretty b vs 10 <br>> inn x f = Pretty $ \(v:vs) n -><br>
> showParen (n > 10) $<br>> showString x . showChar '(' . showString v . showString "). " .<br>> runPretty (f v) vs 10 <br>> p ||| q = Pretty $ \vs n -> <br>
> showParen (n > 4) $<br>> runPretty p vs 5 . <br>> showString " | " .<br>> runPretty q vs 4<br>> rep p = Pretty $ \vs n -> <br>> showParen (n > 10) $<br>
> showString "!" .<br>> runPretty p vs 10<br>> nil = Pretty $ \_ _ -> showChar '0'<br>> embed io = Pretty $ \_ _ -> showString "{IO}"<br><br>> instance Show Pi where<br>
> showsPrec n (Pi p) = runPretty p
vars n<br>> where<br>> vars = fmap return vs
++ <br>> [i : show j | j <- [1..], i <- vs]
where <br>> vs = ['a'..'z']<br><br>Pi> example<br>nu a. (nu b. (b<a>. 0 | b(c). c<b>. b(d). 0) | a(b). b<b>. 0)<br>