the MPTC Dilemma (please solve)

[Claus Reinke]

> <Hand-waving-alert>
>        However, the evaluation model is what is known as "residuation"
>        in the FL community, which is essentially functional programming
>        with logic variables and lenient evaluation (a la Id).  As long
>        as we only have strongly normalising functions, lenient
>        evaluation and lazy evaluation coincide.  So, for Haskell
>        programmers, we are on familiar ground.
> </Hand-waving-alert>

now that is an interesting difference. but we don't need to change
formalizations to achieve that - apart from the difficulty of comparing
the different properties of ATS and FDs if the formalisms also differ,
there is the issue of implementation. if, instead of requiring completely
new tools, ATS can be explained and implemented as a restricted
form of FDs, with nicer syntax, then the existing FD implementations
can be used - no need to add yet another layer of complexity to
the type system implementations.

first, syntax. at the level of type-classes, we are dealing with a simple
first-order language, so adding nested expressions via function calls
does not change expressiveness - we can simply reserve the last 
class parameter for results, and allow that to be omitted in calls.
nested expresssions "F (G x) => C x" can be flattend as 
"G x r,F r => C x", with an FD for G (x->r).

next, semantics. (simplifying slightly,) the difference between 
narrowing and residuation is that the former may instantiate 
variables, the latter suspends decisions that depend on variable 
instantiations, so narrowing subsumes residuation. you do have 
semantic unification in ATS, so you do have unification as a 
special case. so if you really avoid variable instantiations in 
ATS, that means at least:

- not having an explicit result parameter
    (ATS writes the result parameter as an associated type)

- not permitting equations involving variable instantiations
    (ATS has equality constraints, but one must not be able 
     to write G x = r, or else one gets explicit access to a 
     variable to be instantiated with a result, which we could
     feed back as input into the semantic unification)

- not permitting repeated variables in instance heads
    (otherwise one could define an instance implicitly needing
     unification, thereby circumventing the second restriction)

[I don't recall seeing the last two restrictions in ATS papers;
 have I missed them? they may be implicit in the restricted
 subset of the language formalized, but they need to be made
 explicit if ATS are to be integrated into current Haskell]

right so far? the first is the least of our worries: if we flatten
nested calls, and do not permit any calls involving the result/
range parameter, there is no way to refer to the result/range
parameters explicitly. if we also add the other two restrictions,
the narrowing semantics will behave much like the residuation
semantics (the only variables ever instantiated are range/result
variables, and that only puts a type in place of the call).

so it seems that one might use the existing machinery (both
formalization/theory and implemenation) for ATS as well,
just by adding flattening of nested calls plus restrictions 
that ensure a single, full FD per class, and no explicit 
references to result/range variables.

does this make any sense?-)

cheers,
claus