On 10/1/2014 6:02 PM, Carter Schonwald wrote:

This proposal is missing a key ingredient, how to resolve import of two conflicting instances. And I can't imagine any good selection strategy under this scoping scheme. Why should two conflicting in-scope instances be a valid situation? All I'm doing is making instance resolution more similar to other name resolution. Creating a new instance in a scope shadows the instance outside the scope, but multiple instances in the same scope aren't allowed.

Additionally, how this would work in the case of fancier programs that use fundeps and multiparam type classes to construct type level programs is a bit confusing. Would this entail that those programs would have hot swappable parts? What does that mean? You're right, I didn't pay much attention to the fancier stuff we can do. I don't think this will cause trouble, but I'm not qualified to say that with certainty.

One hackage package that would suffer terribly would be the HList one I think. A cursory glance at HList reveals several open type families. I *think* that they can be rewritten to be closed families.

Also I'm not sure what implications this would have for how type inference would work. Having global uniqueness is a wonderful assumption to have, and losing it might result in losing huge swaths of type inference, because suddenly we have 'pick the instance in the nearest scope'.. So how would this notion interact with the instance resolution that happens for overlapping instances? If there's an exact instance that matches the local instance, the local instance shadows it, and overlapping instance inference proceeds as usual.

Some examples:

module Foo where import Bar (Baz) -- With an instance Show (Baz a) instance Show (Baz a) where -- shadows the instance from Bar foo = let instance Show (Baz a) where -- shadows the module instance instance Show (Baz Quz) where -- Does not shadow any instance, OverlappingInstances -- resolution proceeds with the two instances defined in -- the let block

Hope this clarifies things, Gesh

On 2014-10-01 21:49, David Menendez wrote:

On Wed, Oct 1, 2014 at 10:36 AM, Gesh hseG wrote:

...

...

It seems the first part of your proposal just says "Haskellers can no longer expect class instance coherence." As such, this is a drastic change that would require all Haskell programs to be inspected to see if they crucially rely on coherence No. Coherence is preserved, since you always use the unique in-scope dictionary. What *is* lost, however, is global uniqueness, which means that code that assumes that the same dictionary is used for the same type across calls to functions must be modified. Arguably, that code is semantically incorrect to begin with, but that's neither here nor there.

How is that neither here nor there? Haskell says that types belong to classes, and each (type) instance of a class has a specific implementation. The fact that GHC implements this using dictionaries is irrelevant. It’s perfectly valid to implement type classes with partial evaluation, or matching on type parameters, or even C++-style templates.

In other words: no, coherency is not preserved. You can’t change the semantics of classes and then say that programs built around the old semantics were wrong all along.

+1 to this post. -1 to the proposal. (I say "proposal"... this needs some serious fleshing out and a semi-formal specification for instance resolution rules &c before it becomes a proposal. Just "Look at Oleg's paper" is not good enough.) Regards,

Please consider the needs of Haskell *readers* as well as Haskell *writers*, even bears of very little brain like me. This sounds to me like a proposal to make writing (some) programs easier but reading them much harder.

On 02/10/14 02:50, Richard Eisenberg wrote:

For what it's worth, I think I can agree that types like `Set` should carry around the relevant `Ord` dictionary.

What exactly do you mean by that? Redefining the Set type so that it carries a dictionary, such as data Set a where Bin :: Ord a => ... or somehow modifying GHC's internal dictionary passing mechanism without changing any user code (such as Data.Set)? Roman

How can we merge two Sets if they carry different Ord dictionaries? 02.10.2014, 03:51, "Richard Eisenberg" :

Thanks, Gesh, for the email below and the previous one, spelling out the distinction between coherence and global uniqueness. I had been conflating coherence and global uniqueness (as it seems others have been), and drawing this out is helpful.

Though I can't yet say I'm in support, exactly, I'm less vehemently against this idea than I was this morning. In particular, I actually really like the idea of local class instances, which have occurred to me before but which I've never considered seriously.

Unfortunately, this all breaks apart horribly when thinking about type instances. Global uniqueness, not just coherence, is needed for type instances:

