Hi All,
One important property of type class dictionary translation is coherence which basically says that two typing derivations for the same term at the same type in the same environment must be equivalent. This definition is established with the assumption of non-overlapping. In the GHC documentation which describes the extension of overlapping instances, an example similar to the following is given. >class C a where > f:a -> a >instance C Int where > f=e1 >instance C a where > f=e2 > >let g x = f x >in g 1 In this case GHC takes an ¡°incoherent¡± decision by taking the second instance as an instantiation of function f even it is executed with an input of type Int. My question is whether the ¡°incoherence¡± behaviour of overlapping instances is derived from the definition of coherence in the non-overlapping setting? If yes, how is it applicable to rule out the incoherent behaviour? If otherwise, what is the definition of coherence with overlapping instances? Thanks. --william _________________________________________________________________ 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
| In the GHC documentation which describes the extension of overlapping
| instances, an example similar to the following is given. | | >class C a where | > f:a -> a | >instance C Int where | > f=e1 | >instance C a where | > f=e2 | > | >let g x = f x | >in g 1 | | In this case GHC takes an ¡°incoherent¡± decision by taking the second | instance as an instantiation of function f even it is executed with an input | of type Int. No it doesn't (ghc 6.4.1). I've just tried it. It uses the C Int instance, for exactly the reason you describe. There is a flag -fallow-incoherent-instances that _does_ allow incoherence Simon {-# OPTIONS -fallow-overlapping-instances -fglasgow-exts -fallow-undecidable-instances #-} module Main where class C a where f::a -> a instance C Int where f x = x+1 instance C a where f x = x main = print (let g x = f x in g (1::Int)) _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Thank you Simon.
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? Is there any write-up on this? Thanks. --william >From: "Simon Peyton-Jones" <[hidden email]> >To: "william kim" <[hidden email]>,<[hidden email]> >Subject: RE: [Haskell-cafe] coherence when overlapping? >Date: Wed, 12 Apr 2006 17:43:33 +0100 > >| In the GHC documentation which describes the extension of overlapping >| instances, an example similar to the following is given. >| >| >class C a where >| > f:a -> a >| >instance C Int where >| > f=e1 >| >instance C a where >| > f=e2 >| > >| >let g x = f x >| >in g 1 >| >| In this case GHC takes an ¡°incoherent¡± decision by taking the second >| instance as an instantiation of function f even it is executed with an >input >| of type Int. > >No it doesn't (ghc 6.4.1). I've just tried it. It uses the C Int >instance, for exactly the reason you describe. > >There is a flag -fallow-incoherent-instances that _does_ allow incoherence > >Simon > > >{-# OPTIONS -fallow-overlapping-instances -fglasgow-exts >-fallow-undecidable-instances #-} > >module Main where > >class C a where > f::a -> a >instance C Int where > f x = x+1 >instance C a where > f x = x > >main = print (let g x = f x > in g (1::Int)) > _________________________________________________________________ Download MSN Messenger emoticons and display pictures. http://ilovemessenger.msn.com/?mkt=en-sg _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by william kim
> 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). _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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: [hidden email] >Reply-To: [hidden email] >To: [hidden email], [hidden email] >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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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: [hidden email] > >Reply-To: [hidden email] > >To: [hidden email], [hidden email] > >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 > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
I believe that GHC's overlapping instance extensions effectively uses inequalities. Why do you think that 'inequalities' model 'best-fit'? instance C Int -- (1) instance C a -- (2) under a 'best-fit' instance reduction strategy we would resolve C a by using (2). 'best-fit' should be very easy to implement. Simply order instances (resulting CHRs) in an appropriate 'best-fit' order. In case of instance C Int instance a =!=Int | C a (2') we can't reduce C a (because we can't satisfy a=!=Int) Notice that (2') translates to rule C a | a =!=Int <==> True I think it's better to write a =!=Int not as part of the instance context but write it as a guard constraint. I don't think there's any issue for an implementation (either using 'best-fit' or explicit inequalities). The hard part is to establish inference properties such as completeness etc. Martin Tom Schrijvers writes: > On Thu, 13 Apr 2006, Martin Sulzmann wrote: > > > > > 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. > > Claus Reinke was discussing this with me some time ago. He called it the > best fit principle, which would in a way, as you illustrate above, allow > inequality constraints to the instance head. You could even write it like: > > instance (a /= Int) => C a > > as you would do with the superclass constraints... I wonder whether > explicit inequality constraints would be useful on their own in all the > places where type class and equality constraints are used (class and > instance declarations, GADTs, ...). Or maybe it opens a whole new can of > worms :) > > Tom > > -- > Tom Schrijvers > > Department of Computer Science > K.U. Leuven > Celestijnenlaan 200A > B-3001 Heverlee > Belgium > > tel: +32 16 327544 > e-mail: [hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
| I believe that GHC's overlapping instance extensions
| effectively uses inequalities. I tried to write down GHC's rules in the manual: http://haskell.org/ghc/dist/current/docs/users_guide/type-extensions.htm l#instance-decls The short summary is: - find candidate instances that match - if there is exactly one, choose it - if the is more than one, choose the best fit UNLESS that choice would be changed if a type variable was instantiated Simon _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Martin Sulzmann
On Thu, 13 Apr 2006, Martin Sulzmann wrote:
> > I believe that GHC's overlapping instance extensions > effectively uses inequalities. > > Why do you think that 'inequalities' model 'best-fit'? > > instance C Int -- (1) > instance C a -- (2) > > under a 'best-fit' instance reduction strategy > we would resolve C a by using (2). Claus used the term best-fit, and what was meant is exactly the same as what you mean, i.e. a delayed until sufficiently instantiated best-fit rather than an immediate best fit. -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Martin Sulzmann
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by william kim
It seems that the subject is a bit more complex, and one can force GHC to choose the less specific instance (if one confuses GHC well enough): see the example below. First of all, the inequality constraint is already achievable in Haskell now: "TypeEq t1 t2 False" is such a constraint. One can write polymorphic functions that distinguish if the argument a list (any list of something) or not, etc. One can write stronger invariants like records where labels are guaranteed to be unique. There are two problems: first there are several notions of type inequality, all of which are useful in different circumstances. http://www.haskell.org/pipermail/haskell-prime/2006-March/000936.html Second, how inequality interacts with functional dependencies -- and in general, with the type improvement. And here, many interesting things emerge. For example, the following code > {-# OPTIONS -fglasgow-exts #-} > {-# OPTIONS -fallow-undecidable-instances #-} > {-# OPTIONS -fallow-overlapping-instances #-} > > module Foo1 where > > class C a b | a -> b where > f :: a -> b > > instance C Int Bool where > f x = True > > instance TypeCast Int b => C a b where > f x = typeCast (100::Int) > > class TypeCast a b | a -> b, b->a where typeCast :: a -> b > class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b > class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b > instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x > instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast'' > instance TypeCast'' () a a where typeCast'' _ x = x > > class D a b | a -> b where > g :: a -> b > > instance D Bool Bool where > g x = not x > > instance TypeCast a b => D a b where > g x = typeCast x > > test1 = f (42::Int) -- ==> True > test2 = f 'a' -- ==> 100 > > test3 = g (1::Int) -- ==> 1 > test4 = g True -- ==> False > > bar x = g (f x) `asTypeOf` x We see that test1 through test4 behave as expected. We can even define the function 'bar'. It's inferred type is *Foo1> :t bar bar :: (C a b, D b a) => a -> a The question becomes: is this a function? Can it be applied to anything at all? If we apply it to Int (thus instantiating the type a to Int), the type b is instantiated to Bool, and so (following the functional dependency for class D), the type a should be Bool (and it is already an Int). OTH, if we apply bar to anything but Int, then the type b should be Int, and so should the type a. Liar's paradox. And indeed, bar cannot be applied to anything because the constraints are contradictory. What is more interesting is the slight variation of that example: > class C a b | a -> b where > f :: a -> b > > instance C Int Int where > f x = 10+x > > instance TypeCast a b => C a b where > f x = typeCast x > > class D a b | a -> b where > g :: a -> b > > instance D Int Bool where > g x = True > > instance TypeCast Int b => D a b where > g x = typeCast (10::Int) > > test1 = f (42::Int) > test2 = f 'a' > > test3 = g (1::Int) > test4 = g True > > bar x = g (f x) `asTypeOf` x > > test5 = bar (1::Int) *Foo> :t bar bar :: (C a b, D b a) => a -> a If bar is applied to an Int, then the type b should be an Int, so the first instance of D ought to have been chosen, which gives the contradiction a = Bool. And yet it works (GHC 6.4.1). Test5 is accepted and even works *Foo> test5 10 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
> one can force GHC to choose the less specific instance (if one
> confuses GHC well enough): see the example below. your second example doesn't really do that, though it may look that way. >> class D a b | a -> b where g :: a -> b >> instance D Int Bool where g x = True >> instance TypeCast Int b => D a b where g x = typeCast (10::Int) .. >> bar x = g (f x) `asTypeOf` x >> test5 = bar (1::Int) > *Foo> :t bar > bar :: (C a b, D b a) => a -> a > > If bar is applied to an Int, then the type b should be an Int, so the > first instance of D ought to have been chosen, which gives the > contradiction a = Bool. And yet it works (GHC 6.4.1). Test5 is > accepted and even works > *Foo> test5 > 10 your argument seems to imply that you see FD range parameters as outputs of the instance inference process (*), so that the first Int parameter in the constraint D Int Int is sufficient to select the first instance (by ignoring the Int in the second parameter and using best-fit overlap resolution), leading to the contradiction Int=Bool. alas, current FD implementations don't work that way.. Hugs will complain about the overlap being inconsistent with the FD, for both C and D - does it just look at the instance heads? GHC will accept D even without overlapping instances enabled, but will complain about C, so it seems that it takes the type equality implied by FDs in instance contexts into account, seeing instances D Int Bool and D a Int - no overlaps. similarly, when it sees a constraint D Int Int, only the second instance head will match.. if you comment out the second C instance, and disable overlaps, the result of test5 will be the same. > First of all, the inequality constraint is already achievable in > Haskell now: "TypeEq t1 t2 False" is such a constraint. as you noted, that is only used as a constraint, for checks after instantiation, which is of little help as current Haskell has corners that ignore constraints (such as instance selection). specifically, there is a difference between the handling of type equality and type inequality: the former can be implied by FDs, which are used in instance selection, the latter can't and isn't (which is why I'd like to have inequality constraints that are treated the same way as FD-based equality constraints, even where constraints are otherwise ignored). if we want to formalise the interaction of FDs and overlap resolution, and we want to formalise the latter via inequality guards, then it seems that we need to put inequality constraints (negative type variable substitutions) on par with equality constraints (positive type variable substitutions). cheers, claus (*) or does it seem to me to be that way because that is how I'd like FD range parameters to be treated?-) _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Martin Sulzmann
On 2006-04-13, Martin Sulzmann <[hidden email]> wrote:
> > I believe that GHC's overlapping instance extensions > effectively uses inequalities. > > Why do you think that 'inequalities' model 'best-fit'? > > instance C Int -- (1) > instance C a -- (2) > > under a 'best-fit' instance reduction strategy > we would resolve C a by using (2). > > 'best-fit' should be very easy to implement. > Simply order instances (resulting CHRs) in an appropriate > 'best-fit' order. > > In case of > > instance C Int > instance a =!=Int | C a (2') > > we can't reduce C a (because we can't satisfy a=!=Int) > > Notice that (2') translates to > > rule C a | a =!=Int <==> True > > I think it's better to write a =!=Int not as part of the instance > context but write it as a guard constraint. > > I don't think there's any issue for an implementation (either using > 'best-fit' or explicit inequalities). The hard part is to establish > inference properties such as completeness etc. > This best-fit is essentially what people doing multi-method dispatch want. It turns out to not be as trivial as one would hope. -- Aaron Denney -><- _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by william kim
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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |