[Redirecting to Haskell Cafe]

Hi Greg

I think it’s very likely that you *can* do what you want.   I have not taken long enough to understand just what you are trying to do, but I do know why your program is failing, and I think you’ll agree it *should* fail.  Look at these lines (slightly simplified)

class CoreAgentSyntax x where

    offer :: (CoreProcessSyntax p) => [n] -> (p a x) -> x

data MinimalAgentSyntax nn pp = Concretion [nn] pp

instance CoreAgentSyntax (MinimalAgentSyntax nn pp) where

     offer = Concretion

The class decl says that every instance of ‘offer’ must have type

                forall p, forall n, forall a. (CoreProcessSyntax p) => [n] -> p a x -> x

where x is the instance type.  Not the “forall n”!   Even once x is fixed, we must have a function that is polymorphic in n,p,a

But in your instance declaration, offer = Concretion has the type

                [nn] -> pp -> MinimalAgentSyntax nn pp

No for-alls, because the whole instance decl binds the ‘nn’.  Hence it’s just not polymorphic enough.

I’m not sure how to fix your problem.  Perhaps you need another argument for CoreAgentSyntax?        

class CoreAgentSyntax n x where

    offer :: (CoreProcessSyntax p) => [n] -> (p a x) -> x

instance CoreAgentSyntax nn (MinimalAgentSyntax nn pp) where

     offer = Concretion

now you are in better shape. There’s another problem because you use ‘p’ with kind * in some places and (*->*->*) in others, but thats a separate issue. 

Oleg is good at this kind of stuff.

Simon

From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Greg Meredith
Sent: 18 April 2007 14:53
To: haskell@haskell.org
Subject: [Haskell] haskell question

Haskellians,

In the attached file i have implemented the bare bones core of the syntax -- pre structural equivalence -- of Milner's presentation of \pi via abstractions and concretions. (There's a minor twist in that the notion of location affords more structure than in Milner's original presentation which i have added to support an ultimate probabilistic interpretation.)

The file compiles with ghc as is. If you uncomment the last section, however, you see that to close the loop on the constraints for the agent syntax we hit a typing error. i think this is a hard constraint in Haskell that prevents this level of generality in the specification, but maybe you can see a way around it. i'm certainly no Haskell expert.

Best wishes,

--greg

P.S. The reason for this level of generality is that with it you can close the loop and form a mutual recursion between the types for the syntax of processes and the type of names -- without having that choice predesigned into the structure of processes (or names). i can do this trick in OCaml with recursive modules, but it's definitely not pretty. i was hoping Haskell could make it pretty.

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

+1 206.650.3740

http://biosimilarity.blogspot.com