Gaining Closure

A function that captures a variable may outlive the scope that created it. A counter returned from a factory should keep counting after the factory returns. A callback should still have the values it needs when it is finally invoked. The developer writes those functions for what they do, while the compiler and runtime must arrange for their captured state to remain available.

Our Fidelity framework uses the Standard ML and MLKit tradition of flat closures to make those captures explicit in native compilation. Clef specifies which values are copied, which storage is shared, and how long that storage must remain valid. Its null-free construction rule applies to the resulting function and environment.

In a managed runtime, garbage collection can keep captured state alive for as long as it remains reachable. Our native design instead makes lifetime and placement decisions explicit in the compiler. The same function syntax can then work with storage appropriate to a desktop application, an embedded device, or another target with a different memory contract.

The Closure Problem in Native Compilation

Consider a simple counter factory in Clef:

let makeCounter (start: int) : (unit -> int) =
    let mutable count = start
    fun () ->
        count <- count + 1
        count

This function returns a lambda that captures count, a mutable variable. Each call to makeCounter should produce an independent counter with its own state. When invoked, each counter should increment its own captured value.

Whether a value becomes a closure at all is decided upstream, by arity analysis: a saturated call compiles to a direct function call and needs no closure, while a partial application or a returned lambda like this one does. Arity On The Side of Caution covers that decision. This page describes closure representation once arity analysis has decided a closure is required.

In .NET, this works transparently. The runtime allocates a heap object to hold captured variables, and garbage collection ensures that object lives as long as any closure references it. The developer writes the code. The runtime handles memory.

Clef’s native path needs to settle that memory contract before it lowers the closure: where the captured state lives, how each closure references it, and when the storage can be reclaimed. The counter should behave the same way whichever placement satisfies those requirements.

Linked and Flat Closure Representations

Linked and flat closure representations make different trade-offs in capture access and retained storage. Our Fidelity framework uses the flat representation.

Linked Closures

The traditional approach, dating to early Lisp implementations and formalized in Cardelli’s 1983 work, uses linked environment chains. Each closure contains a pointer to its immediately enclosing environment, which may itself contain pointers to outer environments.

  flowchart LR
    subgraph Closure["Closure"]
        CP1[code]
        EP[env_ptr]
    end
    subgraph OuterEnv["Outer Env"]
        CX[captured_x: int]
        OP[outer_ptr]
    end
    subgraph More["..."]
        ETC[" "]
    end
    EP --> OuterEnv
    OP --> More

This representation is simple to implement. Creating a closure requires only storing a pointer to the current environment. Variable access follows the chain to find the appropriate binding.

An environment link can keep bindings alive even when the closure uses only one of them. A compiler must account for that retained reachability when deciding whether storage can be reclaimed.

Flat Closures

A flat closure stores its captures in one environment. Immutable values are copied into fields. Mutable bindings contribute references to their shared storage cells. The field list records the captures directly, without a chain of enclosing environments.

  flowchart LR
    subgraph FlatClosure["Flat Closure"]
        direction LR
        CP[code]
        CX[captured_x]
        CY[captured_y]
        ETC[...]
    end

Each capture is accessed through a field of the flat environment. A field can itself hold a reference, so a flat field list does not imply that all reachable data lives inside that environment.

Constructing a flat environment copies its capture entries, which can cost more than retaining one environment link. Its size depends on the captures and their selected layouts. Each capture then has a known field offset.

Our Fidelity design uses the explicit field list to avoid retaining unused enclosing bindings. This is the motivation of the safe-for-space closure-conversion work discussed below. Reclaiming one closure removes its references. Captured objects remain live wherever another reference still reaches them, including through another closure. The lifetime analysis must account for that sharing.

The MLKit Heritage

The MLKit compiler, developed at the IT University of Copenhagen, pioneered region-based memory management for Standard ML. In place of garbage collection, MLKit statically infers memory regions and their lifetimes. Values are allocated into regions, which are reclaimed when their lifetimes end.

Flat environments fit region analysis because their direct capture dependencies are explicit. Reclaiming an environment’s region also requires that no remaining use depends on storage in that region. A capture can refer to a value in another region, whose lifetime remains a separate obligation.

The MLKit approach influenced our design significantly. While our current implementation uses stack allocation and explicit region management in place of MLKit’s full region inference, the flat closure representation leaves room for future adoption of more involved region-based schemes.

ByValue and ByRef Capture Semantics

Clef specifies different capture modes for mutable and immutable bindings. ByRef Resolved develops the native reference semantics.

When a closure captures an immutable binding, it copies the value into the environment. If that value is a reference to mutable storage, the reference is copied and the underlying storage remains shared.

Mutable bindings require different treatment. A mutable variable captured by multiple closures must share state. All closures must see the same value. Copying the value would break this contract.

