unification of alternatives
 skaller
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20060313 (08:40) 
From:  skaller <skaller@u...> 
Subject:  unification of alternatives 
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