Superclass inference (was: termination for FDs and ATs)
| Superclass implication is reversed when performing type inference. | In the same way that instance reduction is reserved. | | Here's the example again. | | class C a | class F a where |type T a | instance F [a] where |type T [a] = [[[a]]] | class C (T a) = D a | ^ | type function appears in superclass context | instance D [a] = C [[a]] -- satisfies Ross Paterson's Termination Conditions | | Consider | | D [a] | --_superclassC (T [a]), D [a] | --_type function C [[[a]]], D [a] | --_instance D [[a]], D [a] | and so on | | Of course, you'll argue that you apply some other inference methods. Probably! Let me explain what GHC does today, and see if that helps. GHC tries to solve the following problem: Input: a set of given constraints G a set of wanted constraints W Output: evidence that Y can be deduced from G+instance decls During solving, GHC maintain two sets: the given set GG and the wanted set WW. XX is maintained closed under superclasses; that is, when adding a constraint (C t) to GG, I add all of C's superclasses. GG is initialised from G, closing under superclasses. WW is initialised to W, but is *not* closed under superclasses. Then we repeatedly pick a member of WW a) if it's in GG, we are done b) otherwise use an instance decl to simplify it, putting the new constraints back in WW c) if neither applies, error. In the pure inference case, the algorithm is slightly different: Input: a set of wanted constraints W Output: a minimal set of wanted constraints, G plus evidence for how to deduce W from G GG starts empty. The algorithm is the same as before, but in case (c) we add the constraint to GG (plus its superclasses). At the end, extract G from GG; we want all the things that were not the superclass-closure extras. -- The point of explaining this is to say that in your example, (D [a]) is part of Y, so GHC won't add D [a]'s superclasses in the first place, and the problem you describe doesn't arise. I don't know whether that is luck, good judgement, or perhaps wrong. --- In the presence of ATs, I think that when adding a member to XX, or to YY, we need to normalise the types wrt AT rewrites (a confluent terminating process) first. But that should do it. (Of course, I have proved nothing.) Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: termination for FDs and ATs
On Fri, May 05, 2006 at 08:42:12AM +0100, Simon Peyton-Jones wrote: Alas, g simply discards its argument, so there are no further constraints on 'a'. I think Martin would argue that type inference should succeed with a=Bool, since there is exactly one solution. Is this an example of what you mean? Actually a = Maybe Bool However, as a programmer I would not be in the least upset if inference failed, and I was required to add a type signature. I don't expect type inference algorithms to guess, or to solve recursive equations, and that's what is happening here. I think Martin is assuming the current Haskell algorithm: infer the type of the function and then check that it's subsumed by the declared type, while you're assuming a bidirectional algorithm. That makes a big difference in this case, but you still do subsumption elsewhere, so Martin's requirement for normal forms will still be present. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: termination for FDs and ATs
Ross Paterson writes: On Fri, May 05, 2006 at 08:42:12AM +0100, Simon Peyton-Jones wrote: Alas, g simply discards its argument, so there are no further constraints on 'a'. I think Martin would argue that type inference should succeed with a=Bool, since there is exactly one solution. Is this an example of what you mean? Actually a = Maybe Bool However, as a programmer I would not be in the least upset if inference failed, and I was required to add a type signature. I don't expect type inference algorithms to guess, or to solve recursive equations, and that's what is happening here. I think Martin is assuming the current Haskell algorithm: infer the type of the function and then check that it's subsumed by the declared type, while you're assuming a bidirectional algorithm. That makes a big difference in this case, but you still do subsumption elsewhere, so Martin's requirement for normal forms will still be present. A quick reply: Subsumption among two type schemes boilds down to testing whether (roughly) Annotation_Constraint implies Infered_Constraint given demanded iff Annotation_Constraint - Annotation_Constraint /\ Infered_Constraint So, of course the latter is more suitable for testing than the former. (effectively, we push 'given' type information down the abstract syntax tree). In any case, it's entirly unclear to me whether 'stopping' the AT inference process at some stage will guarantee complete inference (in the presence of type annotations etc). Martin ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org//mailman/listinfo/haskell-prime
