An approach to handling polymorphic types in higher order unification

Kreuger, Per (1988) An approach to handling polymorphic types in higher order unification. [SICS Report]



The higher order unification procedure as formulated by Huet [Hu 75] unifies terms in the simple theory of types [Ch 40]. In this language types are expressed in a very weak language (no quantification, "->" being the only operator). In many applications a stronger type-system is desirable. Lambda Prolog [MN 86], e.g. uses a type system that is in some ways similar to that of ML. This type-system uses implicitly universally quantified variables in the type-expressions. It is not trivial to reformulate the higher order unification procedure for such a theory. This paper describes an implementation of the procedure that tries to overcome some of the problems encountered in such an endeavor. The basic approach taken is to let the types be an integral part of the representation of the terms to be unified. This makes it simpler to instanciate type-variables during the unification process, and to delay the unification of terms with completely unspecified types until such time as more information is gained.

Item Type:SICS Report
Additional Information:Original report number R88015.
ID Code:2532
Deposited By:Vicki Carleson
Deposited On:17 Sep 2009
Last Modified:18 Nov 2009 16:10

Repository Staff Only: item control page