This message, sent a few days ago to haskell-cafe, presents,<br>informally, a proposal to solve Haskell'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'd like to hear<br>
your opinions and discuss the proposal here, as well as encourage the<br>proposal's implementation, I am sending the message to this list also.<br><br>The proposal has been published in the SBLP'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 => T is ambiguous iff there is a type variable that<br>occurs in C (the "context", or constraint set) but not in T (the<br>simple, unconstrained type).<br><br>For example: forall a.(Show a, Read a)=>String is ambiguous, because<br>
"a" 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->b<br>
class O a where o:: a<br>and<br> k = f o:: (F a b,O a) => b<br><br>Type forall a b. (F a b,O a) => b can be considered to be not<br>ambiguos, since overloading resolution can be defined so that<br>instantiation of "b" can "determine" that "a" should also be<br>
instantiated (as FD b|->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> "GHC imposes the following restrictions on the constraints in a type<br> signature. Consider the type: forall tv1..tvn (c1, ...,cn) =><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."<br><br>For example, type variable "a" in constraint (O a) in (F a b, O a)=>b<br>
above is reachable, because it appears in (F a b) (the same constraint<br>as type variable "b", 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'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 "k" 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)=>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|->Bool,b|->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) => b<br>
<br>However, "m" 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 "m" includes constraints (Mult Matrix<br>
Vector a, Mult a Vector Matrix) and, with b|->Matrix, type variable "a"<br>appears only in the constraint set, and this type is considered<br>ambiguous. Similarly, if "m" is annotated with type Vector, the type<br>
is also considered ambiguous. There is no means of specializing type<br>variable "a" occurring in the type of "m" to Matrix. And no FD may be<br>used in order to achieve such specialization, because we do not have<br>
here a FD: "a" and "b" do not determine "c" in class Mult: for (a,b =<br>Matrix,Vector), we can have "c" 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)) => Matrix is not ambiguous, in the context of<br>the class and instance declarations of Example 2 (since "a" can be<br>instantiated to Matrix), whereas type m:: forall a.(Mult Matrix Vector<br>
a, Mult a Vector Matrix)) => Vector is ambiguous in this context.<br><br>What do you think?<br><br>Cheers,<br><br>Carlos<br><font color="#888888"><br></font>