Simple, Decidable Type Inference with Subtyping
CoRR (2011)
- arXiv: 1104.3116
Available from arxiv.org
or
Abstract
We demonstrate a method to infer polymorphically principal and subtyping-minimal types for an ML-like core language by assigning ranges within a lattice to type variables. We demonstrate the termination and completeness of this algorithm, and proceed to show that it solves a broad special-case of the generally-undecidable semi-unification problem. Our procedure requires no type annotations, leaves no subtyping constraints in the inferred types, and produces no proof obligations. We demonstrate the practical utility of our technique by showing a type-preserving encoding of Featherweight Java into the expression calculus over which we infer types.
Sign up today - FREE
Mendeley saves you time finding and organizing research. Learn more
- All your research in one place
- Add and import papers easily
- Access it anywhere, anytime
Start using Mendeley in seconds!
Readership Statistics
5 Readers on Mendeley
by Discipline
20% Engineering
by Academic Status
40% Student (Master)
20% Other Professional
20% Researcher (at a non-Academic Institution)
by Country
40% United States
20% United Kingdom
20% Denmark