# [Haskell-cafe] A Finally Tagless Pi Calculus

Arnaud Bailly arnaud.oqube at gmail.com
Thu Jun 10 03:52:03 EDT 2010

```Hello,
I studied (a bit) Pi-calculus and other mobile agents calculus during
my PhD, and I have always been fascinated by the beauty of this idea.
Your implementation is strikingly simple and beautiful.

I have a question though: Why is the fixpoint type

> newtype Nu f = Nu { nu :: f (Nu f) }

needed? And BTW, why generally use fixpoint on types? I read some
papers using/presenting such constructions (most notable a paper by
R.Lammel, I think, on expression trees transformation) but never quite
get it.

Thanks
Arnaud

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