Polymorphic Typed Defunctionalization

François Pottier and Nadji Gauthier, INRIA

Outline

1. Closure conversion and defunctionalization 2. Prior art

3. Our approach

4. Closing remarks Closure conversion

Closure conversion turns a program that makes use of arbitrary functions into a program where only closed functions (code pointers) are allowed. λ-abstractions in the source program are encoded as pairs of a code pointer and an environment (closures).

⟦λx.e⟧ = (λ({x̄}, x).⟦e⟧, {x̄})  where x̄ is fv(λx.e)
⟦e_{1} e_{2}⟧ = let (code, env) = ⟦e_{1}⟧ in code (env, ⟦e_{2}⟧)

It is known that closure conversion preserves types, provided function types are suitably encoded [Minamide, Morrisett, and Harper, POPL’96]:

⟦τ_{1} → τ_{2}⟧ = ∃α.((α × ⟦τ_{1}⟧ → ⟦τ_{2}⟧) × α)

A close cousin: defunctionalization Defunctionalization [Reynolds, 1972] encodes λ-abstractions as pairs of a tag and an environment, that is, as applications of a data constructor to an environment:

⟦λ^{m}x.e⟧ = m {x̄} where x̄ is fv(λx.e)

Function application is encoded as a call to a globally defined function apply...

⟦e_{1} e_{2}⟧ = apply ⟦e_{1}⟧ ⟦e_{2}⟧

... which performs case analysis over m and branches to the appropriate code:

letrec apply = λf .λarg.case f of | m {x̄} ↦ let x = arg in ⟦e⟧ (* one such clause for every tag m *)

Does defunctionalization preserve types?

Imagine the source program contains the functions λ^{succ}x.x + 1 and λ^{not}x.not x, whose types are int → int and bool → bool. Then, the body of apply contains the following clauses:

| succ ↦ let x = arg in x + 1
| not ↦ let x = arg in not x

In (say) System F, these clauses make incompatible assumptions about arg, and produce results of incompatible types: thus, apply is ill-typed.

Prior art: specializing apply

One solution is to split apply into a family of functions, indexed by types:

letrec apply_{int→int} = λf .λarg.case f of | succ ↦ let x = arg in x + 1 and apply_{bool→bool} = λf .λarg.case f of

| not ↦ let x = arg in not x

Here, the data constructors succ and not may be declared as follows:

succ : Arrow_{int→int}
not : Arrow_{bool→bool}

where Arrow_{int→int} and Arrow_{bool→bool} are distinct algebraic data types.

Shortcoming: no polymorphism

In this approach, we have

⟦e_{1} e_{2}⟧ = apply_{τ_{1}→τ_{2}} ⟦e_{1}⟧ ⟦e_{2}⟧ where e_{1} has type τ_{1} → τ_{2}
⟦τ_{1} → τ_{2}⟧ = Arrow_{τ_{1}→τ_{2}}

The trouble is, these definitions only make sense when τ_{1} → τ_{2} has no free type variables. There is no sensible way of translating

Λα_{1}.Λα_{2}.λf : α_{1} → α_{2}.λx : α_{1}.(f x).

As a result, this approach is applicable in a simply-typed setting only (and, via monomorphization, in the setting of ML).

Our approach In order to translate (f x) where f has type α_{1} → α_{2}, we must have

apply : ∀α_{1}α_{2}.⟦α_{1} → α_{2}⟧ → ⟦α_{1}⟧ → ⟦α_{2}⟧.

If, furthermore, the type encoding is uniform, then the above implies

apply ⟦τ_{1}⟧ ⟦τ_{2}⟧ : ⟦τ_{1} → τ_{2}⟧ → ⟦τ_{1}⟧ → ⟦τ_{2}⟧

for all τ_{1} and τ_{2}, so this one apply function is in fact suitable for translating arbitrary applications.

A uniform type encoding

Let Arrow be a binary algebraic data type constructor, and let

\begin{aligned}⟦α⟧ & = & α \\ ⟦τ_{1} → τ_{2}⟧ & = & Arrow ⟦τ_{1}⟧ ⟦τ_{2}⟧ \end{aligned}

This yields a uniform type encoding. Since λ^{succ}x.x + 1 and λ^{not}x.not x have types int → int and bool → bool, their encodings must have types Arrow int int and Arrow bool bool, respectively. So, we declare:

succ : Arrow int int
not : Arrow bool bool

Arrow is a guarded algebraic data type [Xi, Chen, and Chen, POPL’03].

Does defunctionalization preserve types? (reconsidered)

The body of apply, enriched with type annotations, is now:

letrec apply : ∀α_{1}α_{2}.Arrow α_{1} α_{2} → α_{1} → α_{2} =

Λα_{1}.Λα_{2}.λf : Arrow α_{1} α_{2}.λarg : α_{1}.

case f of

| succ ↦ (* f is succ, so Arrow α_{1} α_{2} = Arrow int int holds *)

let x = arg in x + 1 : α_{2} | not ↦ (* f is not, so Arrow α_{1} α_{2} = Arrow bool bool holds *)

let x = arg in not x : α_{2}

Case analysis over a guarded algebraic data type yields extra type information. Defunctionalization is now type-preserving.

Specialization

One may define versions of apply that are specialized with respect to the types of the parameter and of the result:

apply_{τ_{1}→τ_{2}} : ∀ᾱ.⟦τ_{1} → τ_{2}⟧ → ⟦τ_{1}⟧ → ⟦τ_{2}⟧ where ᾱ is ftv(τ_{1} → τ_{2}),

or with respect to the number of arguments that are simultaneously available:

apply_{n} : ∀α_{1} … α_{n}α_{n+1}.⟦α_{1} → … → α_{n} → α_{n+1}⟧ → α_{1} → … → α_{n} → α_{n+1},

or both. Branches that lead to an inconsistent typing assumption may be pruned—for instance, apply_{int→int} need not check for the tag not. This allows dispatch to be made more efficient based on type information available at the call site.

Closing remarks

• When viewed as a transformation from System F, extended with guarded algebraic data types, into itself, defunctionalization is type-preserving.

• Defunctionalization per se is not type-directed, so its correctness may be established using a generic (untyped) simulation argument.

• Interesting type-directed optimizations are possible.

• This illustrates the usefulness of guarded algebraic data types as a programming language feature. (Defunctionalization turns Danvy’s [1998] clever sprintf encoding back to direct style!)