On Wednesday 09 June 2010 2:32:29 pm Dupont Corentin wrote:

I am making a little GATD:

...

{-# LANGUAGE GADTs#-}

data Obs a where

Equal :: Obs a -> Obs a -> Obs Bool Plus :: (Num a) => Obs a -> Obs a -> Obs a

(etc..)

...

instance Show t => Show (Obs t) where

show (Equal a b) = (show a) ++ " Equal " ++ (show b) show (Plus a b) = (show a) ++ " Plus " ++ (show b)

instance Eq t => Eq (Obs t) where

a `Equal` b == c `Equal` d = (a == c) && (b == d) a `Plus` b == c `Plus` d = (a == c) && (b == d)

Your two symptoms have the same underlying cause. The 'a' in Equal is existentially quantified. It might help to think about bundling the type in the Equal constructor: Equal T x y :: Obs Bool where T :: * x :: Obs T y :: Obs T Now we write: show (Equal T x y) = ... but we have no evidence that (Show T), so we cannot conclude (Show (Obs T)), and thus cannot use show on x and y. Similarly: Equal T x y == Equal T' x y = ... Your definition assumes that T = T' (or, it assumes that Obs T = Obs T', but that reduces to T = T'), but we have no reason to suspect that is the case. Hence the mismatch. The first can be solved by putting a Show constraint on the type of the Equal constructor, if that's what you really want. The second can probably only be solved by having Equal take some kind of type rep, and checking that the types are equal. Hope that helps. -- Dan

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