Sébastien Carlier and J. B. Wells
Type inference with expansion variables
and intersection types in System E and an exact correspondence with
beta-reduction
Technical Report HW-MACS-TR-0012, Heriot-Watt Univ., School of Math. & Comput. Sci., January 2004
Completely superseded by [50]
System E is a recently designed type system for the
lambda-calculus with intersection types and
expansion variables. During automatic type
inference, expansion variables allow postponing
decisions about which non-syntax-driven typing rules
to use until the right information is available and
allow the choices to be implemented via
substitution.
This paper shows how expansion variables enable a
unification-based automatic type inference algorithm
for System E that finds a typing for every
beta-normalizable lambda-term. We have
implemented and tested our algorithm and made our
implementation publicly available. We show that each
step of our unification algorithm corresponds to
exactly one beta-reduction step, and vice
versa. This formally verifies and makes precise a
correspondence between type inference and
beta-reduction that before was only known
informally at an intuitive level and only among
those who work with intersection types.
[ bib ]
Back
This file has been generated by
bibtex2html 1.43