[Haskell-cafe] Re: coherence when overlapping?
sulzmann at comp.nus.edu.sg
Thu Apr 13 03:33:01 EDT 2006
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.
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
> 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.
> >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
> > > 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
More information about the Haskell-Cafe