On Wed, Jun 9, 2010 at 6:20 PM, Edward Kmett <
ekmett@gmail.com> wrote:
> 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)
>