[Haskell-cafe] A Finally Tagless Pi Calculus

[Edward Kmett]

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<http://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)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100609/fb8505e9/attachment.html