Multiparameter class confusion (and functional dependencies)

[Graham Klyne]

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