Principal Typing for Intersection Types, Forty-Five Years Later

TL;DR

This work revisits some classical notions, and identifies three elementary operations that allow to build any type derivation in a system characterizing head normalization, and uses such operations in the design of an inference semi-algorithm that computes the principal typing of all and only the strongly normalizing terms.

Abstract

A type assignment system for lambda-calculus enjoys the principal typing property if every typable term M has a special typing, called principal, from which all typings for M can be obtained via suitable operations. The existence of principal typings in various intersection type disciplines has long been established using both semantical and syntactical approaches. Historically, on the syntactical side, proofs of this property and the description of type inference (semi-)algorithms computing principal typings have been complicated by many subtle technicalities; the present work aims at providing a more accessible formulation. To this end, we revisit some classical notions, and identify three elementary operations (substitution, expansion, erasure) that allow to build any type derivation in a system characterizing head normalization. We then use such operations in the design of an inference semi-algorithm that computes the principal typing of all and only the strongly normalizing terms, thus contributing to a modern perspective on results originally proven more than 40 years ago

Figures (2)

• Figure 1: Pseudo-derivation rules for system ${\mathcal{N}}$.
• Figure 2: Unification rules for intersection pre-types.

Theorems & Definitions (50)

• Definition 1
• Definition 2
• Theorem 3: Subject Reduction/Expansion
• Theorem 4: Characterization
• Remark 1
• Definition 5: Pseudo-derivations for ${\mathcal{N}}$
• Definition 6
• Definition 8
• Definition 11: Expansion, Erasure
• Definition 12