Gábor Lehel
If you're referring to the NewAxioms work Simon linked to ... [snip] ... It seems vaguely similar to a paper on instance chains[2] I saw once.
Thanks Gábor for the reference, but I don't think they're very comparable. The instance chains is in context of fundeps and overlaps (as you'd expect from MPJ, since it was him who first introduced fundeps). I know fundeps are 'theoretically' equivalent to type families. But I think the instance chains paper is a good demonstration of why I find fundeps so awkward to follow at the superficial syntax level for type-level programming: - you have to look first to the end of the instance to find the head; - and assume (hope!) that the 'result' is the rightmost typevar; - then backtrack through the list of constraints; - some are only validation limits on the instance; - some are calculating intermediate results (again with their result at right). Instance chains include: - not only resolving overlaps (yes, that's similar to NewAxioms); - but also choosing instances based on type class membership; (often asked for by newbies, but really difficult to implement) - and explicit failure leading to backtracking search (Explicit failure is missing from NewAxioms. I don't mean backtracking, but at least treating certain conditions as no instance match. Oleg's HList work needs that (for example in the Lacks constraint), but has to fudge it by putting a fake instance with a fake constraint.) Does the overall instance chain structure guarantee termination of type inference? I don't follow the algebra enough to be sure. Morris & Jones' examples seem to me contrived: they've set up overlapping instances where you could avoid them, and even where they seem harder to follow. Yes, their solution is simpler than the problem they start with; but no, the problem didn't need to be that complex in the first case. (I'm looking especially at the GCD/Subt/Lte example -- I think I could get that to work in Hugs with fundeps and no overlaps.) I'm surprised there isn't a Monad Transformer example: [3] by MPJ uses overlaps for MonadT. And MonadT was (I thought) what gave all the trouble with overlaps and default instances and silently changing behaviour. (There's a brief example in Morris' supporting survey - ref [11] in [2].) Anybody out there can explain further? AntC
doi=10.1.1.170.9113&rep=rep1&type=pdf
[3] Functional Programming with Overloading and Higher-Order Polymorphism Mark P. Jones, 1995