Satisfiability and ambiguity

[Carlos Camarão]

Folks,=20

I have recently been referred to a paper by Duggan and Ophel, about
"Type-checking Multi-parameter type classes" [1]. I think it will be
useful to consider the following.

----------------------------------------------------------------------
1. "Domain-driven unifying overload resolution" (DDUOR, so-called in
definition 4.1 in [1]) should not fail to terminate;
i.e. satisfiability is not undecidable (see system CT [2]). DDUOR
should consider the *set* of constraints (in C, in def. 4.1), instead
of one after another, for finding unifying substitions (\theta'' in
def. 4.1).

For the example (page 17 of [1]):

   class    F a   b              where f:: a -> b -> Int
   instance F Int Float          where f   x    y  =3D 0
   instance F a   b =3D> F [a] [b] where f  [x]  [y] =3D f x y

   g x y =3D (f [x] y) + (f y [x])
 =20
the definition of g will be detected as erroneous (not well-typed) if
the *set* of constraints is considered for finding the unifying
substitution, instead of one constraint after another. In this way,
DDUOR terminates.

I think full details will not be needed, but this can be (easily)
understood by reading/following the definition of sats in system CT.

--------------------------------------------------------------------
2. The usefulness of multi-parameter type classes has been hindered by
the restrictiveness of the rule for detecting ambiguity. Instead of
   tv(P) \subseteq tv(t),=20
where P is the set of constraints and t is the simple type,=20
the rule for nonambiguity should be=20
   P =3D P |* tv (t,G)=20

where |* denotes "constraint projection" and G the typing context. For
the definition of |* see [3]; the idea is to include constraints that
have type variables in t and G and constraints that have type
variables previously included. In the example:

 For:            P =3D F a b  and  t =3D a=20
 We have that:   P =3D> t is not ambiguous
 Since:          P |* {a} =3D P

This rule would allow multi-parameter type classes to be used in
(well-known) compelling examples, without giving rise to ambiguities.

Carlos

[1] Type-checking multi-parameter type classes, Dominic Duggan and
John Ophel, to appear in JFP.=20

[2] Type Inference for Overloading, Carlos Camar=E3o and Luc=EDlia
Figueiredo, Technical report UFMG, available at
http://www.dcc.ufmg.br/~camarao/jfp-ct.ps.gz.=20

[3] Overloading and Coherence, Carlos Camar=E3o and Luc=EDlia Figueired=
o,
Technical report UFMG, available at=20
http://www.dcc.ufmg.br/~camarao/overloading-and-coherence.ps.gz .