Title: Inferring Intersection Typings that Are Equivalent to Call-by-Name and Call-by-Value Evaluations.
Authors: Adam Bakewell, Sebastien Carlier, A.J. Kfoury, J.B. Wells
Date: April 9, 2005
Abstract:
We present a procedure to infer a typing for an arbitrary lambda-term
M in an intersection-type system that translates into exactly the
call-by-name (resp., call-by-value) evaluation of M. Our framework is
the recently developed System E which augments intersection types with
expansion variables. The inferred typing for M is obtained by setting
up a unification problem involving both type variables and expansion
variables, which we solve with a confluent rewrite system. The
inference procedure is compositional in the sense that typings for
different program components can be inferred in any order, and without
knowledge of the definition of other program components. Using
expansion variables lets us achieve a compositional inference
procedure easily. Termination of the procedure is generally
undecidable. The procedure terminates and returns a typing iff the
input M is normalizing according to call-by-name (resp.,
call-by-value). The inferred typing is exact in the sense that the
exact call-by-name (resp., call-by-value) behaviour of M can be
obtained by a (polynomial) transformation of the typing. The inferred
typing is also principal in the sense that any other typing that
translates the call-by-name (resp., call-by-value) evaluation of M can
be obtained from the inferred typing for M using a substitution-based
transformation.