Simple, Decidable Type Inference with Subtyping
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.
Cite
@article{arxiv.1104.3116,
title = {Simple, Decidable Type Inference with Subtyping},
author = {Eli Gottlieb},
journal= {arXiv preprint arXiv:1104.3116},
year = {2013}
}
Comments
This paper has been withdrawn, due to abundant errors in this version of the paper, and due to ongoing efforts to improve the paper and bring it to real publication