What Are Principal Typings and What Are They Good for?

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. Keywords: Polymorphic recursion, separate compilation, incremental type inference, error messages, intersection types. 1 Introduction We would like to make a careful distinction between the following two properties of type systems. Property A Given: a term M typable in type environment A. There ex..