[Haskell-cafe] A Finally Tagless Pi Calculus

[Arnaud Bailly]

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.
>
> 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)
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>