[Haskell-cafe] Fwd: Increasing Haskell modularity

[Gesh]

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.

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
 > (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.

Please, could you clarify your statements?

Thanks,

Gesh