Re: Proposal to solve Haskell's MPTC dilemma

newer
Improving Haskell on Windows by...

older
How to fix this problem in FreeBSD...

Isaac Dupree

27 May 2010 27 May '10

3 a.m.

On 05/26/10 15:42, Carlos Camarao wrote:

...

What do you think?

I think you are proposing using the current set of instances in scope in order to remove ambiguity. Am I right? ..I read the haskell-cafe thread so far, and it looks like I'm right. This is what I'll add to what's been said so far: Your proposal appears to allow /incoherent/ instance selection. This means that an expression can be well-typed in one module, and well-typed in another module, but have different semantics in the two modules. For example (drawing from above discussion) : module C where class F a b where f :: a -> b class O a where o :: a module P where import C instance F Bool Bool where f = not instance O Bool where o = True k :: Bool k = f o module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k :: Bool k = f o module Main where import P import Q -- (here, all four instances are in scope) main = do { print P.k ; print Q.k } -- should result, according to your proposal, in -- False -- True -- , am I correct? Also, in your paper, example 2 includes

...

m = (m1 * m2) * m3 and you state In Example 2, there is no means of specializing type variable c0 occurring in the type of m to Matrix.

I suggest that there is an appropriate such means, namely, to write m = (m1 * m2 :: Matrix) * m3 . (Could the paper address how that solution falls short? Are there other cases in which there is more than just a little syntactical convenience at stake?, or is even that much added code too much for some use-case?) -Isaac

Show replies by date

Carlos Camarao

27 May 27 May

2:39 p.m.

New subject: Proposal to solve Haskell's MPTC dilemma

On 05/26/10 15:42, Carlos Camarao wrote:

...

I think you are proposing using the current set of instances in scope in order to remove ambiguity. Am I right?

I think that an important point is that it is not exactly "to remove ambiguity", because the proposal tries to solve the problem exactly when there is really no ambiguity. There would be ambiguity if there were two or more conflicting definitions, and the proposal is to use, upon occurrence of an unreachable type variable in a constraint, an instance in the current context that is the single instance that could be used to instantiate that type variable. This was perhaps made unclear when I incorrectly wrote in haskell-cafe that the proposal eliminates the need for defaulting. I should have said that defaulting is not necessary to force instantiation (of unreachable variables) when there are no conflicting definitions in the current context. That is, defaulting should be used exactly to remove ambiguity, i.e. when there exist conflicting definitions and when unreachable type variables appear that can be instantiated to such conflicting definitions.

...

Your proposal appears to allow /incoherent/ instance selection. This means that an expression can be well-typed in one module, and well-typed in another module, but have different semantics in the two modules. For example (drawing from above discussion) :

module C where

class F a b where f :: a -> b class O a where o :: a

module P where import C

instance F Bool Bool where f = not instance O Bool where o = True k :: Bool k = f o

module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k :: Bool k = f o

module Main where import P import Q -- (here, all four instances are in scope) main = do { print P.k ; print Q.k } -- should result, according to your proposal, in -- False -- True -- , am I correct?

If qualified importation of k from both P and from Q was specified, we would have two *distinct* terms, P.k and Q.k. Unqualified importation must cause an error (two distinct definitions for the same non-overloaded name). For overloaded names with distinct instances, *ambiguity* would be reported, as e.g. in: module C where class O a where o::a module P where instance O Bool where o = True module Q where instance O Bool where o = False moduke Main where import P import Q main = do { print o::Bool }

...

Also, in your paper, example 2 includes m = (m1 * m2) * m3 and you state

...
In Example 2, there is no means of specializing type variable c0 occurring in the type of m to Matrix. In Example 2, there is no means of specializing type variable c0 occurring in the type of m to Matrix. I suggest that there is an appropriate such means, namely, to write m = (m1 * m2 :: Matrix) * m3

Yes, that solution is fine. Sorry, I should have written "There is no means of specializing type variable c0 occurring in the type of m to Matrix, without an explicit type annotation in the expression defining m."

...

(Could the paper address how that solution falls short? Are there other cases in which there is more than just a little syntactical convenience at stake? , or is even that much added code too much for some use-case?)

The point should have been that you cannot make a class with FDs eliminate the need for having to make explicit type annotations, in cases such as these. The example should also be such that it would need more type annotations, instead of just one... Cheers, Carlos

David Menendez

