On 20 May 2010 16:50, Carlos Camarao wrote:

...

Using the available instances to resolve overloading is a tricky thing, it's very easy to make things break that way.

Using the available instances is the natural, in fact the only way, to resolve overloading.

AFAIK no other Haskell feature is defined in terms of "available instance" information. Overloaded functions are resolved by at least these mechanisms: * Defaulting * Information from unification (including from user-defined type signatures) * Functional dependencies propagating information "Available instances" are not a natural addition to this list. In particular, using that information can cause programs to become untypeable when the module or *any module it imports transitively* defines a new instance. This leads to programs that are extremely fragile in the face of changes in the libraries! (Admittedly you can get the same issue with GHC Haskell as it is right now if you define an orphan instance in your module) The situation is even worse if you consider "available" instances to also include orphans defined in non-imported modules (as a whole-program compiler way very well do), because then you don't even need to have transitively imported the module which has added an instance for your program to stop type-checking. Furthermore, if you intend to use an "overloaded" function at *one particular instance*, you could just have written the monomorphic type to begin with and not even bothered with overload resolution.

Our proposal cannot make any well-typed program break, any program whatsoever.

That is true, but it makes extra things type check in a really fragile way. I'm not keen. Cheers, Max

I wonder: Of cases where overload resolution via available instances would be reasonable, how many would also make sense as a closed type class? By comparison, it seems that many uses of OverlappingInstances are really just trying to express a closed type class with one or more default instances, akin to functions with _ patterns. I think, though I'm not certain, that both would be straightforward and non-fragile for a closed type class.

Someone recently described the HASP project, at http://hasp.cs.pdx.edu/. It describes "habit", a haskell like language with some additions and subtractions. There are a couple interesting extensions to 'instance' declarations: -- explicitly declare that there is no instance, halting the compiler's search instance xyz fails -- declares instances along with search order instance abc ... else def The result is that if you put 'fails' at the end, you can make a closed typeclass. Presumably you could also make typeclasses open but only in a restricted way. Also presumably the compiler would then be able to make better decisions about overlapping instances and you could avoid a lot of overlapping problems. Of course, it's just a paper with no compiler, so it's all "presumably" for the moment...

Hi Evan, hasn't EHC had something like this for a while with 'type class directives'?

I dunno, I don't even know what ehc is. Is it this? http://www.cs.uu.nl/wiki/Ehc/WebHome I turned up a paper that mentioned type class directives, but I haven't read it yet. In any case, the EHC page says "nearing first release!" so "had something like this for a while" depends on your perspective of "has" :) In any case, I thought the habit paper was fun and had a number of things it would be nice to have in haskell (even simple sugar like case<- and if<-).

On Thu, May 20, 2010 at 1:25 PM, Max Bolingbroke

wrote:

On 20 May 2010 16:50, Carlos Camarao wrote:

...

...

Using the available instances to resolve overloading is a tricky thing, it's very easy to make things break that way.

Using the available instances is the natural, in fact the only way, to resolve overloading.

AFAIK no other Haskell feature is defined in terms of "available instance" information. Overloaded functions are resolved by at least these mechanisms: * Defaulting * Information from unification (including from user-defined type signatures) * Functional dependencies propagating information

"Available instances" are not a natural addition to this list. In particular, using that information can cause programs to become untypeable when the module or *any module it imports transitively* defines a new instance. This leads to programs that are extremely fragile in the face of changes in the libraries!

Replace "Using the available instances is the natural, in fact the only way, to resolve overloading." by "All overloading resolution has to consider the available instances, after unification, user-defined type signatures, defaulting and FDs have been considered." Extremely fragile is debatable; the important fact, highlighted, is that if overloading resolution depends on the existence of a unique substitution, then the program may become untypeable when other instances are defined in the visible typing context. (Admittedly you can get the same issue with GHC Haskell as it is right

now if you define an orphan instance in your module)

Yes. Just to emphasize, with our proposal the issue (of transforming a well-typed program into a program which is not well-typed) is relevant only when unreachable variables exist (for existing programs this never occurs, since they are unambiguous according to the existing ambiguity rule). The situation is even worse if you consider "available" instances to

also include orphans defined in non-imported modules (as a whole-program compiler way very well do), because then you don't even need to have transitively imported the module which has added an instance for your program to stop type-checking.

Consider instances defined in non-imported modules to be visible in the current context is not correct, I think...

Furthermore, if you intend to use an "overloaded" function at *one particular instance*, you could just have written the monomorphic type to begin with and not even bothered with overload resolution.

