[Haskell-cafe] Fwd: Increasing Haskell modularity

[Bertram Felgenhauer]

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.