[Haskell-cafe] Re: coherence when overlapping?

[Martin Sulzmann]

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: oleg at pobox.com
 > >Reply-To: oleg at pobox.com
 > >To: haskelllist at hotmail.com, haskell-cafe at 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 at haskell.org
 > http://www.haskell.org/mailman/listinfo/haskell-cafe