...

there is no implication that d=Bool (you could add: 'instance B a b => C [a] b Char' without violating FD consistency).

These instances (alpha-renamed): instance B a1 b1 => C [a1] b1 Bool instance B a2 b2 => C [a2] b2 Char

violate the consistency condition: a substitution that unifies a1 and a2 need not unify b1 and b2, because the consistency condition makes no mention of the contexts. (If it did, the instance improvement rule would be invalid.)

?? the consistency condition does mention b1 and b2 as t_b and s_b, so any substitution that unifies a1 and a2 (t_a and s_a) needs to unify b1 and b2, independent of context. note also that we are talking about different things here: I am talking about FD consistency, you are talking about the FD consistency condition. let's be concrete: class B a b | a -> b class C a b c | a -> b instance B a1 b1 => C [a1] b1 Bool instance B a2 b2 => C [a2] b2 Char with these declarations, you are concerned about constraints C [a] b Bool,C [a] c Char, which you claim are substitution instances of these declaration heads even if b and c differ. but the class instances of class C are constrained by an FD, and if b and c differ, these two constraints are _not_ substitution instances under that FD. they would be substitution instances if that FD wasn't there (*). the FD consistency condition is an approximation of FD consistency, and it is a strange approximation at that, because it is neither sufficient nor necessary (with the alternative CHR translation) for consistency: - if all instance declarations fulfill the FD consistency condition, the constraint store may still be inconsistent, because it may represent an inconsistent query; so the condition is not sufficient - one of the bonuses of a confluent CHR is that deductions on inconsistent stores will not terminate successfully (if they terminate, they are certain to fail), so the condition is not necessary, either [it was with the old translation, though] as this example shows once again, there are instance declarations for which the FD consistency condition, as currently interpreted by Hugs, fails, even though no inconsistent constraints are implied. so I fail to see the point of continuing to require the FD consistency condition in unrevised form. but my point was that there is no confluence problem. everything else, with the exception of termination, follows from there. cheers, claus (*) this is similar to patterns and guards in the expression language, for instance: f a = .. -- some function c [a1] b1 Bool | b1 == f [a1] = b a1 b1 c [a2] b2 Char | b2 == f [a2] = b a2 b2 now, c [a] b1 Bool and c [a] b2 Char are defined if (b1==f [a]) and (b2==f [a]) and if b a b1 and b a b2 are defined as well. c [a] d Bool with (d/=f[a]) matches the pattern, but fails the guard, so it is not a substitution instance of c's left hand sides under the guard.

Do you have a revised set of restrictions on the form of instances?