Sorry, I do not follow you here (why *at one particular instance*?). A polymorphic (overloaded or not) function is defined and then used at specific cases, with different (instance) types.

...

Our proposal cannot make any well-typed program break, any program whatsoever.

That is true, but it makes extra things type check in a really fragile way. I'm not keen.

Really fragile meaning: "Overloading resolution depends on the set of available instances in the following way: if a constraint on the type of an expression *contains unreachable variables* and these type variables can be instantiated, by a single substitution(*), to instances in the current context, then the constraint/overloading is resolved, and the type is not ambiguous)." then yes, ok. (*) Single restricted to the domain of unreachable type variables... Also, the same fragilty occurs if FDs are used.

Cheers, Max

Cheers, Carlos

On Thu, May 20, 2010 at 7:54 PM, Max Bolingbroke < batterseapower@hotmail.com> wrote:

On 20 May 2010 20:30, Carlos Camarao wrote:

...

... Also, the same fragilty occurs if FDs are used.

This remark is surprising to me. I thought the point of the FDs being declared on the original class (and the subsequent coverage condition check on instances) was to ensure that this fragility couldn't happen. Can you show an example (without using orphan instances) so I can get the idea?

Thanks, Max

Well, what I meant is just that the same would happen if we had a FD a->b in Example 1... (maybe I am not following you). That is: the same would happen if Example 1 was written with a FD as follows: class F a b | a -> b where f:: a -> b instance O a where o:: a And we had the same context: instance F Bool Bool where f = not instance O Bool where o = True k = f o kb = not k Then: kb is well-typed, because FD a |->b "closes the world", causing type (F a b, O a)=>Bool to be simplified ("improved") to Bool. But this type-correct program would become not typeable if instances such as the ones referred to before (by Daniel Fischer) instance F Int Bool where f = even instance O Int where o = 0 were later introduced, or imported... Cheers, Carlos

Hi Max. Excerpts from Max Bolingbroke's message of Sex Mai 21 04:56:51 -0300 2010: (...)

(Incidentally, the link to your paper is broken, so I haven't actually been able to read it, sorry!)

It was easy to find it on google. http://www.dcc.ufmg.br/~camarao/CT/solution-to-mptc-dilemma.pdf Greetings. (...) -- marcot http://wiki.debian.org/MarcoSilva

On 21 May 2010 01:58, Carlos Camarao wrote:

...

But this type-correct program would become not typeable if instances such as the ones referred to before (by Daniel Fischer) ...

It seems that single param type classes enjoy a nice property: ... * Adding an instance to the module defining the class cannot conflict with any non-orphan instance defined elsewhere ...

Max, thanks very much for your message. I will defer comments about definitions of orphan instances to a postscript. First I'd like to say the following. I think that a notion of orphan instances based on whether an instance is defined or not in the module where the class of the instance is defined is not very nice, because classes have global scope and then it should not matter in which module a class is defined, as long as it is defined somewhere in the current or some imported module. Let us thus not try to extend a definition based on this to MPTCs. However, the module fragility issue you raised is quite relevant. Let us call a type-correct module M fragile if definitions inserted in modules imported by M cause M to become type-incorrect. This issue is more relevant in Haskell than in other languages because instance definitions are automatically imported when a module is imported, and importation of an instance cannot be forbidden. Our "unreacheable_var-implies-overloading_resolution_test" proposal can be viewed as a proposal to "test-visible-instances-before-considering-types-as-ambiguous". Ambiguity means the existence of two or more conflicting definitions that could be used in an expression (and the inexistence of a reasonable criteria for selecting between conflicting definitions). In Haskell, nowadays, ambiguity is reported without looking to see if there really are conflicting definitions. What FDs do is to require programmers to specify dependencies between class variables which make the compiler look to see if there exist definitions that can satisfy such dependencies, before reaching any conclusion that an expression is ambiguous. What we propose (relieving the burden on programmers) is to make the compiler look itself to see if there exist two or more (well, or none) definitions and report error only if this is the case (again, before reaching any conclusion that an expression is ambiguous). If there is exactly one instance definition, there is no ambiguity (there is no conflict); in such case, then: use that single definition that the programmer defined. A benefit of adopting our approach would be that defaulting would become unnecessary (defaulting always occurring in favor of visible definitions). Module robustness can be achieved --- even maintaining automatic importation of instance definitions --- by considering, for each instance definition, say I, defined by instance C bla1 I bla2 where ... that an automatic defaulting rule that names C (see hackage.haskell.org/trac/haskell-prime/wiki/Defaulting) is virtually and automatically inserted, namely: default C bla1 I bla2 It should perhaps be noted though that one could have more than one such automatic default rule for the same class. Cheers, Carlos ===================================================================== PS: I think that a definition of orphan/non-orphan instance definition for MPTCs should be different. Letting: defM(C) = module where C is defined local-datatype(T,M,C) = T is defined in M or T is defined in defM(C) import-list(M,C) = {M} U { import-list(M') | M imports M'} instance-def(I,C,M,tv) = I is an instance definition of class C, occurring in module M, that instantiates class variable tv then you consider (if I have correctly understood and expressed what you wrote): Non-orphan = [for all I,C,M,tv: instance-def(I,C,M,tv) => local-datatype(T,M,C)] Orphan = [there exists I,C,M,tv: instance-def(I,C,M,tv) ^ not local-datatype(T,M,C)] And I think a correct definition of orphan/non-orphan for MPTCs should be along the line: Non-orphan = [there exists I,C,M,tv: instance-def(I,C,M,tv) ^ local-datatype(T,M,C) Orphan = [forall I,C,M,tv: instance-def(I,C,M,tv) ^ not local-datatype(T,M,C)] That is, an instance should be considered non-orphan if there exists at least one datatype to which a class type variable in such instance is instantiated, because other instances which instantiated such class type variable to such datatype would be non-orphan. GHC is thus correct, I think.

