Expansion: The crucial mechanism for type inference with intersection types: A survey and explanation

Sébastien Carlier, J. B. Wells

Research output: Contribution to journalArticlepeer-review

12 Citations (Scopus)


The operation of expansion on typings was introduced at the end of the 1970s by Coppo, Dezani, and Venneri for reasoning about the possible typings of a term when using intersection types. Until recently, it has remained somewhat mysterious and unfamiliar, even though it is essential for carrying out compositional type inference. The fundamental idea of expansion is to be able to calculate the effect on the final judgement of a typing derivation of inserting a use of the intersection-introduction typing rule at some (possibly deeply nested) position, without actually needing to build the new derivation. Recently, we have improved on this by introducing expansion variables (E-variables), which make the calculation straightforward and understandable. E-variables make it easy to postpone choices of which typing rules to use until later constraint solving gives enough information to allow making a good choice. Expansion can also be done for type constructors other than intersection, such as the ! of Linear Logic, and E-variables make this easy. There are no significant new technical results in this paper; instead this paper surveys and explains the technical results of a quarter of a century of work on expansion. © 2005 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)173-202
Number of pages30
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 19 Jul 2005
EventProceedings of the third International Workshop on intersection Types and Related Systems -
Duration: 13 Jul 200413 Jul 2004


  • Expansion
  • Intersection types
  • Type inference


Dive into the research topics of 'Expansion: The crucial mechanism for type inference with intersection types: A survey and explanation'. Together they form a unique fingerprint.

Cite this