Re: [Haskell-cafe] A Finally Tagless Pi Calculus

10 Jun 2010

      On Thu, Jun 10, 2010 at 3:52 AM, Arnaud Bailly 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
...
...
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
On Wed, Jun 9, 2010 at 6:20 PM, Edward Kmett  wrote:
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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe