[Haskell-cafe] Proposal to solve Haskell's MPTC dilemma

[Carlos Camarao]

On Thu, May 20, 2010 at 11:54 AM, Daniel Fischer
<daniel.is.fischer at web.de>wrote:

>
> On Thursday 20 May 2010 16:34:17, Carlos Camarao wrote:
> > In the context of MPTCs, this rule alone is not enough. Consider, for
> > example (Example 1):
> >
> >    class F a b where f:: a->b
> >    class O a where o:: a
> > and
> >     k = f o:: (C a b,O a) => b
> > ...
> > Our proposal is: consider unreachability not as indication of
> > ambiguity but as a condition to trigger overloading resolution (in a
> > similar way that FDs trigger overloading resolution): when there is at
> > least one unreachable variable and overloading is found not to be
> > resolved, then we have ambiguity. Overloading is resolved iff there is
> > a unique substitution that can be used to specialize the constraint
> > set to one, available in the current context, such that the
> > specialized constraint does not contain unreachable type variables.
> >...
> > Consider, in Example 1, that we have a single instance of F and
> > O, say:
> >
> > instance F Bool Bool where f = not
> > instance O Bool where o = True
> >
> > and consider also that "k" is used as in e.g.:
> >
> >    kb = not k
> >
> > According to our proposal, kb is well-typed. Its type is Bool. This
> > occurs because (F a b, O a)=>Bool can be simplified to Bool, since
> > there exists a single substitution that unifies the constraints with
> > instances (F Bool Bool) and (O Bool) available in the current context,
> > namely S = (a|->Bool,b|->Bool).
>
> But then somebody defines
>
> instance F Int Bool where f = even
> instance O Int where o = 0
>
> What then?
>

Then (F a b, O a)=>Bool is ambiguous. There are two substitutions that unify
(F a b, O a) with instances in the current context.


> Using the available instances to resolve overloading is a tricky thing,
> it's very easy to make things break that way.
>

Using the available instances is the natural, in fact the only way, to
resolve overloading.

Our proposal cannot make any well-typed program break, any program
whatsoever.

What it can do is to make programs that *were not well-typed* --- because
there existed an ambiguity error --- to be either:
   i) well-typed (because overloading is resolved), or
  ii) not well-typed (because overloading cannot in fact be resolved), and
in this case the ambiguity error may be deferred, to the point where the
unreachability occurs, if there was a FD annotated.

Cheers,

Carlos
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100520/163f96ec/attachment.html