Coherence (roughly) means that the program's semantics is independent of the program's typing.
In case of your example below, I could type the program either use the first or the second instance (assuming g has type Int->Int). That's clearly bound. Guard constraints enforce that instances are non-overlapping. instance C Int instance C a | a =!= Int The second instance can only fire if a is different from Int. Non-overlapping instances are necessary but not sufficient to obtain coherence. We also need that types/programs are unambiguous. Martin william kim writes: > Thank you oleg. > > Sulzmann et al use guards in CHR to turn overlapping heads (instances) into > non-overlapping. Their coherence theorem still assumes non-overlapping. > > I agree that what you described is the desirable behaviour when overlapping, > that is to defer the decision when multiple instances match. However, why > this is coined as coherence? What is the definition of coherence in this > case? > > class C a where > f::a -> a > instance C Int where > f x = x+1 > instance C a where > f x = x > > g x = f x > > In a program like this, how does a coherence theorem rules out the > "incoherent" behaviour of early committing the f to the second instance? > > I am very confused. Please help. > > --william > > >From: [EMAIL PROTECTED] > >Reply-To: [EMAIL PROTECTED] > >To: [EMAIL PROTECTED], haskell-cafe@haskell.org > >Subject: Re: coherence when overlapping? > >Date: 13 Apr 2006 03:46:38 -0000 > > > > > But I am still confused by the exact definition of coherence in the case > >of > > > overlapping. Does the standard coherence theorem apply? If yes, how? > > > If no, is there a theorem? > > > >Yes, the is, by Martin Sulzmann et al, the Theory of overloading (the > >journal version) > > http://www.comp.nus.edu.sg/~sulzmann/ms_bib.html#overloading-journal > > > >A simple intuition is this: instance selection may produce more than > >one candidate instance. Having inferred a polymorphic type with > >constraints, the compiler checks to see of some of the constraints can > >be reduced. If an instance selection produces no candidate instances, > >the typechecking failure is reported. If there is exactly one > >candidate instance, it is selected and the constraint is removed > >because it is resolved. An instance selection may produce more then > >one candidate instance. Those candidate instances may be incomparable: > >for example, given the constraint "C a" and instances "C Int" and "C > >Bool", both instances are candidates. If such is the case, the > >resolution of that constraint is deferred and it `floats out', to be > >incorporated into the type of the parent expression, etc. In the > >presence of overlapping instances, the multiple candidate instances > >may be comparable, e.g. "C a" and "C Int". The compiler then checks > >to see if the target type is at least as specific as the most specific > >of those candidate instances. If so, the constraint is reduced; > >otherwise, it is deferred. Eventually enough type information is > >available to reduce all constraints (or else it is a type error). > > _________________________________________________________________ > Find just what you are after with the more precise, more powerful new MSN > Search. http://search.msn.com.sg/ Try it now. > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe