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

[Carlos Camarao]

On Thu, May 20, 2010 at 1:25 PM, Max Bolingbroke <batterseapower at hotmail.com
> wrote:

> On 20 May 2010 16:50, Carlos Camarao <carlos.camarao at gmail.com> wrote:
> >> 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.
>
> AFAIK no other Haskell feature is defined in terms of "available
> instance" information. Overloaded functions are resolved by at least
> these mechanisms:
>  * Defaulting
>  * Information from unification (including from user-defined type
> signatures)
>  * Functional dependencies propagating information
>
> "Available instances" are not a natural addition to this list. In
> particular, using that information can cause programs to become
> untypeable when the module or *any module it imports transitively*
> defines a new instance. This leads to programs that are extremely
> fragile in the face of changes in the libraries!
>

Replace
  "Using the available instances is the natural, in fact the only way, to
  resolve overloading."
by
  "All overloading resolution has to consider the available instances,
   after unification, user-defined type signatures, defaulting and FDs have
been
  considered."

Extremely fragile is debatable; the important fact, highlighted, is that if
overloading resolution depends on the existence of a unique substitution,
then
the program may become untypeable when other instances are defined in the
visible typing context.

(Admittedly you can get the same issue with GHC Haskell as it is right
> now if you define an orphan instance in your module)
>

Yes. Just to emphasize, with our proposal the issue (of transforming a
well-typed program into a program which is not well-typed) is relevant only
when unreachable variables exist (for existing programs this never occurs,
since they are unambiguous according to the existing ambiguity rule).

The situation is even worse if you consider "available" instances to
> also include orphans defined in non-imported modules (as a
> whole-program compiler way very well do), because then you don't even
> need to have transitively imported the module which has added an
> instance for your program to stop type-checking.
>

Consider instances defined in non-imported modules to be visible in the
current
context is not correct, I think...


>
> Furthermore, if you intend to use an "overloaded" function at *one
> particular instance*, you could just have written the monomorphic type
> to begin with and not even bothered with overload resolution.
>

Sorry, I do not follow you here (why *at one particular instance*?).
A polymorphic (overloaded or not) function is defined and then used at
specific cases,
with different (instance) types.


>
> > Our proposal cannot make any well-typed program break, any program
> > whatsoever.
>
> That is true, but it makes extra things type check in a really fragile
> way. I'm not keen.
>

Really fragile meaning:
   "Overloading resolution depends on the set of available instances in the
following way:
    if a constraint on the type of an expression *contains unreachable
variables* and these
   type variables can be instantiated, by a single substitution(*), to
instances in the current
   context, then the constraint/overloading is resolved, and the type is not
ambiguous)."
then yes, ok.

(*) Single restricted to the domain of unreachable type variables...

Also, the same fragilty occurs if FDs are used.


> Cheers,
> Max
>

Cheers,

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