[Haskell-cafe] RE: On reflection

25 Apr 2007

      Not only that, but when we have associated type synonyms going it'll be even clearer.  Instead of

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

you'll be able to write

class CoreProcessSyntax p where
   type AThing p :: *
   type XThing p :: *
   zero :: p
   sequence :: AThing p -> XThing p -> p
   compose :: [p] -> p

I'm not sure what the 'a' and 'x' parameters stand for, but they are functionally dependent on 'p'; I've called these type functions AThing and XThing, but you'll have more meaningful names.  Now the type of 'sequence' is much rmore perspicuous.

Simon

________________________________
From: lgreg.meredith@gmail.com [mailto:lgreg.meredith@gmail.com] On Behalf Of Greg Meredith
Sent: 25 April 2007 04:27
To: oleg@pobox.com; Simon Peyton-Jones
Cc: haskell-cafe; Matthias Radestock; Matthew Sackman; Tristan Allwood
Subject: On reflection

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