Proposal to solve Haskell's MPTC dilemma

[Carlos Camarao]

This message, sent a few days ago to haskell-cafe, 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
discussion in haskell-cafe started well, involving a discussion
related to module fragility (changes to type-correctness after a
change in imported modules) but it is now quiet. Since there may be
members of this list not in haskel-cafe, and because I'd like to hear
your opinions and discuss the proposal here, as well as encourage the
proposal's implementation, I am sending the message to this list also.

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

The dilemma is well-known (see e.g.
hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClassesDilemma).

www.haskell.org/ghc/dist/current/docs/html/users_guide/type-class-extensions.html
presents a solution to the termination problem related to the
introduction of MPTCs in Haskell. Neither FDs (functional
dependencies) nor any other mechanism like ATs (associated types) are
needed in our proposal, in order to introduce MPTCs in Haskell; the
only change 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 web page above.

Let us review the ambiguity rules used in Haskell-98 and in GHC.
Haskell-98 ambiguity rule, adequate for single parameter type classes,
is: a type C => T is ambiguous iff there is a type variable that
occurs in C (the "context", or constraint set) but not in T (the
simple, unconstrained type).

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:: (F a b,O a) => b

Type forall a b. (F 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 (F a b, O a)=>b
above is reachable, because it appears in (F 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.

What do you think?

Cheers,

Carlos
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20100526/9c2a0e36/attachment.html