# [Haskell-cafe] A Finally Tagless Pi Calculus

Edward Kmett ekmett at gmail.com
Wed Jun 9 12:20:04 EDT 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.

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

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