On 05/26/10 15:42, Carlos Camarao wrote:<br><br>> I think you are proposing using the current set of instances in<br>> scope in order to remove ambiguity. Am I right? <br><br>I think that an important point is that it is not exactly "to remove<br>
ambiguity", because the proposal tries to solve the problem exactly<br>when there is really no ambiguity. There would be ambiguity if there<br>were two or more conflicting definitions, and the proposal is to use,<br>
upon occurrence of an unreachable type variable in a constraint, an<br>instance in the current context that is the single instance that could<br>be used to instantiate that type variable.<br><br>This was perhaps made unclear when I incorrectly wrote in haskell-cafe<br>
that the proposal eliminates the need for defaulting. I should have<br>said that defaulting is not necessary to force instantiation (of<br>unreachable variables) when there are no conflicting definitions in<br>the current context. That is, defaulting should be used exactly to<br>
remove ambiguity, i.e. when there exist conflicting definitions and<br>when unreachable type variables appear that can be instantiated to<br>such conflicting definitions.<br><br>> 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>Unqualified importation must cause an error (two distinct definitions<br>for the same non-overloaded name). <br>
<br>For overloaded names with distinct instances, *ambiguity* would be reported, as e.g. in:<br><br> module C where class O a where o::a<br> module P where instance O Bool where o = True<br> module Q where instance O Bool where o = False<br>
moduke Main where <br> import P<br> import Q<br> main = do { print o::Bool }<br><br>> Also, in your paper, example 2 includes<br>> m = (m1 * m2) * m3<br>> and you state<br>>> In Example 2, there is no means of specializing type variable c0<br>
>> occurring in the type of m to Matrix.<br>> In Example 2, there is no means of specializing type variable c0<br>> occurring in the type of m to Matrix.<br>> I suggest that there is an appropriate such means, namely, to write<br>
> m = (m1 * m2 :: Matrix) * m3<br><br>Yes, that solution is fine. Sorry, I should have written "There is no means<br>of specializing type variable c0 occurring in the type of m to Matrix,<br>without an explicit type annotation in the expression defining m."<br>
<br>> (Could the paper address how that solution falls short? <br>> Are there other cases in which there is more than just a little<br>> syntactical convenience at stake? <br>> , or is even that much added code too much for some use-case?)<br>
<br>The point should have been that you cannot make a class with<br>FDs eliminate the need for having to make explicit type annotations,<br>in cases such as these. The example should also be such that it<br>would need more type annotations, instead of just one...<br>
<br>Cheers,<br><br>Carlos<br><br>