# unify a list of constraints:
# - input = list of constraints of the form "lhs==rhs"
# - output = list of constraints
# a unification is an assignment of values to variable that satisfies
# the constraints in the most general way. in our case, variables
# are the PolymorphicType guys, and values are any Types
def unify( constraints ):
return [] if constraints is an empty list;
(lhs,rhs) = shift constraints;
## if they are already equal, do nothing
if lhs = rhs then
return unify(constraints);
## orient "variables" on the lhs
if lhs is not a PolymorphicType, but rhs is, then
(lhs,rhs) = (rhs,lhs);
if lhs = PolymorphicType(id) then
if PolymorphicType(id) occurs anywhere within constraints, then
croak "you're asking for a recursive type!"
constraints = map { replace each PolymorphicType(id)
with rhs } constraints;
## output this assignment as part of the solution!
return "id:rhs" + unify(constraints);
## for 2 FuncTypes to be equal, their components must be equal,
## so add new constraints
if lhs = FuncType(l1,l2) and rhs = FuncType(r1,r2) then
return unify(constraints + "l1==r1" + "l2==r2");
if lhs = ListType(l1) and rhs = ListType(r1) then
return unify(constraints + "l1==r1");
## we get here if you try to constrain a ListType to equal a
## FuncType, or other such impossible feats
else
croak "unification impossible!";