Efficient Inference of Partial Types

Partial types for the -calculus were introduced by Thatte in 1988 [3] as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. In that paper he showed that type inference for partial types was semidecidable. Decidability remained open until quite recently, when O'Keefe and Wand [2] gave an exponential time algorithm for type inference. In this paper we give an O(n3) algorithm. Our algorithm constructs a certain finite automaton that represents a canonical solution to a given set of type constraints. Moreover, the construction works equally well for recursive types; this solves an open problem stated in [2]. Supported by the Danish Research Academy, the National Science Foundation, and the John Simon Guggenheim Foundation. On sabbatical from: Computer Science Department, Cornell University, Ithaca, New York 14853, USA. 1 

• Type: Conference
• Year: 1992
• Where: FOCS
• Authors: Dexter Kozen, Jens Palsberg, Michael I. Schwartzbach
• Keywords: Exponential Time Algorithm, FOCS 1992, Partial Types, Theoretical Computer Science, Type Inference