Re: coherence when overlapping?
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).
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@pobox.com Reply-To: oleg@pobox.com To: haskelllist@hotmail.com, 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.
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@pobox.com Reply-To: oleg@pobox.com To: haskelllist@hotmail.com, 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
Thank you Martin.
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.
If g has type Int->Int, it is not hard to say the first instance should apply. But how about g having a polymorphic type? In this case it seems to me choosing the second instance is an acceptable choice as that is the only applicable one at the moment. What is the definition of a "coherent" behaviour here? Or is there one?
Non-overlapping instances are necessary but not sufficient to obtain coherence. We also need that types/programs are unambiguous.
Do you therefore imply that coherence is not defined without the non-overlapping assumption? --william _________________________________________________________________ Get MSN Hotmail alerts on your mobile. http://mobile.msn.com/ac.aspx?cid=uuhp_hotmail
Coherence may also arise because of an ambiguous type. Here's the classic example. class Read a where read :: String -> a class Show a where show :: a -> String f s = show (read s) f has type String->String, therefore we can pick some arbitrary Read/Show classes. If you want to know more about coherence/ambiguity in the Haskell context. Check out @TechReport{jones:coherence, author = "M. P. Jones", title = "Coherence for qualified types", institution = "Yale University, Department of Computer Science", year = 1993, month = "September", type = "Research Report", number = "YALEU/DCS/RR-989" } and @Article{overloading-journal, author = {P.~J.~Stuckey and M.~Sulzmann }, title = {A Theory of Overloading}, journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, publisher = "ACM Press", year = "2005", pages = "1-54", volume = 27, number = 6, preprint = {http://www.comp.nus.edu.sg/~sulzmann/chr/download/theory-journal.ps.gz}} As far as I know, the term "coherence" was coined by @article{breazu-tannen-etal:inhertiance-coercion, author = "V. Breazu{-}Tannen and T. Coquand and C. Gunter and A. Scedrov", title = "Inheritance as Implicit Coercion", journal = "Information and Computation", volume = 93, number = 1, month = jul, year = 1991, pages = "172--221" } Martin william kim writes:
Thank you Martin.
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.
If g has type Int->Int, it is not hard to say the first instance should apply. But how about g having a polymorphic type? In this case it seems to me choosing the second instance is an acceptable choice as that is the only applicable one at the moment. What is the definition of a "coherent" behaviour here? Or is there one?
Non-overlapping instances are necessary but not sufficient to obtain coherence. We also need that types/programs are unambiguous.
Do you therefore imply that coherence is not defined without the non-overlapping assumption?
--william
_________________________________________________________________ Get MSN Hotmail alerts on your mobile. http://mobile.msn.com/ac.aspx?cid=uuhp_hotmail
participants (3)
-
Martin Sulzmann -
oleg＠pobox.com -
william kim