sure, but you won't like them any better now than the last time I mentioned them:-) - as for confluence, none of the restrictions seem necessary without FDs, type class inference proceeds by _matching_ of instance heads to constraints, and without overlapping instances, there cannot be more than one matching head. so the only divergence comes from reductions on separate parts of the constraint store, which are independent, so the divergence is temporary. with FDs, type class inference adds _unification_, but only for FD range parameters. instance heads that only differ in FD range positions are now overlapping, but only as far as improvement is concerned. note also that the resulting overlap in the left hand side of rules is over variables, so no variable instantiation can disable such rules. to be initially diverging, such overlapping improvement rules must have different unifications as their right hand sides. memoisation ensures that any improvement that was possible at any point in the reduction process remains possible throughout. so following either of two conflicting improvements will leave the other enabled, ensuring failure of the constraint store instead of non-determistic results. consistency condition: neither necessary nor sufficient coverage/bound variable condition: as far as confluence is concerned, these were possibly motivated by the wish to have variable-restricted CHR, without which arbitrary rule systems might introduce non-confluence by following different instantiations for the fresh variables, through unification with different left hand sides. but due to the peculiarities of Haskell's type classes, such instantiations do not appear to be a problem, as sketched above. (as far as termination is concerned, I remain unconvinced that these two rules are the right way to exclude problematic cases, as they exclude many valid programs just because these might be invoked with problematic queries. in such cases, I'd prefer to exclude the problematic queries.) early checking for superclass instances: also does not seem to be needed any more; as the superclass constraints will be introduced as proof obligations in the same step that introduces infer_Class and memo_Class constraints, they cannot be "forgotten", and inference cannot terminate successfully if those instances are missing (they may, however, be provided later than now, accepting more valid programs). (sigh, I'm sure I've written this before, as so many other things here.. I may well be wrong in what I'm saying - if that is the case, please tell me so, but _please_ don't keep asking me to repeat myself..) - as for termination, the checks not related to the conditions above are a useful start, but they are incomplete, and overly restrictive. in fact, we know that we are dealing with an undecidable problem here, so that no finite system of restrictions will be able to do the job statically. we've already discussed various improvements to the current set of checks here, as have others here and elsewhere. my preference here is unchanged: the variant without static termination checks needs to be the basis, and it needs to be defined clearly, so that all implementations of Haskell' accept the same programs and give the same results. the reason for this preference is my opinion that Haskell has become too complex a language already. heaping special cases on top of restrictions that are necessarily incomplete adds complexity to the language, while restricting its expressiveness. on top of that basis, we should have termination conditions, and we should keep trying to push the envelope by making them encompass more valid programs, but that also means that these termination conditions need to keep evolving! so we should have warnings if the current set of termination checks cannot statically determine whether or not some type class program will terminate, and by all means, have a flag to decide whether or not those warnings should become error messages (for teaching contexts, or for any other software development processes based on strict coding standard conformance, the former might be the right default option). but in the near future, I do not expect to see either of the following two: a set of termination conditions that will cover and permit all practically relevant programs, or a correct and terminating, practically motivated type class program that will run much longer than it takes me to read and understand the warnings produced by the current set of termination checks. oh, two more things: if type class inference fails to terminate, I never get to run my program, so that is perfectly type safe; and if, as will eventually happen, part of my terminating type class programs are beyond the abilities of the current set of termination checks, I do not want to have to resort to a module- or project-wide license to get my code through. I'm no expert in this, but I believe that those folks who are concerned with termination proofs accept it as a matter of routine that tailoring a termination-ordering for each particular problem is an important part of their business; but if Haskell' does not support this, and still insists on doing mandatory termination checks by default, it should at least allow me to indicate which of the type classes/instances I want to take responsibility for (via a pragma, most likely), using its checks on all others. cheers, claus

On Mon, Apr 10, 2006 at 02:39:18PM +0100, Claus Reinke wrote:

...

class B a b | a -> b class C a b c | a -> b

instance B a b => C [a] b Bool

Starting from a constraint set C [a] b Bool, C [a] c d, [...]

CHR-alt:

B a b <=> infer_B a b, memo_B a b. memo_B a b1, memo_B a b2 ==>b1=b2.

C a b c <=> infer_C a b c, memo_C a b c. memo_C a b1 c1, memo_C a b2 c2 ==> b1=b2. infer_C [a] b Bool <=> B a b. memo_C [a] b' c' ==> b'=b.

OK, so you want to modify the usual instance reduction rule by recording functional dependencies from the head. That is, you get confluence by remembering all the choices you had along the way, so you can still take them later. My problem with this scheme is that it makes FDs an essential part of the semantics, rather than just a shortcut, as they are in the original system. With the old system, one can understand instances using a Herbrand model, determined by the instance declarations alone. If the instances respect FDs, types can be made more specific using improvement rules justified by that semantics. With your system, there's only the operational semantics. To understand types, programmers must operate the rewriting system. And the constraint store they must work with will be quite cluttered with all these memoized FDs.

thanks, Tom! indeed, for that old thread on an alternative translation, which forked from an even older thread, I put aside all my wishlist and simply focussed on removing what I considered anomalies in the operationalisation of type classes with FDs via CHR in the old translation. the CHR resulting from the alternative translation should not allow any new constraints to be proven, it should only make sure that any FD-based information is fully used in any results, completing any incomplete deductions in the old system. I found it highly irregular that whether or not an FD was respected by the CHR system resulting from the original translation could depend on reduction strategies - the only way for real implementations to work around this shortcoming would be to iterate improvement before continuing reduction, which puts additional constraints on the implementer in an already complex system; and the only way for a formal system based on this incomplete translation to be safe was to try and cover all the possible holes with a set of restrictions that backfire by complicating the language design and making the whole idea of FDs look more tricky than it needs to be. there are interesting problems in FDs, but it seems that the confluence problems were merely problems of the old translation, not anything inherent in FDs! I really had hoped we had put that phantom to rest. (btw, in a real implementation, I wouldn't expect the memo constraints to enter the constraint store at all - they are just a CHR-based way to express a memo table, hence the name; as, in fact, I explained before even starting that alternative translation thread..). cheers, claus

...

OK, so you want to modify the usual instance reduction rule by recording functional dependencies from the head. That is, you get confluence by remembering all the choices you had along the way, so you can still take them later.

My problem with this scheme is that it makes FDs an essential part of the semantics, rather than just a shortcut, as they are in the original system. With the old system, one can understand instances using a Herbrand model, determined by the instance declarations alone. If the instances respect FDs, types can be made more specific using improvement rules justified by that semantics. With your system, there's only the operational semantics.

The logical semantics of the original CHR program and that of Claus with the memoization is really the same, I'm sure. The justifiable improvemetns are exactly the same. The main difference is that the memoization makes the rules confluent in more cases, i.e. the difference is in the operational semantics. For that matter the operational semantics of the confluent program would be considered to capture more completely the logical semantics and justifiable improvements.

...

To understand types, programmers must operate the rewriting system.

Not at all. The confluent program is really more intuitive, because more of the logically justifiable improvements are done.

...

And the constraint store they must work with will be quite cluttered with all these memoized FDs.

This is more of an implementation issue than a conceptual one, isn't it? I can think of a number of optimizations already to reduce the overhead.

On Thu, 13 Apr 2006, Claus Reinke wrote:

(btw, in a real implementation, I wouldn't expect the memo constraints to enter the constraint store at all - they are just a CHR-based way to express a memo table, hence the name; as, in fact, I explained before even starting that alternative translation thread..).

Sure, you can have any particular dedicated data structure to realize part of the constraint store. CHR implementations already use lists, trees, hashtables, global variables, ... If some Haskell' implementations want a dedicated CHR implementation for their type inference, there is already quite some expertise in efficient implementation and optimized compilation of CHR and I would be interested as a CHR implementor. Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be

that's why Ross chose a fresh variable in FD range position: in the old translation, the class-based FD improvement rule no longer applies after reduction because there's only one C constraint left, and the instance-based FD improvement rule will only instantiate the 'b' or 'c' in the constraint with a fresh 'b_123', 'b_124', .., unrelated to 'b', 'c', or any previously generated variables in the constraint store. hth, claus another way to interpret your message: to show equivalence of the two constraint sets, you need to show that one implies the other, or that both are equivalent to a common constraint set - you cannot use constraints from one set to help discharging constraints in the other.

class B a b | a -> b class C a b c | a -> b

instance B a b => C [a] b Bool

Starting from a constraint set C [a] b Bool, C [a] c d, we have two possible reductions:

1) C [a] b Bool, C [a] c d => c = b, C [a] b Bool, C [a] b d (use FD on C) => c = b, B a b, C [a] b d (reduce instance)

2) C [a] b Bool, C [a] c d => B a b, C [a] c d (reduce instance)

(changed C to B to fix a typo) It seems to me that the constraint sets {B a b, C [a] b d} and {B a b, C [a] c d} are equivalent in the sense that if we assume the first set we can discharge the constraints in the second, and vice versa. So why are we saying that we have lost confluence? Is there perhaps a different example that illustrates the porblem? -Iavor PS: To show that C [a] b d |- C [a] c d we can apply the improving substitution 'b=c' (using the FD on class C), and then solve the goal by assumption, the proof the other way is symmetric. _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime

On Thu, Apr 13, 2006 at 12:07:53PM -0700, Iavor Diatchki wrote:

On 4/12/06, Claus Reinke wrote:

...

that's why Ross chose a fresh variable in FD range position: in the old translation, the class-based FD improvement rule no longer applies after reduction because there's only one C constraint left, and the instance-based FD improvement rule will only instantiate the 'b' or 'c' in the constraint with a fresh 'b_123', 'b_124', .., unrelated to 'b', 'c', or any previously generated variables in the constraint store.

I understand the reduction steps. Are you saying that the problem is that the two sets are not syntactically equal? To me this does not seem important: we just end up with two different ways to say the same thing (i.e., they are logically equivalent).

If c were mentioned in another constraint, they would not be equivalent.

On Thu, Apr 13, 2006 at 05:10:36PM -0700, Iavor Diatchki wrote:

...

...

I understand the reduction steps. Are you saying that the problem is that the two sets are not syntactically equal? To me this does not seem important: we just end up with two different ways to say the same thing (i.e., they are logically equivalent).

If c were mentioned in another constraint, they would not be equivalent.

How so? A concrete example would really be useful. I think that the constraint 'C [a] b d' and 'C [a] c d' are equivalent and I don't see how the rest of the context can affect this (of course I have been wrong in the past :-).

They are equivalent, but C [a] b d, Num c and C [a] c d, Num c are not.