This message, sent a few days ago to haskell-cafe, presents,<br>informally, a proposal to solve Haskell&#39;s MPTC (multi-parameter type<br>class) dilemma.† If this informal proposal turns out to be acceptable,<br>we (I am a volunteer) can proceed and make a concrete proposal. The<br>
discussion in haskell-cafe started well, involving a discussion<br>related to module fragility (changes to type-correctness after a<br>change in imported modules) but it is now quiet. Since there may be<br>members of this list not in haskel-cafe, and because I&#39;d like to hear<br>
your opinions and discuss the proposal here, as well as encourage the<br>proposal&#39;s implementation, I am sending the message to this list also.<br><br>The proposal has been published in the SBLP&#39;2009 proceedings and is<br>
available at <a href="http://www.dcc.ufmg.br/~camarao/CT/solution-to-mptc-dilemma.pdf">www.dcc.ufmg.br/~camarao/CT/solution-to-mptc-dilemma.pdf</a><br><br>The dilemma is well-known (see e.g.<br><a href="http://hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClassesDilemma">hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClassesDilemma</a>).<br>
<br><a href="http://www.haskell.org/ghc/dist/current/docs/html/users_guide/type-class-extensions.html">www.haskell.org/ghc/dist/current/docs/html/users_guide/type-class-extensions.html</a><br>presents a solution to the termination problem related to the<br>
introduction of MPTCs in Haskell. Neither FDs (functional<br>dependencies) nor any other mechanism like ATs (associated types) are<br>needed in our proposal, in order to introduce MPTCs in Haskell; the<br>only change is in the ambiguity rule. This is explained below. The<br>
termination problem is essentially ortogonal and can be dealt with,<br>with minor changes, as described in the web page above.<br><br>Let us review the ambiguity rules used in Haskell-98 and in GHC.<br>Haskell-98 ambiguity rule, adequate for single parameter type classes,<br>
is: a type C =&gt; T is ambiguous iff there is a type variable that<br>occurs in C (the &quot;context&quot;, or constraint set) but not in T (the<br>simple, unconstrained type).<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:: (F a b,O a) =&gt; b<br><br>Type forall a b. (F 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;<br>† type. ...† Each universally quantified type variable tvi must be<br>
† reachable from type.† A type variable a is reachable if it appears<br>† in the same constraint as either a type variable free in the type,<br>† or another reachable type variable.&quot;<br><br>For example, type variable &quot;a&quot; in constraint (O a) in (F a b, O a)=&gt;b<br>
above is reachable, because it appears in (F 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>What do you think?<br><br>Cheers,<br><br>Carlos<br><font color="#888888"><br></font>