relaxed instance rules spec (was: the MPTC Dilemma (please solve))

[Simon Peyton-Jones]

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:claus.reinke at talk21.com]
| Sent: 28 February 2006 19:54
| To: Simon Peyton-Jones; haskell-prime at 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