Monday, July 09, 2012

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 expression and an expression for instantiating a generic. The expression creates a generic expression parametrized by the type variable . The type of such a generic expression is , where T is the type of the inner expression e. The expression 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:

Also, there is one new reduction rule:

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 and 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.

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

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

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

Closure conversion for System F

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

No comments:

Post a Comment