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.
|Number of pages||30|
|Journal||Electronic Notes in Theoretical Computer Science|
|Publication status||Published - 19 Jul 2005|
|Event||Proceedings of the third International Workshop on intersection Types and Related Systems - |
Duration: 13 Jul 2004 → 13 Jul 2004
- Intersection types
- Type inference