[Haskell-cafe] Principal type in Haskell
Hi All, I am confused by the notion of principal type in Haskell with type classes. Consider a simple example: f x y = [x] == [y] GHCi yields type f :: (Eq [a]) = a - a - Bool. But according to the paper Type classes: an exploration of the design space, predicate Eq [a] should be reduced to Eq a. Is this reduction performed here? What should be the principal type of f? Thanks. william _ Get an advanced look at the new version of MSN Messenger. http://messenger.msn.com.sg/Beta/Default.aspx ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Principal type in Haskell
Thanks. Do I therefore able to conclude that none of the reductions using instance declarations are not performed because of potential overlapping instances? william From: Bulat Ziganshin [EMAIL PROTECTED] Reply-To: Bulat Ziganshin [EMAIL PROTECTED] To: william kim [EMAIL PROTECTED] CC: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] Principal type in Haskell Date: Thu, 22 Jun 2006 14:28:14 +0400 Hello william, Thursday, June 22, 2006, 1:22:32 PM, you wrote: GHCi yields type f :: (Eq [a]) = a - a - Bool. But according to the paper Type classes: an exploration of the design space, predicate Eq [a] should be reduced to Eq a. Is this reduction performed here? What should be the principal type of f? Ghc, unlike H98, supports instances like this: instance Eq [MyType] where a==b = True so this extension to type inference allows to use such instance even if MyType is not in Eq class -- Best regards, Bulatmailto:[EMAIL PROTECTED] _ Find love on MSN Personals http://personals.msn.com.sg/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: coherence when overlapping?
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: [EMAIL PROTECTED] Reply-To: [EMAIL PROTECTED] To: [EMAIL PROTECTED], haskell-cafe@haskell.org Subject: Re: coherence when overlapping? Date: 13 Apr 2006 03:46:38 - 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
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
[Haskell-cafe] coherence when overlapping?
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] coherence when overlapping?
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 [EMAIL PROTECTED]
To: william kim [EMAIL PROTECTED],haskell-cafe@haskell.org
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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