The solution is to capture mutable bindings by reference. The portable middle end carries a view of the binding’s storage cell (memref<1xT>). The target pathway realizes the address. The value is not copied into an independent mutable cell.

let makeCounter (start: int) =
    let mutable count = start
    fun () ->
        count <- count + 1
        count

The returned closure must share count with every other closure over that binding. Its storage must outlive the invocation of makeCounter. A pointer into a reclaimed stack frame would violate the contract. The lifetime classification places the storage where its lifetime covers the closure: stack, region, static storage, or heap as justified by the graph and target capabilities. Arena allocation is one realization of the region case.

Captured Constraints

Clef’s flat closure representation carries the source binding’s dimensional identity together with its capture mode. An immutable scalar is captured by value, so a range constraint established for that value remains valid inside the closure. A mutable binding is captured by reference to shared storage, so a guard checked when the closure is constructed does not automatically constrain a later read. Writes through an alias or another closure matter just as direct assignment does. These are the normative capture semantics, independent of whether the backend uses a native flat environment or a JavaScript host closure.

The distinction applies to lazy values and sequences as well. Deferring a computation preserves its dimensional type and pending obligations. Mutable inputs still require validity at the relevant reads. Memoization shares the result already computed. It does not make a shared mutable object inside that result independently polymorphic for each consumer. An immutable binding and immutable reachable storage are different properties, specified in generalization and deferred computation.

Width Inference §2 requires range constraints to retain their guard and dependency provenance on the PSG. If a callback captures an immutable slice length, a bound already established for that value remains useful when the callback runs. If it reads a shared counter, the compiler must account for intervening writes before reusing a bound on the counter’s contents. Retaining those dependencies lets ordinary closure code reuse the facts that still hold and request a fresh check where one is needed.

The Two-Pass Architecture

Our Composer implementation separates capture identification from the allocation of SSA (Static Single Assignment) identifiers and concrete environment layout. The layout needs stable identifiers for the captured values and their storage.

The solution is a two-pass architecture in the Alex preprocessing phase.

Pass 1: Capture Identification runs before SSA assignment. It traverses the Program Semantic Graph (PSG), identifies lambda nodes, and marks which variables each lambda captures. This pass also determines capture semantics: ByValue for immutable bindings, ByRef for mutable bindings.

SSA Assignment then runs with awareness of captures. Variables that are captured by reference receive additional SSA identifiers for their addresses, not just their values.

Pass 2: Closure Layout runs after SSA assignment. With SSA identifiers now available, this pass computes the concrete layout of each closure’s environment structure: field offsets, struct types, and the synthetic SSA identifiers for environment allocation and field access.

Our PSG must carry settled capture and layout facts before witnessing. The Zipper and witnesses read those facts when producing portable IR. A proof ledger currently cross-checks preservation while the proof-carrying graph mechanism is validated. That scaffold does not transfer responsibility for the constraints out of the PSG.

The Witnessed Form

The portable middle end represents a closure as a function value and an environment buffer. The example below illustrates the shape after lifetime analysis has supplied fresh storage for this particular counter. Its four-byte cell assumes that the selected representation of count is 32 bits. Both the extent and that width must come from the graph.

// Illustrative lowered helper: caller supplies distinct, lifetime-checked storage.
func.func @makeCounter(%start: i32, %env: memref<4xi8>)
    -> ((memref<4xi8>) -> i32, memref<4xi8>) {
  %c0 = arith.constant 0 : index

  // The environment belongs to this counter and outlives every use of it.
  %count = memref.view %env[%c0][] : memref<4xi8> to memref<1xi32>
  memref.store %start, %count[%c0] : memref<1xi32>

  // The code: a first-class function value in the portable dialect.
  %fn = func.constant @makeCounter_lambda : (memref<4xi8>) -> i32

  return %fn, %env : (memref<4xi8>) -> i32, memref<4xi8>
}

The closure representation contract carries the function and environment as two values. func.constant names the implementation and func.call_indirect consumes a function value. When an aggregate stores a closure, its settled closure form must also preserve the code identity. An environment buffer alone cannot distinguish closures with the same layout and different implementations.

This portable form uses func, memref, and arith. The target pathway later realizes those operations with its documented conversions. A settled source property must retain its checked correspondence across that conversion boundary, even when its original type representation has served its purpose.

The construction rule requires every environment slot to be initialized and the function value to identify an implementation. Possible absence is represented explicitly in the source type. Null-Free by Construction develops that contract, which the witness and target conversion must preserve.

The construction rule excludes a null-function case from a valid Clef closure. Lowering must preserve that guarantee. Allocation, capture initialization, and invocation still have the costs of their selected realization.

