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.