8:43 p.m.

New subject: Proposal to solve Haskell's MPTC dilemma

On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao wrote:

...

Isaac Dupree:

...
Your proposal appears to allow /incoherent/ instance selection. This means that an expression can be well-typed in one module, and well-typed in another module, but have different semantics in the two modules. For example (drawing from above discussion) :

module C where

class F a b where f :: a -> b class O a where o :: a

module P where import C

instance F Bool Bool where f = not instance O Bool where o = True k :: Bool k = f o

module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k :: Bool k = f o

module Main where import P import Q -- (here, all four instances are in scope) main = do { print P.k ; print Q.k } -- should result, according to your proposal, in -- False -- True -- , am I correct?

If qualified importation of k from both P and from Q was specified, we would have two *distinct* terms, P.k and Q.k.

I think Isaac's point is that P.k and Q.k have the same definition (f o). If they don't produce the same value, then referential transparency is lost. -- Dave Menendez http://www.eyrie.org/~zednenem/

Carlos Camarao

9:42 p.m.

New subject: Proposal to solve Haskell's MPTC dilemma

On Thu, May 27, 2010 at 5:43 PM, David Menendez wrote:

...

On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao wrote:

...
Isaac Dupree:

...
Your proposal appears to allow /incoherent/ instance selection. This means that an expression can be well-typed in one module, and well-typed in another module, but have different semantics in the two modules. For example (drawing from above discussion) :

module C where

class F a b where f :: a -> b class O a where o :: a

module P where import C

instance F Bool Bool where f = not instance O Bool where o = True k :: Bool k = f o

module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k :: Bool k = f o

module Main where import P import Q -- (here, all four instances are in scope) main = do { print P.k ; print Q.k } -- should result, according to your proposal, in -- False -- True -- , am I correct?

If qualified importation of k from both P and from Q was specified, we would have two *distinct* terms, P.k and Q.k.

I think Isaac's point is that P.k and Q.k have the same definition (f o). If they don't produce the same value, then referential transparency is lost.

-- Dave Menendez <http://www.eyrie.org/~zednenem/ http://www.eyrie.org/%7Ezednenem/>

The definitions of P.k and Q.k are textually the same but the contexts are different. "f" and "o" denote distinct values in P and Q. Thus, P.k and Q.k don't have the same definition. Thanks for the clarification. I thought the point was about coherence. Cheers, Carlos

Isaac Dupree

28 May 28 May

5:36 a.m.

New subject: Proposal to solve Haskell's MPTC dilemma

On 05/27/10 17:42, Carlos Camarao wrote:

...

On Thu, May 27, 2010 at 5:43 PM, David Menendez wrote:

...
On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao wrote:

...
Isaac Dupree:

...
Your proposal appears to allow /incoherent/ instance selection. This means that an expression can be well-typed in one module, and well-typed in another module, but have different semantics in the two modules. For example (drawing from above discussion) :

module C where

class F a b where f :: a -> b class O a where o :: a

module P where import C

instance F Bool Bool where f = not instance O Bool where o = True k :: Bool k = f o

module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k :: Bool k = f o

module Main where import P import Q -- (here, all four instances are in scope) main = do { print P.k ; print Q.k } -- should result, according to your proposal, in -- False -- True -- , am I correct?

If qualified importation of k from both P and from Q was specified, we would have two *distinct* terms, P.k and Q.k.

I think Isaac's point is that P.k and Q.k have the same definition (f o). If they don't produce the same value, then referential transparency is lost.

-- Dave Menendez <http://www.eyrie.org/~zednenem/http://www.eyrie.org/%7Ezednenem/>

The definitions of P.k and Q.k are textually the same but the contexts are different. "f" and "o" denote distinct values in P and Q. Thus, P.k and Q.k don't have the same definition.

