Type Inference with Expansion Variables and Intersection Types in System E and an Exact Correspondence with Beta-Reduction
Sebastien Carlier, J.B. Wells
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.