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

[Job Vranish]

Sorry for reopening an old thread, but I thought I'd counter some of the
negative feedback :)


I think this proposal is a great idea!

It seems like this would make working with MPTCs much easier.
When programming, I generally want to only specify the minimum amount of
information to make my code logically unambiguous.
If the code contains enough information to infer the proper instantiation
without the use of an FD, then I shouldn't need to add a FD.
It seems like this would have much more of a "it just works" feel than the
currently alternatives.

Also the MPTC + FDs type errors are a pain. I'm not sure if the type errors
for your proposal would be better, but it would be hard to make them worse.

I do worry about imported instances, (over which we currently have little
control) messing up our code. But this would probably be pretty unusual and
I feel that this is more of a problem with how instances are imported than
with this proposal itself.


Anyway, just my two cents,

- Job


On Thu, May 20, 2010 at 10:34 AM, Carlos Camarao
<carlos.camarao at gmail.com>wrote:

> This message presents, informally, a proposal to solve Haskell's MPTC
> (multi-parameter type class) dilemma. If this informal proposal turns
> out to be acceptable, we (I am a volunteer) can proceed and make a
> concrete proposal.
>
> The proposal has been published in the SBLP'2009 proceedings and is
> available at
>     www.dcc.ufmg.br/~camarao/CT/solution-to-MPTC-dilemma.pdf<http://www.dcc.ufmg.br/%7Ecamarao/CT/solution-to-MPTC-dilemma.pdf>
>
> The well-known dilemma
> (hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClassesDilemma)
> is that it is generally accepted that MPTCs are very useful, but their
> introduction is thought to require the introduction also of FDs
> (Functional Dependencies) or another mechanism like ATs (Associated
> Types) and FDs are tricky and ATs, somewhat in a similar situation,
> have been defined more recently and there is less experience with its
> use.
>
> In
>
> www.haskell.org/ghc/dist/current/docs/html/users_guide/type-class-extensions.html
> there exists a solution to the termination problem related to the
> introduction of MPTCs in Haskell. In our proposal, neither FDs nor any
> other mechanism like ATs are needed in order to introduce MPTCs in
> Haskell; the only change we have to make is in the ambiguity
> rule. This is explained below. The termination problem is essentially
> ortogonal and can be dealt with, with minor changes, as described in
> the solution presented in the above mentioned (type-class-extensions)
> web page.
>
> Let us review the ambiguity rule used in Haskell-98 and after that the
> ambiguity rule used in GHC. Haskell-98 ambiguity rule (which is
> adequate for Haskell-98's single parameter type classes) is: a type
> C => T is ambiguous iff there is a type variable v that occurs in the
> "context" (constraint set) C but not in the simple (unconstrained)
> type T.
>
> For example: forall a.(Show a, Read a)=>String is ambiguous, because
> "a" occurs in the constraints (Show a,Read a) but not in the simple
> type (String).
>
> 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
>
> Type forall a b. (C a b,O a) => b can be considered to be not
> ambiguos, since overloading resolution can be defined so that
> instantiation of "b" can "determine" that "a" should also be
> instantiated (as FD b|->a does), thus resolving the overloading.
>
> GHC, since at least version 6.8, makes significant progress towards a
> definition of ambiguity in the context of MPTCs; GHC 6.10.3 User’s
> Guide says (section 7.8.1.1):
>
>   "GHC imposes the following restrictions on the constraints in a type
>   signature. Consider the type: forall tv1..tvn (c1, ...,cn) => type. ...
>   Each universally quantified type variable tvi must be reachable from
> type.
>   A type variable a is reachable if it appears in the same constraint as
>   either a type variable free in the type, or another reachable type
> variable.”
>
> For example, type variable "a" in constraint (O a) in the example
> above is reachable, because it appears in (C a b) (the same constraint
> as type variable "b", which occurs in the simple type).
>
> 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.
> (A formal definition, with full details, is in the cited SBLP'09 paper.)
>
> 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).
>
> As another example (Example 2), consider:
>
> {-# NoMonomorphismRestriction, MultiParameterTypeClasses #-}
> data Matrix = ...
> data Vector = ...
> class Mult a b c where (*):: a ! b ! c
> instance Mult Matrix Vector Matrix where (*) = ...
> instance Mult Matrix Vector Vector where (*) = ...
> m1:: Matrix = ...
> m2:: Vector = ...
> m3:: Vector = ...
> m = (m1 * m2) * m3
>
> GHC gives the following type to m:
>   m :: forall a, b. (Mult Matrix Vector a, Mult a Vector b) => b
>
> However, "m" cannot be used effectively in a program compiled with
> GHC: if we annotate m::Matrix, a type error is reported. This occurs
> because the type inferred for "m" includes constraints (Mult Matrix
> Vector a, Mult a Vector Matrix) and, with b|->Matrix, type variable "a"
> appears only in the constraint set, and this type is considered
> ambiguous. Similarly, if "m" is annotated with type Vector, the type
> is also considered ambiguous. There is no means of specializing type
> variable "a" occurring in the type of "m" to Matrix. And no FD may be
> used in order to achieve such specialization, because we do not have
> here a FD: "a" and "b" do not determine "c" in class Mult: for (a,b =
> Matrix,Vector), we can have "c" equal to either Matrix or Vector.
>
> According to our proposal, type m:: forall a. (Mult Matrix Vector a,
> Mult a Vector Matrix)) => Matrix is not ambiguous, in the context of
> the class and instance declarations of Example 2 (since "a" can be
> instantiated to Matrix), whereas type m:: forall a.(Mult Matrix Vector
> a, Mult a Vector Matrix)) => Vector is ambiguous in this context.
>
> We would like to encourage compiler front-end developers to change
> Haskell's ambiguity rule, and test with as many examples as desired,
> including recurring examples that appear in Haskell mailing lists
> involving MPTCs, FDs etc. We would like to hear and discuss your
> doubts, opinions, comments, criticisms etc.
>
> Cheers,
>
> Carlos
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100608/e159bdf3/attachment.html