Re: [Caml-list] Type indexed types?

[skaller <skaller@users.sourceforge.net>]

On Wed, 2005-01-26 at 04:01, skaller wrote:
> On Tue, 2005-01-25 at 23:28, Jim Farrand wrote:

> > Note that I already have a function which can compute if type a is a
> > specialisation of type b.

The algorithm I have requires a comparison with 4 possible
results: less, greater, equal or incomparable. You can
derive that from just less-equal:

	match a <= b, b <= a with
	| true, true -> Equal
	| true, false -> Less
	| false, true -> Greater
	| false, false -> Incomparable

Unfortunately this requires two unification steps.
To use you own comment "There must be a better way" but
I don't know what it is.

BTW: I obtain this result by adding a constraint
to the unification algorithm that it only permits
equations of the form:

	'a = t

in the MGU, where 'a is a variable taken from the LHS of the
input equation (there is only a single equation when 
you're measuring 'less')

This is essential matching an function argument against a 
function signature (we want to reduce the signature to make
it equal to the argument).

However, when we're trying to order all the match
candidates, it would be nicer to get one of the
above four results in one unification step.

However it just won't work for an arbitrary MGU,
which might have the LHS variables coming from
either side of the equation. This can happen
if you get matching type variables. Unfortunately,
you can't just pick the LHS one every time,
since after substitution, an RHS variable
can end uo on the LHS .. :(

So I'd like to know if there is a better way to calculate
the four value partial ordering relation between two types
than two comparisons for less.. any hints?

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net