Hi Carlos, Apologies for the lateness of my reply. On 23 May 2010 02:24, Carlos Camarao wrote:

I think that a notion of orphan instances based on whether an instance is defined or not in the module where the class of the instance is defined is not very nice

I broadly agree, but pragmatically the notion of orphans is useful for designing robust libraries, even if the notion is a bit horrible.

A benefit of adopting our approach would be that defaulting would become unnecessary (defaulting always occurring in favor of visible definitions).

This is something I don't understand (and is not elaborated in your paper that I can see). Defaulting seems like an orthogonal mechanism. It turns a constraint that really does have multiple solutions (e.g. (Num a) => ...) into one where a particular preferred choice is taken (e.g. Num Int), in situations where abstracting over the choice is disallowed. However, you mechanism only turns constraints into instances when there is no ambiguity. Can you perhaps explain what you mean a bit further? I looked at your definition for orphan-hood, which I think might be OK if you don't have FlexibleInstances. However, if you do then consider this series of modules: """ {-# LANGUAGE MultiParamTypeClasses #-} module Common where class C a b where foo :: a -> b -> String """ """ {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} {-# OPTIONS_GHC -fwarn-orphans #-} module Mod2 where import Common data E = E instance C a E where foo _ _ = "Mod2" """ """ {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} {-# OPTIONS_GHC -fwarn-orphans #-} module Mod1 where import Common data D = D instance C D b where foo _ _ = "Mod1" """ """ {-# OPTIONS_GHC -fwarn-orphans #-} import Common import Mod1 import Mod2 main = putStrLn (foo D E) """ None of the instances are reported as orphans but IMHO they should be, because we get a conflict in the Main module. I guess that a MPTC instance (C t1 .. tn) for class C in module M1 is NOT an orphan if: 1) C is defined in the same module as the instance 2) OR ALL the t1..tn are instantiated to some concrete type (i.e. not a type variable) defined in the same module as the instance Imagine that we had an instance defined in a different module than the class and violating 2). Then: \exists i. t_i is a type variable or a datatype defined in another module Case 1: If t_i is a type variable, we can have a parallel module M2: """ data F = F instance C a_1 ... a_{i-1} F a_{i+1} ... a_n where """ Adding the instance to M2 may break client code because it is potentially ambiguous with the one from M1. Furthermore, the instance is considered non-orphan by GHC because it has at least one type which is defined in the same module. However, at least one of this instance and the one in M1 should have been flagged as orphans :( Case 2: if t_i is a datatype G defined in another module, we can similarly consider adding a new instance to that module: """ instance C a_1 ... a_{i-1} G a_{i+1} ... a_n where """ Same argument as for case 1. Does this seem right? == Basically, you want an orphanhood criteria P you can test locally on a per-module basis such that: * For any composition of modules where P holds on every module individually... * Changing any module by *adding* instances such that P still holds.. * Is guaranteed not to break any other module due to ambiguity It is not clear to me exactly what this should look like, especially in the presence of more complicated instance definitions (like the "instance C [Bool]" style of thing allowed by FlexibleInstances. It would probably be interesting to find out though. Cheers, Max