unification of alternatives

unification of alternatives

[skaller]

I have an interesting problem with unification algorithm.
The problem is basically that given two terms,
either that unify, they don't unify, or *NEW* they don't
unify yet but might later.

Does anyone know how to modify the algorithm to account
for this?

It's hard for me to give a formal description, so I'll
illustrate with an example. I have a term

	typematch t with
	| t1 => t1'
	| t2 => t2'
	..
	endmatch

The reduction rule for this term is:

(a) if t is t1, return t1'
(b) if t cannot unify with t1, return

	reduce (typematch t with | t2 => t2' .. endmatch)

In other words throw out the first branch and try again.

(c) Otherwise return the whole term.
 
The indeterminism arises whenever there are type variables
present which may be replaced later on. Since we don't
know what substitutions will occur yet, we have no choice
but to delay reduction. Whilst this is probably not as
general as one may like it is actually very useful:


typedef fast_sints = typesetof (tiny, short, int, long, vlong);
...

// C integer promotion rule
typedef fun integral_promotion: TYPE -> TYPE =
  | tiny => int
  | utiny => int
  | short => int
  ...

typedef fun arithmax(l: TYPE, r: TYPE): TYPE =>
  typematch integral_promotion l, integral_promotion r with
  | vlong,vlong => vlong 
  ...

  fun add[t1:fast_ints, t2:fast_ints]: t1 * t2 -> arithmax(t1,t1)="$1
+$2";

The last rule here allows mixed mode arithmetic in Felix
to model the usual C rules .. without allowing any implicit
conversions. The typesetof operator converts a type tuple
into a set of types. The notation:

	t1:fast_ints

is constrained genericity. Basically, the overload resolution
algorithm uses unification to find the type variables,
then then constraints are checked. Unfortunately that
isn't good enough. Consider this case:

fun g[t,u:ptr[t]]: u -> t = "*$1";
var x = 1;
var px:ptr[int] = addr x;
print$ g[int] px; endl;

This actually works, but this one does not:

print$ g px; endl;

because it isn't possible to deduce t from the argument.
I have modified the algorithm so  that this now does work,
by adding the type constraint into the set of equations
to be unified.

Ok -- sorry it took so long -- so here is the problem.
The above works fine with 'regular types'. But if the
constraint is a typeset, it doesn't work.

The obvious way to make it work is to consider each
member of the typeset in turn.. however that just
isn't tractable (combinatorial explosion).

However the regular solution WILL work in many cases
if we simply delay reduction of any typesets, in particular,
just leave any typeset constraints out of the unification
step, and just check the constraint afterwards (as before).

Of course this is a real hack, since the rule isn't recursive.
The 'proper' way to do it is to throw everything at a modified
unification algorithm. The problem is to stop the algorithm
aborting prematurely with a failure. In particular in the
original example:

fun add[t1:fast_ints, t2:fast_ints]: t1 * t2

we don't want the algorithm to fail unification, when in
fact it works just fine *without* the constraints being
thrown in.

-- 
John Skaller <skaller at users dot sourceforge dot net>
Async PL, Realtime software consultants
Checkout Felix: http://felix.sourceforge.net

Re: unification of alternatives

[Stefan Monnier]

> I have an interesting problem with unification algorithm.
> The problem is basically that given two terms,
> either that unify, they don't unify, or *NEW* they don't
> unify yet but might later.

I believe you're looking for something called "residualization" in
constraint and logic programming: if the unification algorithm can return
not just a substitution but also some residual constraints that it wasn't
able to resolve (but which may be resolvable later).


        Stefan