Type Inference with Inequalities
DOI:
https://doi.org/10.7146/dpb.v19i336.6566Abstract
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.Downloads
Published
1990-10-01
How to Cite
Schwartzbach, M. I. (1990). Type Inference with Inequalities. DAIMI Report Series, 19(336). https://doi.org/10.7146/dpb.v19i336.6566
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.