What are principal typings and what are they good for?

Abstract

We demonstrate the pragmatic value of the principal typing property, a property more general than ML's principal type property, by studying a type system with principal typings. The type system is based on rank 2 intersection types and is closely related to ML. Its principal typing property provides elegant support for separate compilation, including "smartest recompilation" and incremental type inference, and for accurate type error messages. Moreover, it motivates a novel rule for typing recursive definitions that can type many examples of polymorphic recursion. Type inference remains decidable; this is surprising, since type inference for ML plus polymorphic recursion is undecidable.