Has anyone written an efficient purely-functional implementation of unification (for type checking)? If not, what makes it difficult to solve the problem in that way? David Feuer This message has been brought to you by the letter alpha and the number pi.