The Algebra of Expansion

Issue title: Intersection Types and Related Systems (ITRS)

Article type: Research Article

Authors: Carlier, Sébastien | Wells, J.B.

Affiliations: Heriot-Watt University, School of Mathematical and Computing Sciences, Edinburgh, Scotland

Note: [] Address for correspondence: http://www.macs.hw.ac.uk/~jbw/

Abstract: Expansion is an operation on typings (pairs of type environments and result types) in type systems for the λ-calculus. Expansion was originally introduced for calculating possible typings of a λ-term in systems with intersection types. This paper aims to clarify expansion and make it more accessible to a wider community by isolating the pure notion of expansion on its own, independent of type systems and types, and thereby make it easier for non-specialists to obtain type inference with flexible precision by making use of theory and techniques that were originally developed for intersection types. We redefine expansion as a simple algebra on terms with variables, substitutions, composition, and miscellaneous constructors such that the algebra satisfies 8 simple axioms and axiom schemas: the 3 standard axioms of a monoid, 4 standard axioms or axiom schemas of substitutions (including one that corresponds to the usual “substitution lemma” that composes substitutions), and 1 very simple axiom schema for expansion itself. Many of the results on the algebra have also been formally checked with the Coq proof assistant. We then take System E, a λ-calculus type system with intersection types and expansion variables, and redefine it using the expansion algebra, thereby demonstrating how a single uniform notion of expansion can operate on both typings and proofs. Because we present a simplified version of System E omitting many features, this may be independently useful for those seeking an easier-to-comprehend version.

DOI: 10.3233/FI-2012-771

Journal: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 43-82, 2012