Partial types for the lambda-calculus were introduced by Thatte in 198
8 as a means of typing objects that are not typable with simple types,
such as heterogeneous lists and persistent data. In that paper he sho
wed that type inference for partial types was semidecidable. Decidabil
ity remained open until quite recently, when O'Keefe and Wand gave an
exponential time algorithm for type inference. In this paper we give a
n O(n3) algorithm. Our algorithm constructs a certain finite automatio
n that represents a canonical solution to a given set of type constrai
nts. Moreover, the construction works equally well for recursive types
; this solves an open problem stated by O'Keefe and Wand (in ''Proceed
ings, European Symposium on Programming,'' Lect. Notes in Comput. Sci.
, Vol. 582, pp. 408-417, Springer-Verlag, New York/Berlin, 1992). (C)
1994 Academic Press, Inc.