[m-dev.] diff: "superclass search"

[Fergus Henderson]

On 05-May-1998, David Glen JEFFERY <dgj at cs.mu.OZ.AU> wrote:
> Re-implement the part of context reduction which seeks to eliminate a
> typeclass constraint by using the fact that one class is a superclass of 
> another.

> +eliminate_constraint_by_class_rules(C, DeclaredConstraints, SuperClassTable,
> +		TVarSet, Proofs0, Proofs) :-
...
> +	(
> +			% Do the first level of search
> +		FindSub = lambda([TheConstraint::in] is semidet,(

I suggest s/,)/, )/

> +			list__member(TheConstraint, DeclaredConstraints)
>  		)),
> +		list__filter(FindSub, SubClassConstraints, [Sub|_])
> +	->
> +		map__set(Proofs0, C, superclass(Sub), Proofs)
>  	;
> +			% Recursively search the rest of the superclass
> +			% relation.
> +		SubClassSearch = lambda([Constraint::in, CnstrtAndProof::out] 
> +				is semidet, (
> +			eliminate_constraint_by_class_rules(Constraint,
> +				DeclaredConstraints, SuperClassTable,
> +				TVarSet, Proofs0, SubProofs),
> +			CnstrtAndProof = Constraint - SubProofs
> +		)),
> +			% XXX this could (and should) be more efficient. 
> +			% (ie. by manually doing a "cut").
> +		list__filter_map(SubClassSearch, SubClassConstraints,
> +			[NewSub - NewProofs|_]),
> +		map__set(NewProofs, C, superclass(NewSub), Proofs)
> +	).

I'd like to see a proof of termination for this algorithm.
I think it won't terminate in the case where the class
hierarchy is cyclic, and I think we currently don't check
whether the class hierarchy is cyclic.

If case like this

	:- typeclass c1(T) <= c2(T) where [].
	:- typeclass c2(T) <= c1(T) where [].

were the only ones we had to worry about, modifying
the algorithm so that it always terminates would be
pretty easy.  But we also need to worry about cases
like this:

	:- typeclass c3(T) <= c4(list(T)) where [].
	:- typeclass c4(T) <= c3(list(T)) where [].

There's no way you could write any instance declaration
that would satisfy these (since any such instance
declaration would require the prior existence of an
infinite set of ancestor instance declarations),
so this would not be a useful declaration,
but the type checker still needs to terminate if
someone writes something like that by mistake.

Thus the simplest thing to do is probably to check
for cyclic class hierarchies.  I guess this could be
done in make_hlds.m when you're constructing the
subclass table.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.