Oleg, Simon, <br><br>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.
<br><br>Best wishes,<br><br>--greg<br><br>{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}<br><br>module Core(<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Nominal<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,Name<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,Locality<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,Location<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,CoreProcessSyntax
<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,CoreAgentSyntax<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,MinimalProcessSyntax<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,MinimalAgentSyntax<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,ReflectiveProcessSyntax<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; ,make_process<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; )<br>&nbsp;&nbsp;&nbsp; where<br><br>-- What&#39;s in a name?
<br><br>class Nominal n where<br>&nbsp;&nbsp; nominate :: i -&gt; n i<br><br>-- newtype Name i = Nominate i deriving (Eq, Show)<br>newtype Name i = Name i deriving (Eq, Show)<br><br>instance Nominal Name where nominate i = Name i<br>
<br>-- Where are we?<br><br>class Locality a where<br>&nbsp;&nbsp; locate :: (Eq s, Nominal n) =&gt; s -&gt; (n i) -&gt; a s (n i)<br>&nbsp;&nbsp; name :: (Eq s, Nominal n) =&gt; a s (n i) -&gt; (n i)<br><br>-- data Location s n = Locate s n deriving (Eq, Show)
<br>data Location s n = Location s n deriving (Eq, Show)<br><br>instance Locality Location where<br>&nbsp; locate s n = Location s n<br>&nbsp; name (Location s n) = n<br><br><br>-- Constraints<br><br>class CoreProcessSyntax p a x | p -&gt; a x where
<br>&nbsp;&nbsp; zero :: p<br>&nbsp;&nbsp; sequence :: a -&gt; x -&gt; p<br>&nbsp;&nbsp; compose :: [p] -&gt; p<br><br>class CoreAgentSyntax x p n | x -&gt; p n where<br>&nbsp;&nbsp; bind&nbsp; :: [n] -&gt; p -&gt; x<br>&nbsp;&nbsp; offer :: [n] -&gt; p -&gt; x<br><br>-- Freedom (as in freely generated)
<br><br>data MinimalProcessSyntax l x =<br>&nbsp;&nbsp;&nbsp; Null<br>&nbsp;&nbsp;&nbsp; | Sequence l x<br>&nbsp;&nbsp;&nbsp; | Composition [MinimalProcessSyntax l x]<br><br>data MinimalAgentSyntax n p =<br>&nbsp;&nbsp;&nbsp; Thunk (() -&gt; p)<br>&nbsp;&nbsp;&nbsp; | Abstraction ([n] -&gt; p)<br>
&nbsp;&nbsp;&nbsp; | Concretion [n] p<br><br>-- Responsibility : constraining freedom to enjoy order<br><br>instance CoreProcessSyntax (MinimalProcessSyntax l x) l x where<br>&nbsp;&nbsp;&nbsp; zero = Null<br>&nbsp;&nbsp;&nbsp; sequence l a = Sequence l a<br>&nbsp;&nbsp;&nbsp; compose [] = zero
<br>&nbsp;&nbsp;&nbsp; compose ps = Composition ps<br><br>instance CoreAgentSyntax (MinimalAgentSyntax n p) p n where<br>&nbsp;&nbsp;&nbsp; bind [] proc = Thunk (\() -&gt; proc)<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; -- TODO : lgm : need to substitute m for name in proc<br>&nbsp;&nbsp;&nbsp; bind (name:names) proc = Abstraction (\m -&gt; comp $ bind names proc)
<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; where comp (Thunk fp) = fp ()<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; -- comp (Abstraction abs) = abs name<br>&nbsp;&nbsp;&nbsp; offer names proc = Concretion names proc<br><br>data ReflectiveProcessSyntax =<br>&nbsp;&nbsp;&nbsp; Reflect <br>&nbsp;&nbsp;&nbsp; (MinimalProcessSyntax
<br>&nbsp;&nbsp;&nbsp;&nbsp; (Location [(Name ReflectiveProcessSyntax)] (Name ReflectiveProcessSyntax)) <br>&nbsp;&nbsp;&nbsp;&nbsp; (MinimalAgentSyntax (Name ReflectiveProcessSyntax) ReflectiveProcessSyntax))<br><br>-- instance (CoreProcessSyntax p a x) =&gt;<br>
--&nbsp;&nbsp;&nbsp;&nbsp; CoreProcessSyntax<br>--&nbsp;&nbsp;&nbsp;&nbsp; (MinimalProcessSyntax<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Location<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; [(Name (MinimalProcessSyntax a x))]<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Name (MinimalProcessSyntax a x)))<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (MinimalAgentSyntax<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Name (MinimalProcessSyntax a x))
<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (MinimalProcessSyntax a x)))<br>--&nbsp;&nbsp;&nbsp;&nbsp; (Location<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; [(Name (MinimalProcessSyntax a x))]<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Name (MinimalProcessSyntax a x)))<br>--&nbsp;&nbsp;&nbsp;&nbsp; (MinimalAgentSyntax<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (Name (MinimalProcessSyntax a x))
<br>--&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; (MinimalProcessSyntax a x))<br clear="all"><br>-- <br>L.G. Meredith<br>Managing Partner<br>Biosimilarity LLC<br>505 N 72nd St<br>Seattle, WA 98103<br><br>+1 206.650.3740<br><br><a href="http://biosimilarity.blogspot.com">
http://biosimilarity.blogspot.com</a>