...

 type family F a b  type instance F a b = b

 oops :: F a b -> b  oops = id

 unsafeCoerce :: a -> b  unsafeCoerce = let type instance F a b = a in                 oops

The problem is that a type instance introduces a type equality. Haskell is capable of passing type equality evidence around, so equalities can escape their scope, if the programmer wants to do so. Thus, there can never be a situation where some type (in this case `F a b`) is equal to one thing in one context and an incompatible thing in a different context, anywhere in the same program. I've written my example above with non-associated types, but the same thing can be written with associated types (and more syntactic overhead). I can't currently imagine a type-safe system that did not require global uniqueness for type instances.

For what it's worth, I think I can agree that types like `Set` should carry around the relevant `Ord` dictionary. Global uniqueness of class instances is already threatened by all manner of extensions; we've just been much more careful about global uniqueness of type instances.

Richard

On Oct 1, 2014, at 6:05 PM, Gesh wrote:

...

 On 10/1/2014 11:42 PM, Bardur Arantsson wrote:

...

 (I say "proposal"... this needs some serious fleshing out and a  semi-formal specification for instance resolution rules &c before it  becomes a proposal. Just "Look at Oleg's paper" is not good enough.)  I see I came off unclearly. Please allow me to remedy that.

 My reference to Oleg's paper was badly framed. What I meant to say was  more along the following lines:  Oleg discussed adding local typeclass instances in his reflection paper.  For some reason, his proposal wasn't taken. (Does anyone know why?)  I'd like to suggest something along similar lines:  Allow instances in let-expressions and where-clauses. These instances  shadow other instances with the same parameter list.  Similarly, instances defined in modules shadow imported instances.

 Thus, in the following program:

...

 module Foo where  import Bar (Baz) -- Where Bar defines instance Show (Baz a)  instance Show (Baz a) where -- shadows the imported instance  foo = let instance Show (Baz a) where -- shadows the instance defined        in ...              -- in where below, just like other bindings    where instance Show (Baz a) -- shadows the module-global instance          instance Show (Baz Quz) -- only allowed with          -- OverlappingInstances, isn't shadowed by any of the other          -- instances in this example.  In this example, the instances for Baz have the following scopes:  * From Bar: Nowhere, as it is immediately shadowed.  * From Foo: Within all top-level declarations besides foo, as foo's             where clause shadows it.  * From the where clause: Within the where clause. The instance for                          Baz Quz is also visible within the let                          expression, as it is not shadowed by it.  * From the let expression: Within the let expression.

 Basically all I'm doing is applying regular name resolution semantics  to instances with the same parameter lists.

 I hope this helps clarify things. If not, please tell me what needs to  be done to fully clarify this.

 Gesh  _______________________________________________  Haskell-Cafe mailing list  Haskell-Cafe@haskell.org  http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 10/2/2014 2:50 AM, Richard Eisenberg wrote:

Unfortunately, this all breaks apart horribly when thinking about type instances. Global uniqueness, not just coherence, is needed for type instances:

...

type family F a b type instance F a b = b

oops :: F a b -> b oops = id

unsafeCoerce :: a -> b unsafeCoerce = let type instance F a b = a in oops

The problem is that a type instance introduces a type equality. Haskell is capable of passing type equality evidence around, so equalities can escape their scope, if the programmer wants to do so. Thus, there can never be a situation where some type (in this case `F a b`) is equal to one thing in one context and an incompatible thing in a different context, anywhere in the same program. I've written my example above with non-associated types, but the same thing can be written with associated types (and more syntactic overhead). I can't currently imagine a type-safe system that did not require global uniqueness for type instances. Thank you, Richard, for giving a concrete example.

