Sébastien Carlier and J. B. Wells
Expansion: the crucial mechanism for type inference with intersection types:
A survey and explanation
In Proc. 3rd Int'l Workshop Intersection Types & Related
Systems (ITRS 2004), pages 173-202, 2005
The ITRS '04 proceedings appears as vol. 136 (2005-07-19) of
Elec. Notes in Theoret. Comp. Sci.
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.
[ bib |
http |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43