Polymorphic typed defunctionalization

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 -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 typepreserving. 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.

• Type: Conference
• Year: 2004
• Where: POPL
• Authors: François Pottier, Nadji Gauthier
• Keywords: Algebraic Data Types, Closure Conversion, POPL 2004, Programming Languages, Type-preserving Compiler Writers