Several things can be said about the above code. First and foremost, it seems unsafe to allow oops to even typecheck today. Suppose `F` did not have a catchall instance. Then the type `F a b` is morally equivalent to `forall a. a`, because we could create any instance we wished for `F`. Therefore, I would suggest that regardless of my original proposal being accepted, we only allow open type families in type signatures where they are either morally equivalent to closed type families (by having catchall instances) or where they appear as restrictions on more polymorphic values (such as `id :: F a b -> F a b`). Associated types would also be permitted if an instance of their typeclass were in scope. Second, as hinted above, open type families with catchall instances are morally equivalent to a closed type families, since no other instances can be added to them without overlapping with the catchall instance. Therefore, I also suggest that open type families with catchall clauses be considered closed. Finally, this case serves as an excellent example to show that if and when we add support for local closed type families, we must consider the local type family distinct from the global one. In particular, one won't be able to pass instances of the local families to functions expecting the global family without compromising type safety. With the proposal from my first point, we outlaw `oops`, even with associated types, and thereby regain type safety. Any other problems? Gesh

On 10/2/2014 10:09 PM, Richard Eisenberg wrote:
 > On Oct 2, 2014, at 2:37 PM, Gesh  wrote:
 >> On 10/2/2014 2:50 AM, Richard Eisenberg wrote:
 >>>> type family F a b
 >>>> type instance F a b = b
 >>>>
 >>>> oops :: F a b -> b
 >>>> oops = id
 >>
 >>
 >> Several things can be said about the above code.
 >> First and foremost, it seems unsafe to allow oops to even typecheck
 >> today. Suppose `F` did not have a catchall instance. Then the type
 >> `F a b` is morally equivalent to `forall a. a`, because we could
 >> create any instance we wished for `F`. Therefore, I would suggest
 >> that regardless of my original proposal being accepted, we only
 >> allow open type families in type signatures where they are either
 >> morally equivalent to closed type families (by having catchall
 >> instances) or where they appear as restrictions on more polymorphic
 >> values (such as `id :: F a b -> F a b`). Associated types would
 >> also be permitted if an instance of their typeclass were in scope.
 >>
 >
 > I'm sorry, but I don't understand the paragraph above at all.
 > You say below that "open type families with catchall instances
 > [such as F] are morally equivalent to closed type families" and you
 > say "we only allow open type families in type signatures where there
 > are morally equivalent to closed type families". So it seems `oops`
 > is OK. And I don't know what you're getting at by
 > "restrictions on more polymorphic values".
 >
 > Incidentally, as type family instances can *never* overlap, a type
 > family with a catchall instance must have only that one instance.
 >
 >> Second, as hinted above, open type families with catchall instances
 >> are morally equivalent to a closed type families, since no other
 >> instances can be added to them without overlapping with the catchall
 >> instance. Therefore, I also suggest that open type families with
 >> catchall clauses be considered closed.
 >
 > What does your last sentence mean? What do you mean by a type family
 > that is considered closed?
 >
 >> Finally, this case serves as an excellent example to show that if
 >> and when we add support for local closed type families, we must
 >> consider the local type family distinct from the global one.
 >
 > But I don't have a local type family. I have a local type family
 > instance. How can one instance be seen as distinct from another?
 >
 >> In particular, one
 >> won't be able to pass instances of the local families to functions
 >> expecting the global family without compromising type safety.
 >
 > Unlike class instances, type family instances do not form
 > dictionaries and are not passed around. Given that fact, I'm not
 > sure what you mean here.
Looking at what I wrote, I'm sorry for spreading confusion.

Basically, what I was trying to get at is the following:
* There are only three type-safe ways of using instances of open type
   families:
   * As a specialization of a polymorphic function
   * If the open type family is an associated type and an appropriate
     instance is in scope
   * If all possible instances are known, i.e. no more instances can be
     defined without overlapping. This is only possible when there
     exists a catchall instance. (I thought that open type families
     could overlap, but had OverlappingInstances-like semantics. In
     either case, catchall instances eliminate all possibility of
     additional instances. This also explains my point above regarding
     "open type families considered closed", in that if we had
     OverlappingInstances semantics, it would make sense that a
     declaration like
 > type family Open a
 > type instance Open Foo = Bar
 > type instance Open a = a
     would be equivalent to the declaration
 > type family Open a where
 >     Open Foo = Bar
 >     Open a   = a
     What I was suggesting was that these declarations be declared
     equivalent by fiat.)
