Claus,
I urge you to read our paper Understanding functional dependencies via
Constraint Handling Rules, which you can find here
http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/.
It will tell you more than you want to know about why relaxing
apparently-conservative rules is entirely non-trivial. It's one of
those areas in which it is easy to suggest a plausible-sounding
alternative, but much harder to either prove or disprove whether the
alternative a sound one.
The paper describes rules we are reasonably sure of. It would be great
to relax those rules. But you do need to have a proof that the
relaxation preserves the properties we want. Go right ahead! The paper
provides a good framework for such work, I think.
Simon
| -Original Message-
| From: Claus Reinke [mailto:[EMAIL PROTECTED]
| Sent: 28 February 2006 19:54
| To: Simon Peyton-Jones; haskell-prime@haskell.org
| Subject: relaxed instance rules spec (was: the MPTC Dilemma (please
solve))
|
| The specification is here:
|
http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extension
s.html#instance-decls
|
| two questions/suggestions about this:
|
| 1. there are other termination criteria one migh think of, though
| many will be out because they are not easy to specify. but here
| is an annoyingly simple example that doesn't fit the current rules
| even though it is clearly terminating (it's not even recursive):
|
| class Fail all -- no instances!
|
| class TypeNotEq a b
| instance Fail a = TypeNotEq a a
| instance TypeNotEq a b
|
| class Test a b where test :: a - b - Bool
| instance TypeNotEq a b = Test a b where test _ _ = False
| instance Test a a where test _ _ = True
|
| main = print $ (test True 'c', test True False)
|
| never mind the overlap, the point here is that we redirect from
| Test a b to TypeNotEq a b, and ghc informs us that the
| Constraint is no smaller than the instance head.
|
| it is true that the parameters don't get smaller (same number,
| same number of constructors, etc.), but they are passed to a
| smaller predicate (in terms of call-graph reachability: there
| are fewer predicates reachable from TypeNotEq than from
| Test - in particular, Test is not reachable from TypeNotEq).
|
| this is a non-local criterion, but a fairly simple one. and it
seems
| very strange to invoke undecidable instances for this example
| (or is there anything undecidable about it?).
|
| 2. the coverage condition only refers to the instance head. this
| excludes programs such as good old record selection (which
| should terminate because it recurses over finite types, and is
| confluent -in fact deterministic- because of best-fit overlap
| resolution):
|
| -- | field selection
| infixl #?
|
| class Select label val rec | label rec - val where
| (#?) :: rec - label - val
|
| instance Select label val ((label,val),r) where
| ((_,val),_) #? label = val
|
| instance Select label val r = Select label val (l,r) where
| (_,r) #? label = r #? label
|
| now, it is true that in the second instance declaration, val is
| not covered in {label,(l,r)}. however, it is covered in the
recursive
| call, subject to the very same FD, if that recursive call complies
| with the (recursive) coverage criterion. in fact, for this
particular
| task, that is the only place where it could be covered.
|
| would it be terribly difficult to take such indirect coverage (via
| the instance constraints) into account? there'd be no search
| involved (the usual argument against looking at the constraints),
| and it seems strange to exclude such straightforward consume
| a type recursions, doesn't it?
|
| cheers,
| claus
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
