[Haskell-cafe] Re: coherence when overlapping?

[william kim]

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.