Type Inference with Inequalities

Type inference can be phrased as constraint-solving over types. We consider an implicitly typed language equipped with recursive types, multiple inheritance, 1st order parametric polymorphism, and assignments. Type correctness is expressed as satisfiability of a possibly infinite collection of (monotonic) inequalities on the types of variables and expressions. A general result about systems of inequalities over semilattices yields a solvable form. We distinguish between deciding typability (the existence of solutions) and type inference (the computation of a minimal solution). In our case, both can be solved by means of nondeterministic finite automata; unusually, the two problems have different complexities: polynomial vs. exponential time.

• Type: Conference
• Year: 1991
• Where: TAPSOFT
• Authors: Michael I. Schwartzbach
• Keywords: Nondeterministic finite Automata, Order Parametric Polymorphism, Software Engineering, TAPSOFT 1991, Type Inference