5 Oct
2014
5 Oct
'14
4:09 a.m.
At the end of the say, for any interesting type system changes, there's only one way to check soundness with confidence : (machine checked) proofs. For simple changes it suffices to formalize the rules, but this seems a bit more subtle. On Oct 4, 2014 4:03 PM, "Gesh" <gesh@gesh.uni.cx> 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. > > 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 > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >