<br><div class="gmail_quote">On Thu, May 27, 2010 at 5:43 PM, David Menendez <span dir="ltr"><<a href="mailto:dave@zednenem.com">dave@zednenem.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao<br>
<div class="im"><<a href="mailto:carlos.camarao@gmail.com">carlos.camarao@gmail.com</a>> wrote:<br>
</div>> Isaac Dupree:<br>
<div><div></div><div class="h5">>> Your proposal appears to allow /incoherent/ instance selection.<br>
>> This means that an expression can be well-typed in one module, and<br>
>> well-typed in another module, but have different semantics in the<br>
>> two modules. For example (drawing from above discussion) :<br>
>><br>
>> module C where<br>
>><br>
>> class F a b where f :: a -> b<br>
>> class O a where o :: a<br>
>><br>
>> module P where<br>
>> import C<br>
>><br>
>> instance F Bool Bool where f = not<br>
>> instance O Bool where o = True<br>
>> k :: Bool<br>
>> k = f o<br>
>><br>
>> module Q where<br>
>> import C<br>
>> instance F Int Bool where f = even<br>
>> instance O Int where o = 0<br>
>> k :: Bool<br>
>> k = f o<br>
>><br>
>> module Main where<br>
>> import P<br>
>> import Q<br>
>> -- (here, all four instances are in scope)<br>
>> main = do { print P.k ; print Q.k }<br>
>> -- should result, according to your proposal, in<br>
>> -- False<br>
>> -- True<br>
>> -- , am I correct?<br>
><br>
> If qualified importation of k from both P and from Q was specified, we<br>
> would have two *distinct* terms, P.k and Q.k.<br>
<br>
</div></div>I think Isaac's point is that P.k and Q.k have the same definition (f<br>
o). If they don't produce the same value, then referential<br>
transparency is lost.<br>
<font color="#888888"><br>
--<br>
Dave Menendez <<a href="mailto:dave@zednenem.com">dave@zednenem.com</a>><br>
<<a href="http://www.eyrie.org/%7Ezednenem/" target="_blank">http://www.eyrie.org/~zednenem/</a>><br>
</font></blockquote></div><br>The definitions of P.k and Q.k are textually the same but the contexts are different. "f" and "o" denote distinct values in P and Q. Thus, P.k and Q.k don't have the same definition.<br>
<br>Thanks for the clarification. I thought the point was about coherence.<br><br>Cheers,<br><br>Carlos<br><br>