* The above example, if `F` is taken to be a closed type family and
   the declarations are modified accordingly, shows that in the event
   that we allow local closed type family declarations, then in order
   to keep things type-safe, the local type family and the global one
   may not be considered equal. Otherwise, `unsafeCoerce` would be
   possible.

   But upon further reflection, this point is quite trivial.

Again, sorry for the confusion. I hope things are clearer now.

Gesh

How is that neither here nor there? Haskell says that types belong to classes, and each (type) instance of a class has a specific implementation. The fact that GHC implements this using dictionaries is irrelevant. It’s perfectly valid to implement type classes with partial evaluation, or matching on type parameters, or even C++-style templates. How is this point relevant? As far as I understand typeclasses enjoy

In other words: no, coherency is not preserved. You can’t change the semantics of classes and then say that programs built around the old semantics were wrong all along. Correct, although that's not what I said. I just said that a case could be made for saying the design of programs around global uniqueness was

On 10/1/2014 10:49 PM, David Menendez wrote: three properties: confluence, coherence and global uniqueness. These are defined as follows: * Confluence: Constraint-solving always terminates with the same sets of constraints on terms. * Coherence: The same instance is always chosen for terms. * Global uniqueness: For any type and typeclass, there exists at most one instance of the typeclass for the type. What I suggested was to weaken global uniqueness to local uniqueness, defined as: * Local uniqueness: For any type and typeclass, in any scope there exists at most one instance of the typeclass for the type. And a scope is a set of parallel bindings, introduced by a module declaration, let expression or where clause. Since this only affects global uniqueness, I fail to see how concerns about coherence being lost are relevant. poorly thought out. I admit that these changes will require people to redesign such programs. I'm not convinced this is a bad thing. I am sorry for not being clearer to begin with. Gesh

Daniel, This is an interesting discussion and I personally also think Haskell should in time move away from global uniqueness of instances, at least as the default. 2014-10-02 10:50 GMT+02:00 Daniel Trstenjak :

On Thu, Oct 02, 2014 at 12:44:25AM +0300, Gesh wrote:

...

Correct, although that's not what I said. I just said that a case could be made for saying the design of programs around global uniqueness was poorly thought out.

I think the problem is, that for some type classes global uniqueness is a very good idea and for some it might not be that relevant.

If there's e.g. a PrettyPrint type class, then one might argue, that it's a good idea to be able to change the pretty printing of a data type depending on the context.

But for a type class represeting the equality of a data type it might be more harmful then good, to be able to change it.

I think you're right that whether we want global uniqueness of instances depends on the situation. However, it doesn't just depend on the type class in question. Consider for example the Ord type class. The fact that we sometimes want to use different orderings for the same data types is clearly evidenced by the existence of functions such as sortBy and all of the "comparing ..." stuff in Data.Ord. On the other hand, there is the fact that data types like Set crucially depend on being used with a single Ord instance for correctness. As you suggest, a way to deal with this could be to make a data type like Data.Set carry around the Ord instance, something like this: data Set a where SomeInternalConstructor :: Ord a => ... insert :: a -> Set a -> Set a However, it seems a bit unfortunate to me that this extra data (the type class dictionary) would be carried around at runtime instead of it being inferred and potentially compiled out at compile time. I wonder if a more static alternative could be to introduce some limited form of dependent types (I'm reminded of Scala's value-dependent types) to index the Data.Set data type with the Ord instance that it should be used with, something like: data Set a (instOrdA :: Ord a) where ... insert :: (ordA :: Ord a, ordA ~v instOrdA) => a -> Set a instOrdA -> Set a instOrdA In such code, the constraint "ordA ~v instOrdA" would require that the two instances are equal in some intentional and decidably checkable way (i.e. no automatic unfolding of recursive definitions and such). Perhaps it's not even needed to require the "(ordA :: Ord a, ordA ~v instOrdA) =>" contraint, but the compiler could somehow just take the instance from the "Set a instOrdA" type and make it available for type class resolution in the body of insert? Anyway, I agree with Gesh that at some point, Haskell should deprecate global uniqueness of type class instances, but we should first explore alternatives for modeling data types like Set that currently depend on it. There's still quite some room for research here in my opinion. Regards, Dominique

