Sorry for reopening an old thread, but I thought I&#39;d counter some of the negative feedback :)<br><br><br>I think this proposal is a great idea! <br><br>It seems like this would make working with MPTCs much easier.<br>When programming, I generally want to only specify the minimum amount of information to make my code logically unambiguous.<br>
If the code contains enough information to infer the proper instantiation without the use of an FD, then I shouldn&#39;t need to add a FD.<br>It seems like this would have much more of a &quot;it just works&quot; feel than the currently alternatives.<br>
<br>Also the MPTC + FDs type errors  are a pain. I&#39;m not sure if the type errors for your proposal would be better, but it would be hard to make them worse.<br><br>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.<br>
<br><br>Anyway, just my two cents,<br><br>- Job<br><br><br><div class="gmail_quote">On Thu, May 20, 2010 at 10:34 AM, Carlos Camarao <span dir="ltr">&lt;<a href="mailto:carlos.camarao@gmail.com">carlos.camarao@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">This message presents, informally, a proposal to solve Haskell&#39;s MPTC<br>(multi-parameter type class) dilemma. If this informal proposal turns<br>
out to be acceptable, we (I am a volunteer) can proceed and make a<br>concrete proposal.<br>
<br>The proposal has been published in the SBLP&#39;2009 proceedings and is<br>available at<br>    <a href="http://www.dcc.ufmg.br/%7Ecamarao/CT/solution-to-MPTC-dilemma.pdf" target="_blank">www.dcc.ufmg.br/~camarao/CT/solution-to-MPTC-dilemma.pdf</a><br>

<br>The well-known dilemma<br>(<a href="http://hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClassesDilemma" target="_blank">hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClassesDilemma</a>)<br>is that it is generally accepted that MPTCs are very useful, but their<br>

introduction is thought to require the introduction also of FDs<br>(Functional Dependencies) or another mechanism like ATs (Associated<br>Types) and FDs are tricky and ATs, somewhat in a similar situation,<br>have been defined more recently and there is less experience with its<br>

use.<br><br>In<br><a href="http://www.haskell.org/ghc/dist/current/docs/html/users_guide/type-class-extensions.html" target="_blank">www.haskell.org/ghc/dist/current/docs/html/users_guide/type-class-extensions.html</a><br>
there exists a solution to the termination problem related to the<br>
introduction of MPTCs in Haskell. In our proposal, neither FDs nor any<br>other mechanism like ATs are needed in order to introduce MPTCs in<br>Haskell; the only change we have to make is in the ambiguity<br>rule. This is explained below. The termination problem is essentially<br>

ortogonal and can be dealt with, with minor changes, as described in<br>the solution presented in the above mentioned (type-class-extensions)<br>web page.<br><br>Let us review the ambiguity rule used in Haskell-98 and after that the<br>

