jonwa@ida.liu.se (Jonas Wallgren) (09/18/90)
What is unification?
How would you describe or explain unification in a simple way, with as few
technicalities as possible?
Is "equation solving" a good candidate?
Well, what do you mean by equation solving?
Does it have to result in a number of variable bindings (a unifier)?
Or could I say that a=b is solved if I can construct a c that is the result of
trying to get a and b equal?
My specific problem has to do with types:
If I have a=int and b=X (a type variable) I can solve a=b by letting
X=int and substitute that on both sides to get int=int.
But if I also allow sum types (e.g. overloading) I could have
a=int and b=bool and then solve a=b by saying that the resulting
type c should be int+bool.
Would you call this equation solving? Would you call it unification?
If not, what would you call it?
-------------------------------------------------------------------------------
Jonas Wallgren | jwc@ida.liu.se
Department of Computer and Information Science |
Linkoping University |-------------------------------
SE-581 83 Linkoping |
Sweden |(\x.xx)(\x.x):(forall a.(a->a))
-------------------------------------------------------------------------------