The issue of defunctionalization with type preservation is addressed in this paper. Defunctionalization is a program transformation that turns a higher-order functional program into a first-order functional program (with no functions as first-order values). The purpose of this transformation is similar to that of closure conversion, but it differs by storing a tag instead of a code pointer within every closure. Defunctionalization serves both as a reasoning tool and as a compilation technique.

Defunctionalization is defined and studied most commonly in the setting of a simply typed lambda-calculus, where semantics and well typedness are preserved. With polymorphic type systems, as in ML or System F, defunctionalization is not type-preserving. The authors extend System F with guarded algebraic data types to preserve types.

The problem with defining defunctionalization for a typed-polymorphic lambda-calculus lies in the definition of “apply” that simulates the application of a source function to a source value, then returning its result. The main contribution of this paper is its proof that defunctionalization may be viewed as a type-preserving transformation from System F, as extended with guarded algebraic data types, into itself. Also noted is a similar process that can be applied to ML. Another contribution of this paper is its proof that the transformation is meaning-preserving in an untyped setting; this result can then be lifted to the typed setting.

After a carefully prepared introduction, the second section defines the extension of System F with guarded algebraic data types. The third section defines the defunctionalization of well-typed programs, and the fourth section includes a proof that defunctionalization of untyped programs preserves well typedness. The fifth section defines the defunctionalization of untyped programs, and includes a proof of meaning preservation, which also carries over to typed programs. The last section contains closing remarks.

The authors’ version of defunctionalization does not address optimization or a sophisticated treatment of multiple-argument functions, but it does broaden the case for defunctionalization as a compilation technique, and as a tool to help programmers transform programs and reason about them. The paper is rigorous, well written, and includes sufficient detail to satisfy functional language theorists.