On Thu, Jun 10, 2010 at 3:52 AM, Arnaud Bailly <arnaud.oq...@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 <ekm...@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@haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> >
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
