Simple, Decidable Type Inference with Subtyping

TL;DR

This paper presents a decidable, annotation-free type inference method for ML-like languages that handles subtyping and semi-unification, demonstrated through encoding Featherweight Java.

Contribution

It introduces a novel lattice-based type inference algorithm that is both complete and terminates, solving a broad class of semi-unification problems.

Findings

Algorithm is terminating and complete

No type annotations or proof obligations required

Successfully encodes Featherweight Java types

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.