Oh, I guess you are correct: it is like defaulting: it is a similar effect where the same expression means different things in two different modules as if you had default (Int) in one, and default (Bool) in the other. Except: Defaulting according to the standard only works in combination with the 8 (or however many it is) standard classes; and defaulting in Haskell is already a bit poorly designed / frowned upon / annoying that it's specified per-module when nothing else in the language is*.(that's a rather surmountable argument) It may be worth reading the GHC user's guide which attempts to explain the difference between incoherent and non-incoherent instance selection, http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/type-class-extension... I didn't read both it and your paper closely enough that I'm sure anymore whether GHC devs would think your extension would require or imply -XIncoherentInstances ... my intuition was that IncoherentInstances would be implied... *(it's nice when you can substitute any use of a variable, such as P.k, with the expression that it is defined as -- i.e. the expression written so that it refer to the same identifiers, not a purely textual substitution -- but in main above, you can't write [assuming you imported C] "print (f o)" because it will be rejected for ambiguity. (Now, there is already an instance-related situation like this where Main imports two different modules that define instances that overlap in an incompatible way, such as two different instances for Functor (Either e) -- not everyone is happy about how GHC handles this, but at least those overlaps are totally useless and could perhaps legitimately result in a compile error if they're even imported into the same module.))

Carlos Camarao

30 May 30 May

1:24 a.m.

New subject: Proposal to solve Haskell's MPTC dilemma

On Fri, May 28, 2010 at 2:36 AM, Isaac Dupree < ml@isaac.cedarswampstudios.org> wrote:

...

On 05/27/10 17:42, Carlos Camarao wrote:

...
On Thu, May 27, 2010 at 5:43 PM, David Menendez wrote:

On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao

...
wrote:

...
Isaac Dupree:

...
Your proposal appears to allow /incoherent/ instance selection. This means that an expression can be well-typed in one module, and well-typed in another module, but have different semantics in the two modules. For example (drawing from above discussion) :

module C where

class F a b where f :: a -> b class O a where o :: a

module P where import C

instance F Bool Bool where f = not instance O Bool where o = True k :: Bool k = f o

module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k :: Bool k = f o

module Main where import P import Q -- (here, all four instances are in scope) main = do { print P.k ; print Q.k } -- should result, according to your proposal, in -- False -- True -- , am I correct?

If qualified importation of k from both P and from Q was specified, we would have two *distinct* terms, P.k and Q.k.

I think Isaac's point is that P.k and Q.k have the same definition (f o). If they don't produce the same value, then referential transparency is lost.

-- Dave Menendez <http://www.eyrie.org/~zednenem/ http://www.eyrie.org/%7Ezednenem/< http://www.eyrie.org/%7Ezednenem/>>

The definitions of P.k and Q.k are textually the same but the contexts are different. "f" and "o" denote distinct values in P and Q. Thus, P.k and Q.k don't have the same definition.

Oh, I guess you are correct: it is like defaulting: it is a similar effect where the same expression means different things in two different modules as if you had default (Int) in one, and default (Bool) in the other. Except: Defaulting according to the standard only works in combination with the 8 (or however many it is) standard classes; and defaulting in Haskell is already a bit poorly designed / frowned upon / annoying that it's specified per-module when nothing else in the language is*.(that's a rather surmountable argument)

...

It may be worth reading the GHC user's guide which attempts to explain the difference between incoherent and non-incoherent instance selection,

http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/type-class-extension... I didn't read both it and your paper closely enough that I'm sure anymore whether GHC devs would think your extension would require or imply -XIncoherentInstances ... my intuition was that IncoherentInstances would be implied...

