Type class problem

[Brandon Michael Moore]

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