Proposal to solve Haskell's MPTC dilemma

[Carlos Camarao]

On 05/26/10 15:42, Carlos Camarao wrote:

> I think you are proposing using the current set of instances in
> scope in order to remove ambiguity.  Am I right?

I think that an important point is that it is not exactly "to remove
ambiguity", because the proposal tries to solve the problem exactly
when there is really no ambiguity. There would be ambiguity if there
were two or more conflicting definitions, and the proposal is to use,
upon occurrence of an unreachable type variable in a constraint, an
instance in the current context that is the single instance that could
be used to instantiate that type variable.

This was perhaps made unclear when I incorrectly wrote in haskell-cafe
that the proposal eliminates the need for defaulting. I should have
said that defaulting is not necessary to force instantiation (of
unreachable variables) when there are no conflicting definitions in
the current context. That is, defaulting should be used exactly to
remove ambiguity, i.e. when there exist conflicting definitions and
when unreachable type variables appear that can be instantiated to
such conflicting definitions.

> Your proposal appears to allow /incoherent/ instance selection.
> This means that an expression can be well-typed in one module, and
> well-typed in another module, but have different semantics in the
> two modules.  For example (drawing from above discussion) :
>
> module C where
>
> class F a b where f :: a -> b
> class O a where o :: a
>
> module P where
> import C
>
> instance F Bool Bool where f = not
> instance O Bool where o = True
> k :: Bool
> k = f o
>
> module Q where
> import C
> instance F Int Bool where f = even
> instance O Int where o = 0
> k :: Bool
> k = f o
>
> module Main where
> import P
> import Q
> -- (here, all four instances are in scope)
> main = do { print P.k ; print Q.k }
> -- should result, according to your proposal, in
> -- False
> -- True
> -- , am I correct?

If qualified importation of k from both P and from Q was specified, we
would have two *distinct* terms, P.k and Q.k.

Unqualified importation must cause an error (two distinct definitions
for the same non-overloaded name).

For overloaded names with distinct instances, *ambiguity* would be reported,
as e.g. in:

  module C where class O a where o::a
  module P where instance O Bool where o = True
  module Q where instance O Bool where o = False
  moduke Main where
    import P
    import Q
    main = do { print o::Bool }

> Also, in your paper, example 2 includes
>    m = (m1 * m2) * m3
> and you state
>> In Example 2, there is no means of specializing type variable c0
>> occurring in the type of m to Matrix.
> In Example 2, there is no means of specializing type variable c0
> occurring in the type of m to Matrix.
> I suggest that there is an appropriate such means, namely, to write
> m = (m1 * m2 :: Matrix) * m3

Yes, that solution is fine. Sorry, I should have written "There is no means
of specializing type variable c0 occurring in the type of m to Matrix,
without an explicit type annotation in the expression defining m."

> (Could the paper address how that solution falls short?
> Are there other cases in which there is more than just a little
> syntactical convenience at stake?
> , or is even that much added code too much for some use-case?)

The point should have been that you cannot make a class with
FDs eliminate the need for having to make explicit type annotations,
in cases such as these. The example should also be such that it
would need more type annotations, instead of just one...

Cheers,

Carlos
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20100527/881f22b0/attachment.html