ambiguity rule used in GHC. Haskell-98 ambiguity rule (which is<br>adequate for Haskell-98&#39;s single parameter type classes) is: a type<br>C =&gt; T is ambiguous iff there is a type variable v that occurs in the<br>&quot;context&quot; (constraint set) C but not in the simple (unconstrained)<br>

type T.<br><br>For example: forall a.(Show a, Read a)=&gt;String is ambiguous, because<br>&quot;a&quot; occurs in the constraints (Show a,Read a) but not in the simple<br>type (String).<br><br>In the context of MPTCs, this rule alone is not enough. Consider, for<br>

example (Example 1):<br><br>   class F a b where f:: a-&gt;b<br>   class O a where o:: a<br>and <br>    k = f o:: (C a b,O a) =&gt; b <br><br>Type forall a b. (C a b,O a) =&gt; b can be considered to be not<br>ambiguos, since overloading resolution can be defined so that<br>

instantiation of &quot;b&quot; can &quot;determine&quot; that &quot;a&quot; should also be<br>instantiated (as FD b|-&gt;a does), thus resolving the overloading.<br><br>GHC, since at least version 6.8, makes significant progress towards a<br>

definition of ambiguity in the context of MPTCs; GHC 6.10.3 User’s<br>Guide says (section 7.8.1.1):<br><br>  &quot;GHC imposes the following restrictions on the constraints in a type<br>  signature. Consider the type: forall tv1..tvn (c1, ...,cn) =&gt; type. ...<br>

  Each universally quantified type variable tvi must be reachable from type. <br>  A type variable a is reachable if it appears in the same constraint as <br>  either a type variable free in the type, or another reachable type variable.”<br>

<br>For example, type variable &quot;a&quot; in constraint (O a) in the example<br>above is reachable, because it appears in (C a b) (the same constraint<br>as type variable &quot;b&quot;, which occurs in the simple type).<br>

<br>Our proposal is: consider unreachability not as indication of<br>ambiguity but as a condition to trigger overloading resolution (in a<br>similar way that FDs trigger overloading resolution): when there is at<br>least one unreachable variable and overloading is found not to be<br>

resolved, then we have ambiguity. Overloading is resolved iff there is<br>a unique substitution that can be used to specialize the constraint<br>set to one, available in the current context, such that the<br>specialized constraint does not contain unreachable type variables. <br>

(A formal definition, with full details, is in the cited SBLP&#39;09 paper.)<br><br>Consider, in Example 1, that we have a single instance of F and<br>O, say:<br><br>instance F Bool Bool where f = not <br>instance O Bool where o = True <br>

<br>and consider also that &quot;k&quot; is used as in e.g.:<br><br>   kb = not k<br><br>According to our proposal, kb is well-typed. Its type is Bool. This<br>occurs because (F a b, O a)=&gt;Bool can be simplified to Bool, since<br>

there exists a single substitution that unifies the constraints with<br>instances (F Bool Bool) and (O Bool) available in the current context,<br>namely S = (a|-&gt;Bool,b|-&gt;Bool). <br><br>As another example (Example 2), consider:<br>

<br>{-# NoMonomorphismRestriction, MultiParameterTypeClasses #-}<br>data Matrix = ...<br>data Vector = ...<br>class Mult a b c where (*):: a ! b ! c<br>instance Mult Matrix Vector Matrix where (*) = ...<br>instance Mult Matrix Vector Vector where (*) = ...<br>

m1:: Matrix = ...<br>m2:: Vector = ...<br>m3:: Vector = ...<br>m = (m1 * m2) * m3<br><br>GHC gives the following type to m: <br>  m :: forall a, b. (Mult Matrix Vector a, Mult a Vector b) =&gt; b<br><br>However, &quot;m&quot; cannot be used effectively in a program compiled with<br>

GHC: if we annotate m::Matrix, a type error is reported. This occurs<br>because the type inferred for &quot;m&quot; includes constraints (Mult Matrix<br>Vector a, Mult a Vector Matrix) and, with b|-&gt;Matrix, type variable &quot;a&quot;<br>

appears only in the constraint set, and this type is considered<br>ambiguous. Similarly, if &quot;m&quot; is annotated with type Vector, the type<br>is also considered ambiguous. There is no means of specializing type<br>

variable &quot;a&quot; occurring in the type of &quot;m&quot; to Matrix. And no FD may be<br>used in order to achieve such specialization, because we do not have<br>here a FD: &quot;a&quot; and &quot;b&quot; do not determine &quot;c&quot; in class Mult: for (a,b =<br>

Matrix,Vector), we can have &quot;c&quot; equal to either Matrix or Vector.<br><br>According to our proposal, type m:: forall a. (Mult Matrix Vector a,<br>Mult a Vector Matrix)) =&gt; Matrix is not ambiguous, in the context of<br>

the class and instance declarations of Example 2 (since &quot;a&quot; can be<br>instantiated to Matrix), whereas type m:: forall a.(Mult Matrix Vector<br>a, Mult a Vector Matrix)) =&gt; Vector is ambiguous in this context.<br>

<br>We would like to encourage compiler front-end developers to change<br>Haskell&#39;s ambiguity rule, and test with as many examples as desired,<br>including recurring examples that appear in Haskell mailing lists<br>involving MPTCs, FDs etc. We would like to hear and discuss your<br>

doubts, opinions, comments, criticisms etc.<br><br>Cheers,<br><font color="#888888"><br>Carlos<br><br>
</font><br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br>