Polymorphic typed defunctionalization

François Pottier, Nadji Gauthier

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


Defunctionalization is a program transformation that aims to turn a higher-order functional program into a first-order one, that is, to eliminate the use of functions as first-class values. Its purpose is thus identical to that of closure conversion. It differs from closure conversion, however, by storing a tag, instead of a code pointer, within every closure. Defunctionalization has been used both as a reasoning tool and as a compilation technique. Defunctionalization is commonly defined and studied in the setting of a simply-typed lambda-calculus, where it is shown that semantics and well-typedness are preserved. It has been observed that, in the setting of a polymorphic type system, such as ML or System F, defunctionalization is not type-preserving. In this paper, we show that extending System F with "guarded algebraic data types" allows recovering type preservation. This result allows adding defunctionalization to the toolbox of type-preserving compiler writers.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems