At 02:18 07/06/03 +0200, Dylan Thurston wrote:
On Wed, Jun 04, 2003 at 01:21:00PM +0100, Graham Klyne wrote:
There is a recurring difficulty I'm having using multiparameter classes. =20 Most recently, I have a class Rule: [[ class (Expression ex, Eq (rl ex)) =3D> Rule rl ex where ... ]] =20 Which I wish to instantiate for a type GraphClosure via something like: [[ instance (Label lb, LDGraph lg lb) =3D> Expression (lg lb) where ... =20 data (Label lb, LDGraph lg lb) =3D> GraphClosure lg lb =3D ... =20 instance Rule GraphClosure (NSGraph RDFLabel) where ... =20 ]] ... I think that what I really *want* to do here is change the kind of=20 GraphClosure to be (* -> *) rather than (* -> * -> *). But if I try this: =20 [[ data (Label lb, LDGraph lg lb) =3D> GraphClosure (lg lb) =3D ... ]] a syntax error is reported by Hugs and GHC.
You haven't quite shown enough of your code. One thing you might consider is dropping the context from the definition of the GraphClosure type. Class contexts in data declarations end up being largely useless, anyway, since the dictionary is never actually used for anything. (There was a thread a few years ago about this.) You could then write
data GraphClosure lglb =3D ...
But this only works if the definition of GraphClosure only uses (lg lb), not the individual pieces.
I'm still wrestling with the exact form of the code, and it's part of a much larger program in development. I reproduce more of the code below, but I suspect you may be right in that I'm including unnecessary context in the data declaration(s). After writing my original message, I also spotted something in the implementation of Control.Monad.State, in which: [[ class (Monad m) => MonadState s m | m -> s where get :: m s put :: s -> m () ]] has 's' being declared as determined by m, without explicitly saying how. I haven't yet really learned about functional dependencies... [ ... wanders off to read paper [1] on functional dependencies ... ] ... they do seem to shed some light on the issue, if only to indicate that I've been mis-reading the multiparameter class construct. For some reason, I've been reading it so that, say, (C a b) means that (a b) is an instance of C, where it seems that I should be reading is to mean (a,b) are in some relation C. And, if I've got it right, each instantiation of C potentially extends the relation (a,b) defined by C. A supplementary musing: suppose I have: class X a b c d | (a,b) -> (c,d) then among all the instances of D, the combination D a b _ _ must appear at most once for any given a and b? I think this is beginning to make more sense, but I've yet to go figure how it affects my code. (Maybe this will make the magic seem less black for me?) #g -- [1] http://www.cse.ogi.edu/~mpj/pubs/fundeps-esop2000.pdf Below is an larger excerpt from the (unfinished) code I'm working on. Based on your comments, I think I can lose the context (and the 'lg' references) from 'GraphClosure'. Maybe there are similar changes I can make to the definition of LDGraph (which I already know should be reviewed). The following two classes are intended to provide some base components of a generic inference-verification (proof) framework: [[ -- |Expression is a type class for values over which proofs -- may be constructed. class (Eq ex) => Expression ex where -- |Is expression true in all interpretations? -- If so, then its truth is assumed without justification. isValid :: ex -> Bool -- |Rule is a type class for inference rules that can be used -- to construct a step in a proof. class (Expression ex, Eq (rl ex)) => Rule rl ex where -- |Name of rule, for use when displaying a proof ruleName :: rl ex -> String -- |Forward application of a rule, takes a list of -- expressions and returns a list (possibly empty) -- of forward applications of the rule to combinations -- of the antecedent expressions. fwdApply :: rl ex -> [ex] -> [ex] -- |Backward application of a rule, takes an expression -- and returns a list of antecedent expressions that -- jointly yield the given expression through application -- of the inference rule. bwdApply :: rl ex -> ex -> [ex] ]] And here are my attempts to instantiate these classes for a generic class of directed labelled graphs (LDGraph) over some node-label type lb: [[ -- |Instances of LDGraph are also instance of the -- Expression class, for which proofs can be constructed. -- The empty RDF graph is always True (other enduring -- truths are asserted as axioms). instance (Label lb, LDGraph lg lb) => Expression (lg lb) where isValid gr = null $ getArcs gr -- |Datatype for graph closure rule data (Eq lg, Label lb) => GraphClosure lb lg = GraphClosure { nameGraphRule :: String -- ^ Name of rule for proof display , ruleAnt :: [Arc lb] -- ^ Antecedent triples pattern -- (may include variable nodes) , ruleCon :: [Arc lb] -- ^ Consequent triples pattern -- (may include variable nodes) } ]] and finally declaring a specific type and rule instance in which a particular label type is used: [[ type RDFClosure = GraphClosure RDFGraph -- |Define RDFClosure as instance type of proof -- inference rule class. instance Rule (GraphClosure RDFLabel) RDFGraph where ruleName rl = nameGraphRule rl fwdApply rl ags = let ag = foldl1 merge ags vars = queryFind (ruleAnt rl) ag in querySubs vars (ruleCon rl) bwdApply rl cg = let vars = queryFind (ruleCon rl) cg in map (querySubs vars) (ruleAnt rl) ]] ------------------- Graham Klyne <GK@NineByNine.org> PGP: 0FAA 69FF C083 000B A2E9 A131 01B9 1C7A DBCA CB5E