*(it's nice when you can substitute any use of a variable, such as P.k, with the expression that it is defined as -- i.e. the expression written so that it refer to the same identifiers, not a purely textual substitution -- but in main above, you can't write [assuming you imported C] "print (f o)" because it will be rejected for ambiguity. (Now, there is already an instance-related situation like this where Main imports two different modules that define instances that overlap in an incompatible way, such as two different instances for Functor (Either e) -- not everyone is happy about how GHC handles this, but at least those overlaps are totally useless and could perhaps legitimately result in a compile error if they're even imported into the same module.)) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

I have no idea why you think IncoherentInstances would be implied. The proposal says: do not issue ambiguity error if, using whatever means permitted and specified (OverlappingInstances, IncoherentInstances, whatever), you can select a single instance. The situation is as if we a FD: module C where class F a b | a->b where f :: a -> b class O a where o :: a module P where import C; instance F Bool Bool where f = not instance O Bool where o = True g:: Bool -> Bool g = f k::Bool k = g o module Q where import C instance F Int Bool where f = even instance O Int where o = 0 g::Int->Bool g = f k :: Bool k = g o module Main where import P import Q main = do { print P.k ; print Q.k } Cheers, Carlos

Isaac Dupree

2:25 a.m.

New subject: Proposal to solve Haskell's MPTC dilemma

On 05/29/10 21:24, Carlos Camarao wrote:

...

The situation is as if we a FD:

Well, that is indeed equivalent here in the second argument of class F, but I constructed the example to show an issue in the class's *first* argument. Notice you needed to add type-signatures, on the functions you named "g" -- in particular their first arguments -- to make the example work with only FDs?

...

module C where class F a b | a->b where f :: a -> b class O a where o :: a

module P where import C; instance F Bool Bool where f = not instance O Bool where o = True g:: Bool -> Bool g = f k::Bool k = g o

module Q where import C instance F Int Bool where f = even instance O Int where o = 0 g::Int->Bool g = f k :: Bool k = g o

you can inline these "k"-definitions into module Main and it will work (modulo importing C). module Main where import C import P import Q main = do { print (((f :: Bool -> Bool) o) :: Bool); print (((f :: Int -> Bool) o) :: Bool) } These are two different expressions that are being printed, because " :: Bool -> Bool" is different from " :: Int -> Bool". In my example of using your proposal, one cannot inline in the same way, if I understand correctly (the inlining would cause ambiguity errors -- unless of course the above distinct type-signatures are added). If your proposal was able to require those -- and only those -- bits of type signatures that were essential to resolve the above ambiguity; for example, the ( :: Int) below, module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k = f (o :: Int) , then I would be fine with your proposal (but then I suspect it would have to be equivalent to FDs -- or in other words, that it's not really practical to change your proposal to have that effect). I stand by my assertion that "the same expression means different things in two different modules" is undesirable, (and that I suspect but am unsure that this undesirability is named "incoherent instances"). I'm trying to work out whether it's possible to violate the invariants of a Map by using your extension (having it select a different instance in two different places, given the same type).. I think, no it is not possible for Ord or any single-parameter typeclass, though there might be some kind of issues with multi-parameter typeclasses, if the library relies on a FD-style relationship between two class type-parameters and then two someones each add an instance that together violate that implied FD-relationship (which is allowed under your scheme, unlike if there was an actual FD). Er, odd, I need to play with some actual FD code to think about this, but I'm too sleepy / busy packing for a trip. Did any of the above make sense to you? It's fine if some didn't, type systems are complicated... and please point out if something I said was outright wrong. -Isaac

Carlos Camarao

31 May 31 May

1:57 a.m.

New subject: Proposal to solve Haskell's MPTC dilemma

...

...
The situation is as if we [had] a FD: Well, that is indeed equivalent here in the second argument of class F, but I constructed the example to show an issue in the class's *first* argument.

The example should be equivalent in all respects (at least that was my motivation when I wrote it).

...

Notice you needed to add type-signatures, on the functions you named "g" -- in particular their first arguments -- to make the example work with only FDs?

I wrote g, with type signatures, just to avoid writing the type signatures (f:: Bool->Bool and f::Int->Bool) inside (f o). I wanted to use, textually, the same expression.

...

These are two different expressions that are being printed, because " :: Bool -> Bool" is different from " :: Int -> Bool". In my example of using your proposal, one cannot inline in the same way,

I wrote the example just to show that one can obtain the same effect with FDs: one not "inline", i.e. use "g o", in the same way.

...

If your proposal was able to require those -- and only those -- bits of type signatures that were essential to resolve the above ambiguity; for example, the ( :: Int) below, module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k = f (o :: Int) , then I would be fine with your proposal (but then I suspect it would have to be equivalent to FDs -- or in other words, that it's not really practical to change your proposal to have that effect). I stand by my assertion that "the same expression means different things in two different modules" is undesirable, (and that I suspect but am unsure that this undesirability is named "incoherent instances").

"k::Bool; k=f o" in Q has exactly the same effect as "k=f(o::Int)", under our proposal. "(f o)::Bool" in P and in Q are not "the same expression", they are distinct expressions, because they occur in distinct contexts which make "f" and "o" in (f o)::Bool denote distinct values, just as "(g o)::Bool" are distinct expressions in P and Q in the example with a FD (because "g" and "o" in (g o)::Bool denote distinct values in P and in Q). Cheers, Carlos

5516

Age (days ago)

5520

Last active (days ago)

List overview

Download

7 comments

3 participants

participants (3)

Carlos Camarao
David Menendez
Isaac Dupree

Re: Proposal to solve Haskell's MPTC dilemma

tags

participants (3)