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 10/4/2014 9:52 AM, Bertram Felgenhauer wrote:
I think there are different possible interpretations of coherence in thePlease reread my definition of coherence. Admittedly, it is slightly
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.
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 ifIf what you're saying is that in my opinion, the above code is
instance selection is deferred to the caller, even if different callers
may select different instances for the same types.
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