Unboxed Closures

[evincarofautumn]

Currently, when a function is placed on the stack, its closure variables are copied to a new heap-allocated structure. I believe it’s possible to avoid this in the following way:

1. Treat closures as existential types that hide the closure types Ĉ and convert function types to take the closure as arguments:

   R → S ⇓ ∃Ĉ. (R × Ĉ → S)

2. Convert words that accept closures into Skolem normal form:

   call : ∀RS. (R × ∃Ĉ. (R × Ĉ → S) → S) ⇓ call′ : ∀RSĈ. (R × (R × Ĉ → S) → S)

3. Convert words that return closures into continuation-passing style:

   function : ∀RT. R × T → R × ∀S.∃Ĉ. (S × Ĉ → S × T) ⇓ function′ : ∀RTV. R × ∀UĈ. (U × ∀S. (S × Ĉ → S × T) → V) × T → V

4. Convert call sites of words that return closures into continuation-passing style:

   1 function f ⇓ { f′ } 1 function′

For (4), I’m not yet sure whether the types will work out when converting the CPS continuation to a closure itself—need to make sure this terminates.

I don’t believe we need to surface existentials to the user—they can be an intermediate step only. Existentials would be useful in their own right, but would require additional design work. Tentative syntax would be [T…] T for existential quantification, by visual analogy with <> : ∀ :: [] : ∃, but we would also need notation for packing and unpacking.

It’s also worth noting that size for arbitrary unboxed existentials might need to be dynamic, which complicates code generation; this problem doesn’t exist if they are fully eliminated.

[evincarofautumn]

I’ve been thinking more about incorporating first-class unboxed existentials, and I have a sketch of a design. As a bonus, it would give us a more elegant implementation of closures.

Syntax:

• Existential quantification: [T] (…)

  Represents an instance of a type containing some abstract type variables.

• Packing: pack (A) as [T] (B)

  Takes one argument from the stack and packs it into an existential, where A is the concrete hidden type and T is the type variable representing it within the type B. Both A and T can be replaced with a list of any number of types (as long as there are the same number in each), but only one value is ever packed. To pack multiple values, use a pair or structure.

• Unpacking: unpack …

  Takes one argument from the stack, an existentially quantified type, and unpacks all top-level existentials into scope with fresh type constants. Like a local variable introduction, unpack introduces a new scope (…), in which the existentially quantified types are available as fresh type constants that aren’t allowed to escape.

Example:

define f (Int32 -> (-> Int32)):
  -> x;
  { x + 1 }

2 f call  // 3

// =>

// Quotations are rewritten to take their closure values from the stack.
define f::lambda0 (Int32 -> Int32):
  -> closure0;
  closure0 + 1

// Constructing a quotation packs the closure values and function pointer into an existential.
define f (Int32 -> [T] (Pair<T, (T => Int32)>)):
  -> x;
  x \f::lambda0 pair
  pack (Int32) as [T] (Pair<T, (T => Int32)>)

// Invoking a closure unpacks it onto the stack and does a normal function call.
2 f unpack
  unpair
  call

Note that this wouldn’t compile if the existential contained T => T, because T would escape. Also, call needs to be overloaded to work on both functions with (->) and without (=>) closures, which opens the door for user-defined callable values.

I don’t want to have to add a subtyping relationship between function pointers and functions with closures, so the surface syntax should probably always produce closures; if they don’t capture anything, we can allow existentials that quantify over no types [] (T) or maybe introduce a dummy type variable defaulted to Unit.

We may also need to store size information in kinds, in order to deal with higher-rank polymorphism over unboxed types.

For packing, rather than pack (A) as [T] (B), we could bring the type variables and types closer together with something more along the lines of pack [T = A] (B). I don’t care for = here because we don’t use it anywhere else in the language, and : always means a layout block; maybe something like pack [A as T] (B)?