RE: [Haskell-cafe] Re: coherence when overlapping?
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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: coherence when overlapping?
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: [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Re: coherence when overlapping?
| 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Re: coherence when overlapping?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: coherence when overlapping?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
