2 Nov
2014
2 Nov
'14
12:53 p.m.
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.