|
|
Technical Report HW-MACS-TR-0029
| Title | Expansion: the Crucial Mechanism for Type Inference with Intersection Types: Survey and Explanation |
|---|
| Authors | Sébastien Carlier, J.B. Wells |
|---|
| Date | 2005-03-18 |
|---|
| Abstract | 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. |
|---|
| Group | ULTRA |
|---|
| Notes | |
|---|
| Download |   |
|---|
|
|
