Folks,
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 = 0
instance F a b => F [a] [b] where f [x] [y] = f x y
g x y = (f [x] y) + (f y [x])
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),
where P is the set of constraints and t is the simple type,
the rule for nonambiguity should be
P = P |* tv (t,G)
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 = F a b and t = a
We have that: P => t is not ambiguous
Since: P |* {a} = 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.
[2] Type Inference for Overloading, Carlos Camarão and Lucília
Figueiredo, Technical report UFMG, available at
http://www.dcc.ufmg.br/~camarao/jfp-ct.ps.gz.
[3] Overloading and Coherence, Carlos Camarão and Lucília Figueiredo,
Technical report UFMG, available at
http://www.dcc.ufmg.br/~camarao/overloading-and-coherence.ps.gz .
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