On Thursday, October 2, 2014 11:30:20 AM UTC+2, Dominique Devriese wrote:

Daniel,

This is an interesting discussion and I personally also think Haskell should in time move away from global uniqueness of instances, at least as the default.

2014-10-02 10:50 GMT+02:00 Daniel Trstenjak javascript:>:

...

On Thu, Oct 02, 2014 at 12:44:25AM +0300, Gesh wrote:

...

Correct, although that's not what I said. I just said that a case could be made for saying the design of programs around global uniqueness was poorly thought out.

I think the problem is, that for some type classes global uniqueness is a very good idea and for some it might not be that relevant.

If there's e.g. a PrettyPrint type class, then one might argue, that it's a good idea to be able to change the pretty printing of a data type depending on the context.

But for a type class represeting the equality of a data type it might be more harmful then good, to be able to change it.

I think you're right that whether we want global uniqueness of instances depends on the situation. However, it doesn't just depend on the type class in question.

Consider for example the Ord type class. The fact that we sometimes want to use different orderings for the same data types is clearly evidenced by the existence of functions such as sortBy and all of the "comparing ..." stuff in Data.Ord. On the other hand, there is the fact that data types like Set crucially depend on being used with a single Ord instance for correctness.

As you suggest, a way to deal with this could be to make a data type like Data.Set carry around the Ord instance, something like this:

data Set a where SomeInternalConstructor :: Ord a => ... insert :: a -> Set a -> Set a

However, it seems a bit unfortunate to me that this extra data (the type class dictionary) would be carried around at runtime instead of it being inferred and potentially compiled out at compile time.

I wonder if a more static alternative could be to introduce some limited form of dependent types (I'm reminded of Scala's value-dependent types) to index the Data.Set data type with the Ord instance that it should be used with, something like:

data Set a (instOrdA :: Ord a) where ... insert :: (ordA :: Ord a, ordA ~v instOrdA) => a -> Set a instOrdA -> Set a instOrdA

In such code, the constraint "ordA ~v instOrdA" would require that the two instances are equal in some intentional and decidably checkable way (i.e. no automatic unfolding of recursive definitions and such). Perhaps it's not even needed to require the "(ordA :: Ord a, ordA ~v instOrdA) =>" contraint, but the compiler could somehow just take the instance from the "Set a instOrdA" type and make it available for type class resolution in the body of insert?

I also like this design, and it's been discussed before in the same context (http://lists.seas.upenn.edu/pipermail/types-list/2009/001412.html). I know a few ways to allow checking the constraints, but I'm not sure whether any of these fits with Haskell: - using definitional equality like in dependent types, or some encoding thereof (e.g. with empty types, as when encoding Peano numbers in the Haskell type system) - using singleton types, as in Scala (not really powerful, and does not fit with Haskell). However, Scala's relevant feature arise from making ML modules first-class and unifying them with objects. For Haskell, I'd leave out objects and get to... - use some variant of ML modules, where the modules are easier to compare because they're second-class (I wonder whether that means using singleton kinds where Scala uses singleton types). Given that the upcoming Backpack descends from a form of ML modules, this might be more relevant than is currently apparent (to me at least). Anyway, I agree with Gesh that at some point, Haskell should deprecate

global uniqueness of type class instances, but we should first explore alternatives for modeling data types like Set that currently depend on it. There's still quite some room for research here in my opinion.

On 10/4/2014 9:52 AM, Bertram Felgenhauer wrote:

I think there are different possible interpretations of coherence in the absence of global uniqueness. To me, correctness of Data.Set (which your proposal would break) relies solely on coherence, on the fact that the comparisons in its various functions always go the same way for any two given values. Global or local uniqueness should not matter; after all, the locations of those comparisons do not change. (Actually, ghc falls short of this ideal, see [1].) Put differently, I view global uniqueness as an ingredient for ensuring coherence in the case that instance selection is deferred to the caller. Please reread my definition of coherence. Admittedly, it is slightly too concise, but the way I define coherence is that no matter how you resolve constraints, the same instance is picked for each term.

