[Haskell-cafe] A Finally Tagless Pi Calculus

[Edward Kmett]

On Thu, Jun 10, 2010 at 3:52 AM, Arnaud Bailly <arnaud.oqube at gmail.com>wrote:

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

You need the Nu type because you need channels that can only send channels
of channels of channels of channels of ...

You could equivalently use the formulation

newtype NuChan = NuChan (Chan NuChan)

but then I couldn't recycle the wrapper for other types if I wanted.

Without it the code below it would be untype because of the "occurs check".

If you look in category-extras under Control.Morphism.* you'll find a lot of
other uses of the types Mu/Nu though there the type is called FixF.

-Edward Kmett


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