[Haskell-cafe] On reflection

24 Apr 2007

      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] On reflection

Greg Meredith