Managed implementations often represent closures with heap objects whose lifetimes are maintained by garbage collection. Clef’s native path instead requires explicit lifetime and placement facts for the environment and any shared captures.

One Witnessed Form, Three Realizations

Our closure design admits several target realizations. A known environment extent gives a target a concrete layout to work with. Moving the closure to another memory space additionally requires usable code identity and a valid mapping for every captured reference. A byte copy alone cannot relocate a storage cell or preserve its shared identity. Those transfer obligations connect closure placement to BAREWire’s memory, IPC, and network contracts.

LLVM: The Common Case

The native CPU pathway uses LLVM. Its conversion pipeline realizes portable function values and environment views using the target’s function pointers and memory representation. The following fragment illustrates that target-level form. Details such as the memref calling convention depend on the pathway’s settled lowering contract.

// Below the witness boundary: produced by standard target conversion, not by Alex.
%fn_ptr  = llvm.mlir.addressof @makeCounter_lambda : !llvm.ptr
%env_ptr = llvm.getelementptr %arena_base[0] : (!llvm.ptr) -> !llvm.ptr
// application, elsewhere:
%r = llvm.call %fn_ptr(%env_ptr) : !llvm.ptr, (!llvm.ptr) -> i32

The LLVM operations belong below the portable witness boundary. Capture initialization and source identity must already have their evidence before this target realization is chosen.

CIRCT: The Hardware Direction

For hardware targets, our design points toward CIRCT. An environment with synthesizable captures can become a structure carried on wires or held in registers. Applying a closure also requires an available implementation of its code and an established schedule. Flat layout supplies a finite list of direct captures, while referenced storage and stateful effects require their own hardware treatment. The explicit captures give the hardware pathway a concrete set of dependencies to realize.

MLIR-AIE: The NPU Direction

For an MLIR-AIE-style target, an environment with a known byte extent offers a candidate tile-local buffer and DMA transfer size. That transfer must also establish where captured references point and whether the closure’s code can execute at the destination. We want to extend the native LLVM implementation’s explicit capture contract to this setting, so an offloaded function arrives with both the state it needs and a checked account of how it may use that state.

The same source capture contract applies across these realizations. Each pathway must establish its storage, code, and sharing correspondence before accepting the closure.

The Developer-Facing API

Clef developers use ordinary function syntax:

let greetAlice = makeGreeter "Alice"
let greetBob = makeGreeter "Bob"
Console.writeln (greetAlice "Hello, ")   // "Hello, Alice"
Console.writeln (greetBob "Welcome, ")   // "Welcome, Bob"

The source syntax leaves placement to the compiler. Scope-bounded environments may use the stack, while escaping closures need storage whose lifetime covers their use. Native flat environments and JavaScript host closures must preserve the same observable immutable-copy and mutable-sharing semantics.

Our tooling should expose these Clef capture and lifetime facts directly, so developers can inspect the native consequences without inheriting assumptions from the .NET host.

Research Basis

Our closure implementation builds on decades of research. The key sources include:

Appel and Shao’s 1992 paper “Callee-save Registers in Continuation-passing Style” introduced the flat closure representation that eliminates environment chains. Their subsequent work on space efficiency, from “Space-Efficient Closure Representations” at LFP 1994 through the 2000 TOPLAS treatment of safe-for-space closure conversion, formalized the safety properties that flat closures provide.

Tofte and Talpin’s 1997 paper “Region-Based Memory Management” established the theoretical foundation for the MLKit compiler’s approach, demonstrating that static analysis could replace garbage collection for a significant class of programs.

The MLKit compiler itself, documented in “Programming with Regions in the MLKit” (Elsman, 2021), provides a production-quality implementation of these ideas for Standard ML.

More recently, Perconti and Ahmed’s 2019 paper “Closure Conversion is Safe for Space” provides formal verification that flat closure representations maintain the asymptotic space bounds of the original program, under the conditions of that conversion.

We apply this research to Clef’s capture contract and its compilation through the PSG into portable MLIR. The representation choice supplies a basis for lifetime reasoning. Correctness of the resulting implementation still depends on its capture, allocation, and lowering behavior.

Validation Scope

The counter factory gives us a useful first test: two returned counters must keep independent state, while two closures over the same binding must observe their shared state. Delayed callbacks add another: an immutable captured constraint should remain usable, while a stale fact about mutable contents should prompt a new check. These regression cases complement the preservation checks required at each lowering boundary.

Higher-order functions, sequences, and lazy values extend the closure mechanism. Each introduces additional demand or sharing behavior that must preserve the source capture contract.

A flat field list makes those direct dependencies inspectable. We can extend the language’s higher-order features while keeping the same promise to the developer: the values a function needs remain available for its uses, with the intended copying and sharing behavior intact.