relaxed instance rules spec (was: the MPTC Dilemma (please
solve))
Simon PeytonJones
simonpj at microsoft.com
Wed Mar 1 03:32:14 EST 2006
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
apparentlyconservative rules is entirely nontrivial. It's one of
those areas in which it is easy to suggest a plausiblesounding
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 PeytonJones; haskellprime 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/typeextension
s.html#instancedecls

 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 callgraph reachability: there
 are fewer predicates reachable from TypeNotEq than from
 Test  in particular, Test is not reachable from TypeNotEq).

 this is a nonlocal 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 bestfit 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
More information about the Haskellprime
mailing list