(let instance Ord Char where compare = flip (compare `on` ord) in 'a' < 'b' , 'a' < 'b') == (False, True)

You seem to be defining coherence as meaning that no matter where a term appears, then if the same type is inferred for it the same instance will be picked. I fail to see how this does not require global uniqueness of instances, nor how the locations of the comparisons have anything to do with it. Just for clarification, the difference between our definitions is that under your definition, it seems that no matter where I see the term `'a' < 'b'`, it will reduce to `True`. However, under my definition, while the reduction is context-dependent, since the same instance will be chosen in both expressions - that is, the local one in the first element and the global one in the second - under any valid constraint resolver.

You seem to take the relaxed view that coherence is already satisfied if instance selection is deferred to the caller, even if different callers may select different instances for the same types. If what you're saying is that in my opinion, the above code is coherent, then I agree with your statement.

Please, could you clarify your statements? Thanks, Gesh

Sorry, I'm very late in returning to this thread, but maybe the answer
is still of some interest.

Gesh wrote:
> On 10/4/2014 9:52 AM, Bertram Felgenhauer wrote:
> >I think there are different possible interpretations of coherence in the
> >absence of global uniqueness. To me, correctness of Data.Set (which your
> >proposal would break) relies solely on coherence, on the fact that the
> >comparisons in its various functions always go the same way for any two
> >given values.  Global or local uniqueness should not matter; after all,
> >the locations of those comparisons do not change. (Actually, ghc falls
> >short of this ideal, see [1].) Put differently, I view global uniqueness
> >as an ingredient for ensuring coherence in the case that instance
> >selection is deferred to the caller.

> Please reread my definition of coherence. Admittedly, it is slightly
> too concise, but the way I define coherence is that no matter how you
> resolve constraints, the same instance is picked for each term.

I had the impression that different people in this thread were using
different interpretations of "coherence"; my aim was to point out this
possible misunderstanding.

> You seem to be defining coherence as meaning that no matter where a term
> appears, then if the same type is inferred for it the same instance will
> be picked.

Right. This justifies inlining, for example.

It also ensures that Data.Set as is is correct, without having to worry
about different paths to the set implementation leading to different
results. I find this very desirable.

> I fail to see how this does not require global uniqueness of
> instances, nor how the locations of the comparisons have anything to do
> with it.

I could have phrased that better. What I mean is that global uniqueness
would not have to be stated explicitely, because, as you write, it's a
consequence of the stronger interpretation of coherence.

> > (let instance Ord Char where compare = flip (compare `on` ord)
> >  in 'a' < 'b'
> > ,   'a' < 'b')
> > == (False, True)
> the same instance will be chosen in both expressions - that is,
> the local one in the first element and the global one in the second
> - under any valid constraint resolver.
> 
> >You seem to take the relaxed view that coherence is already satisfied if
> >instance selection is deferred to the caller, even if different callers
> >may select different instances for the same types.

> If what you're saying is that in my opinion, the above code is
> coherent, then I agree with your statement.

What I mean is that you consider this code to be coherent:

  (.<.) :: Ord a => a -> a -> Bool
  x .<. y = x < y

(by "deferred" instance selection I mean that the instance is provided
by the caller) even though

  (let instance Ord Char where compare = flip (compare `on` ord)
   in 'a' .<. 'b'
  ,   'a' .<. 'b')

shows that for x = 'a' and y = 'b', different instances may be used for
the 'a' < 'b' comparison in (.<.). This is, again, what breaks Data.Set.
It also breaks specialization. And what about factoring out 'a' .<. 'b'?

Overall I think global uniqueness is too useful to give up.

Cheers,

Bertram

P.S. Kiselyov et al. discuss a restriction for local instances based on
"opaque types" in Section 6.1. That looks like a good way for getting
useful local instances (in particular for the configurations problem)
without giving up global uniqueness.