<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