Type inference with partial types

Abstract

This paper introduces a new form of type expressions which represent partial type information. These expressions are meant to capture the type information statically derivable from heterogeneous objects. The new monotypes form a lattice of subtypes and require type inference based on inclusion constraints. We discuss the existence and form of principle types under this extension and present a semi-decision procedure for the well-typing problem which can be restricted to a form that terminates for most practical programs. The partial type information derivable for heterogeneous entities is not sufficient to guarantee type-correctness for many of their uses. We therefore introduce a notion of statically generated dynamic type checks. Finally, all these elements are pulled together to sketch the derivation of a static system for "plausibility checking" which identifies the applications which may require a dynamic check and catches many type errors.