Principal Typing for Intersection Types, Forty-Five Years Later

TL;DR

This paper revisits classical intersection type systems to provide a clearer, more accessible formulation of principal typings, introducing elementary operations and a semi-algorithm for strongly normalizing terms, enhancing understanding of type inference in lambda calculus.

Contribution

It offers a simplified, more accessible approach to principal typings in intersection type systems, with a semi-algorithm for strongly normalizing terms based on elementary operations.

Findings

Identifies three elementary operations for type derivations

Designs a semi-algorithm for principal typings of strongly normalizing terms

Provides a modern, accessible perspective on classical results

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