[TYPES] Paper: Polymorphic Typed Defunctionalization and Other Tales

[Francois Pottier]

Dear all,

Nadji Gauthier and I would like to announce the availability of the following
draft paper, which has been submitted to HOSC. This is the journal version of
our POPL'04 paper, with some extra material (see third paragraph of abstract
below). Comments and suggestions warmly welcomed!

  Title:
  Polymorphic Typed Defunctionalization and Other Tales

  URL:
  http://pauillac.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf

  Abstract:
  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 Hindley and Milner's 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.

  We also suggest that the principle of defunctionalization can be applied to
  eliminate constructs other than functions. To illustrate this point, we define
  two new type-preserving transformations. One eliminates Rémy-style polymorphic
  records by translating them down to guarded algebraic data types and basic
  records. The other eliminates the dictionary records introduced by the
  standard compilation scheme for Haskell's type classes. This yields a new
  type-preserving compilation scheme for type classes, whose target type system
  is an extension of Hindley and Milner's discipline with polymorphic recursion
  and guarded algebraic data types.

-- 
François Pottier
Francois.Pottier at inria.fr
http://pauillac.inria.fr/~fpottier/