Efficient Inference of Partial Types

Partial types for the lambda -calculus were introduced by Thatte (1988) as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. He showed that type inference for partial types was semidecidable. Decidability remained open until O'Keefe and Wand gave an exponential time algorithm for type inference. The authors give an O(n/sup 3/) algorithm. The 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. >

Authors

• Dexter Kozen
• Jens Palsberg
• Michael I. Schwartzbach

Keywords

• Inference algorithms
• Computer science
• Automata
• State Machine
• Subtree
• System Constraints
• Binary Tree
• Polynomial-time Algorithm
• Construction Algorithm
• Partial Order
• Starting State
• Boolean Variable
• Depth-first
• Graph Size
• Simple Type
• Induction Hypothesis
• Type Inference
• Mathematical Sciences
• Consequence Of The Definition
• Universal Type
• Path Tree