Oleg, Simon,

Thanks for your help. If i understand it correctly, the code below gives a reasonably clean first cut at a demonstration of process calculi as polymorphically parametric in the type of name, allowing for an instantiation of the type in which the quoted processes play the role of name. This is much, much cleaner and easier to read than the OCaml version.

Best wishes,

--greg

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

module Core(
            Nominal
           ,Name
           ,Locality
           ,Location
           ,CoreProcessSyntax
           ,CoreAgentSyntax
           ,MinimalProcessSyntax
           ,MinimalAgentSyntax
           ,ReflectiveProcessSyntax
--           ,make_process
           )
    where

-- What's in a name?

class Nominal n where
   nominate :: i -> n i

-- newtype Name i = Nominate i deriving (Eq, Show)
newtype Name i = Name i deriving (Eq, Show)

instance Nominal Name where nominate i = Name i

-- Where are we?

class Locality a where
   locate :: (Eq s, Nominal n) => s -> (n i) -> a s (n i)
   name :: (Eq s, Nominal n) => a s (n i) -> (n i)

-- data Location s n = Locate s n deriving (Eq, Show)
data Location s n = Location s n deriving (Eq, Show)

instance Locality Location where
locate s n = Location s n
name (Location s n) = n

-- Constraints

class CoreProcessSyntax p a x | p -> a x where
   zero :: p
   sequence :: a -> x -> p
   compose :: [p] -> p

class CoreAgentSyntax x p n | x -> p n where
   bind :: [n] -> p -> x
   offer :: [n] -> p -> x

-- Freedom (as in freely generated)

data MinimalProcessSyntax l x =
    Null
    | Sequence l x
    | Composition [MinimalProcessSyntax l x]

data MinimalAgentSyntax n p =
    Thunk (() -> p)
    | Abstraction ([n] -> p)
    | Concretion [n] p

-- Responsibility : constraining freedom to enjoy order

instance CoreProcessSyntax (MinimalProcessSyntax l x) l x where
    zero = Null
    sequence l a = Sequence l a
    compose [] = zero
    compose ps = Composition ps

instance CoreAgentSyntax (MinimalAgentSyntax n p) p n where
    bind [] proc = Thunk (\() -> proc)
--      -- TODO : lgm : need to substitute m for name in proc
    bind (name:names) proc = Abstraction (\m -> comp $ bind names proc)
        where comp (Thunk fp) = fp ()
              -- comp (Abstraction abs) = abs name
    offer names proc = Concretion names proc

data ReflectiveProcessSyntax =
    Reflect
    (MinimalProcessSyntax
     (Location [(Name ReflectiveProcessSyntax)] (Name ReflectiveProcessSyntax))
     (MinimalAgentSyntax (Name ReflectiveProcessSyntax) ReflectiveProcessSyntax))

-- instance (CoreProcessSyntax p a x) =>
--     CoreProcessSyntax
--     (MinimalProcessSyntax
--      (Location
--       [(Name (MinimalProcessSyntax a x))]
--       (Name (MinimalProcessSyntax a x)))
--      (MinimalAgentSyntax
--       (Name (MinimalProcessSyntax a x))
--       (MinimalProcessSyntax a x)))
--     (Location
--       [(Name (MinimalProcessSyntax a x))]
--       (Name (MinimalProcessSyntax a x)))
--     (MinimalAgentSyntax
--       (Name (MinimalProcessSyntax a x))
--       (MinimalProcessSyntax a x))

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103

+1 206.650.3740

http://biosimilarity.blogspot.com