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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
