Satisfiability and ambiguity
Carlos Camarão
camarao@dcc.ufmg.br
Tue, 25 Sep 2001 14:28:46 -0400 (PYT)
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 .