On 28 Aug 2003, Carl Witty wrote:
On Thu, 2003-08-28 at 13:10, Brandon Michael Moore wrote:
Unfortunately I don't have a useful syntatic condition on instance declarations that insures termination of typechecking. If types are restriced to products, sums, and explicit recursion, then termination is ensured if we restrict the assumtions of a declaration to instances for subexpressions of the type we are declaring an instance for (there are only a finite number of subexpressions times a finite number of classes, and one is added each time we apply a rule). I haven't made any progress if type operators are allowed, and I don't have any simple check whether a Haskell type expression can be represented without type operators. I was hoping to get normalization of type expressions from the simple kinding, but recursive operator definitions break that. Rather, regularity of the resulting types, or something like that. We can always evaluate a type expression to head normal form, but the complete expansion of a type can be irregular.
I think some of David McAllester's papers from about 1990-1994 may be relevant here. He has several papers on deciding when sets of inference rules are terminating, or terminating in polynomial time. (He applies this in the context of automated theorem proving, but it should apply perfectly well to type class inference as well.)
Thanks, this is interesting work. I've read "New Results on Local Inference Relations", and skimmed a few other papers. Too bad I can't see how to use it. Determining locality seemed to require a global analysis, and superficial rules look too restrictive for instance declarations. Some of the ideas could probably be adapted to prove termination (and bounds) for sets of rules if the anteceedents of rules mention only subterms of the conclusion. It's pretty trivial to prove that regular terms have regular derivations if any, but I haven't looked for good bounds. It looked to me like most of the results assumed that terms were finite, but most of it should carry over to regular terms. I don't think it would be easy to extend to irregular terms, even if I had a good characterication of Haskell types. Does anyone know of any results in that direction? Simple kinds give you head normalization, but I don't know how to describe the sorts of terms that end up as constructor arguments as you evaluate type expressions. I want some reasonable characterization of the sort of trees you get when you evaluate type expressions completely. Does anyone know of papers or books on this? Thanks Brandon