[Haskell-cafe] Fwd: Increasing Haskell modularity

[Carter Schonwald]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141004/3e9f2bce/attachment.html>