Closure Conversion, with Polymorphism

In the last post, we discussed closure conversion applied to the Simply-Typed Lambda Calculus (STLC), perhaps the simplest language with lexical scoping and first-class functions. Now we turn to closure conversion applied to a richer language, one that includes generics.

The Polymorphic Lambda Calculus (aka. System F)

System F extends the STLC with first-class generics: the $\Lambda$ expression and an expression for instantiating a generic.

$$\begin{array}{lrcl} \text{types} & T & ::= & \ldots \mid \alpha \mid \forall \alpha. T \\ \text{expressions} & e & ::= & \ldots \mid \Lambda \alpha. e \mid e[T] \\ \text{values} & v & ::= & \ldots \mid \Lambda \alpha. e \\ \text{frames} & F & ::= & \ldots \mid \Box[T] \end{array}$$ The expression $\Lambda \alpha.e$ creates a generic expression parametrized by the type variable $\alpha$. The type of such a generic expression is $\forall \alpha. T$, where T is the type of the inner expression e. The expression $e[T]$ instantiates the generic e, replacing its type parameter with type T.

The typing rules for System F are those of the STLC plus the following:

$$\frac{ \Gamma,\alpha \vdash e : T }{ \Gamma \vdash \Lambda \alpha.e : \forall \alpha. T } \qquad \frac{ \Gamma \vdash e : \forall \alpha. T_2 }{ \Gamma \vdash e[T_1] : [\alpha := T_1] T_2 }$$

Also, there is one new reduction rule:

$$(\Lambda \alpha. e)[T] \longrightarrow [\alpha {:=} T]e$$

Updating the Intermediate Language: IL2

With the introduction of generics, we not only worry about lexically scoped term variables but we are also concerned with lexically scoped type variables. So the $\delta$ and $\gamma$ functions must be updated to include type variables and their bindings. Furthermore, the closure operator must be extended with type arguments to bind the new type variables.

$$\begin{array}{lrcl} \text{expressions} & e & ::= \ldots \mid \delta \overline{y{:}T},\overline{\alpha},x{:}T.e \mid \gamma x{:}T,\overline{y{=}v,\alpha{=}T}. e \mid e \{ \overline{e}, \overline{T} \} \end{array}$$

The following are the reduction rules for the functions of IL2.

$$\begin{align*} (\delta \overline{y{:}T},\overline{\alpha},x{:}T.e)\{\overline{e},\overline{T}\} & \longrightarrow \gamma x{:}T,\overline{y{=}v,\alpha{=}T}. e \\ (\gamma x{:}T,\overline{y{=}v,\alpha{=}T}. e)\, v & \longrightarrow [\overline{\alpha{:=}T}]\{ \overline{y{:=}v}\} \{ x{:=}v \} e \end{align*}$$

Next we turn to the $\Lambda$. We'll need to translate $\Lambda$ to something in IL2, and in the spirit of closure conversion, it should be something that does not support lexical scoping. Inspired by the $\delta$ and $\gamma$ functions, we create analogous things for generics.

$$\begin{array}{lrcl} \text{expressions} & e & ::= \ldots \mid \Phi \overline{y{:}T},\overline{\alpha},\alpha.e \mid \Upsilon \alpha,\overline{y{=}v,\alpha{=}T}. e \end{array}$$

The following are the reduction rules for the generics of IL2.

$$\begin{align*} (\Phi \overline{y{:}T},\overline{\alpha},\alpha.e)\{\overline{e},\overline{T}\} & \longrightarrow \Upsilon \alpha,\overline{y{=}v,\alpha{=}T}. e \\ (\Upsilon \alpha,\overline{y{=}v,\alpha{=}T}. e) [T] & \longrightarrow [\overline{\alpha{:=}T}]\{ \overline{y{:=}v} \} [\alpha{:=}T]e \end{align*}$$

Closure conversion for System F

With IL2 in place, the definition of closure conversion for System F is relatively straightforward. The case for $\lambda$ computes the free type variables (FTV) and includes them in the $\delta$ function. The new case for $\Lambda$ is analogous to the case for $\lambda$.

$$\mathit{ClosureConversion}(e) = \mathrm{let}\;(e',\overline{f}) = C(e)\,\mathrm{in}\; (\mathbf{globals} \,\overline{f}\,\mathbf{in}\, e') \\ $$ $$\begin{align*} C(x) &= (x,\epsilon) \\ C(c) &= (c,\epsilon) \\ C(\mathit{op}(\overline{e})) &= \mathrm{let}\;(\overline{e}',\overline{f}) = \overline{C}(\overline{e})\,\mathrm{in} \; (\mathit{op}(\overline{e}'), \overline{f}) \\ C(\lambda x{:}T.e) &= \mathrm{let}\; (e',\overline{f}) = C(e) \\ & \qquad\; \overline{y{:}T} = \mathrm{FV}(e) - \{x\} \\ & \qquad\; \overline{\alpha} = \mathrm{FTV}(e) \\ & \qquad\; g = \mathrm{freshname}() \\ & \quad \mathrm{in}\; (g\{\overline{y},\overline{\alpha}\}, (g = (\delta \overline{y{:}T,\alpha},x{:}T.e'), \overline{f}))\\ C(e_1\,e_2) &= \mathrm{let}\; (e'_1,\overline{f}_1) = C(e_1) \\ & \qquad\; (e'_2,\overline{f}_2) = C(e_2) \\ & \quad \mathrm{in}\; (e'_1\,e'_2, (\overline{f}_1 , \overline{f}_2)) \\ C(\Lambda \alpha.e) &= \mathrm{let}\; (e',\overline{f}) = C(e) \\ & \qquad\; \overline{y{:}T} = \mathrm{FV}(e) \\ & \qquad\; \overline{\alpha} = \mathrm{FTV}(e) - \{ \alpha \} \\ & \qquad\; g = \mathrm{freshname}() \\ & \quad \mathrm{in}\; (g\{\overline{y},\overline{\alpha}\}, (g = (\Phi \overline{y{:}T,\alpha},\alpha.e'), \overline{f}))\\ C(e[T]) &= \mathrm{let}\;(e',\overline{f}) = C(e) \,\mathrm{in} \; (e'[T], \overline{f}) \end{align*}$$