Lazy Value Representation

Normative specification for lazy value memory layout and thunk semantics in Clef compilation.

1. Overview

Clef implements Lazy<'T> as an extension of the flat closure architecture. Lazy values are thunks that defer computation until forced. This chapter specifies the memory representation, capture semantics, thunk calling convention, and memoization behavior.

2. Relationship to Closures

Lazy values build directly on the flat closure representation specified in Closure Representation. A lazy value is a flat closure with additional fields for memoization state.

Key Insight: The lazy keyword creates a thunk, which is a nullary closure (a function of unit) with embedded state tracking whether evaluation has occurred.

3. Memory Layout Specification

3.1 Lazy Structure

A lazy value in Clef is the two-value pair (thunk, env) of Closure Representation §6.3: the thunk is a function value (func.constant @thunk), and the environment is a flat struct containing:

Lazy<T> with captures [c₁: T₁, ..., cₘ: Tₘ]
┌─────────────────────────────────────────────────────────────────────────┐
│ computed: i1              (1 byte, padded to alignment)                  │
├─────────────────────────────────────────────────────────────────────────┤
│ value: T                  (sizeof(T) bytes, aligned)                     │
├─────────────────────────────────────────────────────────────────────────┤
│ c₁: T₁                    (sizeof(T₁) bytes, aligned)                    │
├─────────────────────────────────────────────────────────────────────────┤
│ ...                                                                      │
├─────────────────────────────────────────────────────────────────────────┤
│ cₘ: Tₘ                    (sizeof(Tₘ) bytes, aligned)                    │
└─────────────────────────────────────────────────────────────────────────┘

Field Indices:
  [0] = computed flag
  [1] = memoized value
  [2..N+1] = captured values

The thunk symbol is never stored in the environment as data: it travels as the function-value half of the pair, and where the force site knows the thunk (a lazy value that does not escape) it is elided altogether and force is a direct call. An earlier revision of this chapter placed a code_ptr word at [2]; that slot is retired with the cast that populated it (Backend Lowering Architecture §4).

3.2 Field Semantics

3.3 Size Formula

For a lazy value with element type T and N captures with types T₁, ..., Tₙ:

size(Lazy<T, [T₁...Tₙ]>) = align(1) + sizeof(T) + Σᵢ sizeof(Tᵢ)
                         = 1 + padding + sizeof(T) + Σᵢ sizeof(Tᵢ)

No platform word is spent on a code pointer; the thunk is the other half of the pair, not a field. The byte totals below are worked for two targets. Taking int as a 64-bit value for the x86-64 column:

• lazy 42 (no captures):
  • x86-64: 1 + 7 + 8 = 16 bytes
  • thumbv8m (M33), with int as a 4-byte value: 1 + 3 + 4 = 8 bytes
• lazy (a + b) with a, b: int:
  • x86-64: 1 + 7 + 8 + 8 + 8 = 32 bytes
  • thumbv8m (M33): 1 + 3 + 4 + 4 + 4 = 16 bytes

4. Thunk Calling Convention

4.1 Struct Pointer Passing

Clef uses the environment passing convention for thunks. The thunk receives its environment — the lazy struct of §3.1 — as its sole environment parameter and extracts captures itself.

Thunk Signature:

thunk_fn: (memref<Exi8>) -> T      // E = the environment extent of §3.3, a literal at saturation

Rationale:

• Uniform signature for all thunks regardless of capture count
• Force is one call: func.call_indirect %thunk(%env), or func.call @thunk(%env) where the force site knows the thunk
• Thunk extracts its own captures at known offsets

4.2 Thunk Implementation

The thunk body:

1. Receives the lazy struct’s environment as %arg0
2. Extracts captures from indices [3..N+2]
3. Executes the deferred computation
4. Returns the result

The middle end emits the thunk as a portable func.func and reads captures through a memref, exactly as the flat closure does (see Flat Closure Pattern and Deferred Resolution). Nothing in the middle-end form names a target:

// Middle end — portable dialects only.
func.func private @thunk_example(%env: memref<?xi64>) -> i64 {
    // Extract capture at index 3 — portable memref access, no ABI committed.
    %c3 = arith.constant 3 : index
    %a = memref.load %env[%c3] : memref<?xi64>

    // Extract capture at index 4.
    %c4 = arith.constant 4 : index
    %b = memref.load %env[%c4] : memref<?xi64>

    // Compute result.
    %result = arith.addi %a, %b : i64
    func.return %result : i64
}

A thunk with no captures (e.g., lazy 42) is still a func.func; its body reads nothing from the environment. The thunk is the function-value half of the lazy pair — func.constant @thunk — and is never stored as data; no cast exists in the middle end (Backend Lowering Architecture §4).

The llvm.func / llvm.mlir.addressof form is one target pathway’s realization of this thunk, not what the middle end emits. On the LLVM pathway the standard lowerings do all of it: func.constant becomes llvm.mlir.addressof, and the memref capture read becomes a getelementptr + load in the target ABI. No cast-resolution pass runs. A different pathway (CIRCT, SPIR-V, WebAssembly) realizes the same middle-end IR its own way.

4.3 Alternative Considered: Parameter Passing

An alternative convention passes captures as function parameters:

thunk_fn: (cap₁, cap₂, ..., capₙ) -> T

This was rejected because:

• Force implementation must know capture types at each call site
• Different thunks have different signatures
• Type complexity at forcing increases with capture count

5. Capture Analysis

5.1 Binding Classification

Capture analysis for lazy values must distinguish:

Critical Rule: Module-level bindings are NOT captured. They have stable addresses and are referenced directly in the generated code.

5.2 IsModuleLevel Tracking

CCS (Clef Compiler Service) tracks binding scope in ResolvedBinding:

type ResolvedBinding = {
    QualifiedName: string
    Type: NativeType
    IsMutable: bool
    NodeId: NodeId option
    IsModuleLevel: bool  // True if defined at module scope
    // ...
}

During capture analysis:

let computeCaptures env bodyNodeId excludeNames =
    bodyVarRefs
    |> List.choose (fun name ->
        match tryLookupBinding name env with
        | Some binding ->
            if binding.IsModuleLevel then
                None  // Not captured - reference by address
            else
                Some { Name = name; Type = binding.Type; ... }
        | None -> None)

5.3 Example: Correct vs Incorrect Capture

// Module level
let sideEffect msg = Console.writeln msg

// Function with lazy returning body
let lazyAdd a b = lazy (sideEffect "Computing..."; a + b)

Correct captures for lazyAdd’s lazy body: [a, b]

Incorrect (bug): [a, b, sideEffect]

The sideEffect function is module-level; it should be called via its global address, not captured.

6. LazyExpr in the PSG

6.1 SemanticKind.LazyExpr

type SemanticKind =
    // ...
    | LazyExpr of bodyNodeId: NodeId * captures: CaptureInfo list

The PSG node contains:

• bodyNodeId: Reference to the thunk Lambda node
• captures: Pre-computed capture list (same as thunk’s captures)

6.2 Lambda with LazyThunk Context

The thunk is represented as a Lambda with special context:

type LambdaContext =
    | RegularClosure
    | LazyThunk
    // ...

SemanticKind.Lambda(
    parameters = [("_unit", UnitType, NodeId -1)],
    bodyNodeId = <computation body>,
    captures = [...],
    enclosingFunction = ...,
    context = LambdaContext.LazyThunk
)

7. Coeffect Model

7.1 LazyLayout Coeffect

SSA assignment computes LazyLayout for each lazy expression:

type LazyLayout = {
    LazyNodeId: NodeId              // The LazyExpr node
    CaptureCount: int               // Number of captures
    Captures: CaptureSlot list      // Reuses CaptureSlot from closures
    LazyStructType: MLIRType        // { i1, T, cap₀, cap₁, ... }
    ElementType: MLIRType           // T (for force operations)
    
    // SSA identifiers for construction
    FalseConstSSA: SSA              // computed flag = false
    UndefSSA: SSA                   // undef lazy struct
    WithComputedSSA: SSA            // insertvalue computed at [0]
    CaptureInsertSSAs: SSA list     // insertvalue for each capture at [2..N+1]
    LazyResultSSA: SSA              // final result
}

This layout is computed in Composer’s SSA assignment today, which is interim: it is the consequence of the closure hyperedge and moves into CCS with it (clef/docs/fidelity/phg/Closure_Retooling_Plan.md). The witness reads it; it does not compute it.

7.2 SSA Cost Formula

For a lazy expression with N captures: 4 + N SSAs

7.3 ClosureLayout for Thunk

The thunk Lambda uses ClosureLayout with LazyThunk context:

type ClosureLayout = {
    // ...
    Context: LambdaContext  // LazyThunk for lazy thunks
    LazyStructType: MLIRType option  // Full lazy struct type for capture extraction
}

When Context = LazyThunk:

• closureExtractionBaseIndex returns 2 (captures start at index 2)
• closureLoadStructType returns the full lazy struct type

8. MLIR Generation

The middle end emits lazy construction over memref, with the thunk address carried as a deferred func_type → index cast. The struct is a memref of the lazy layout; field writes are memref.store at the fixed indices. Nothing here commits a target ABI.

8.1 Lazy Value Creation

// lazy (a + b) where a, b are captured int values.
// Middle end — portable dialects only.

// Step 1: Allocate the lazy struct's storage per its lifetime class (§9).
//         Scope-bounded here, so memref.alloca; a program-lifetime lazy
//         would be a memref.global instead.
%lazy = memref.alloca() : memref<4xi64>

// Step 2: Write computed flag = false at [0].
%c0 = arith.constant 0 : index
%false = arith.constant 0 : i64
memref.store %false, %lazy[%c0] : memref<4xi64>

// Step 3: Write captures at [2], [3], ...
%c2 = arith.constant 2 : index
memref.store %a, %lazy[%c2] : memref<4xi64>
%c3 = arith.constant 3 : index
memref.store %b, %lazy[%c3] : memref<4xi64>

// Step 4: The thunk is the other half of the pair — a function value, not data.
%thunk = func.constant @thunk_lazyAdd_body : (memref<4xi64>) -> i64

// (%thunk, %lazy) is the complete lazy value.

The target pathway commits this to its ABI through its standard lowerings: on the LLVM pathway the memref becomes a pointer with store at the same indices and func.constant becomes llvm.mlir.addressof. That committed form is one pathway’s realization, not middle-end output, and no cast is involved.

8.2 Force Operation

Force reads the computed flag, and either returns the cached value or calls the thunk — the function-value half of the pair — with the environment. The middle end emits this over func, memref, and scf. Nothing here commits a target ABI.

// Lazy.force lazy_val, where the value is (%thunk, %lazy) and %lazy is memref<4xi64> (§8.1).
// Middle end — portable dialects only.

// Read computed flag at [0].
%c0 = arith.constant 0 : index
%flag = memref.load %lazy[%c0] : memref<4xi64>
%zero = arith.constant 0 : i64
%computed = arith.cmpi ne, %flag, %zero : i64

%value = scf.if %computed -> i64 {
    // Already computed: return the cached value at [1].
    %c1 = arith.constant 1 : index
    %cached = memref.load %lazy[%c1] : memref<4xi64>
    scf.yield %cached : i64
} else {
    // Environment-passing convention: call the thunk with its environment.
    // Where the force site knows the thunk this is func.call @thunk_lazyAdd_body(%lazy).
    %result = func.call_indirect %thunk(%lazy) : (memref<4xi64>) -> i64

    // For memoizing: store %result at [1] and set the flag at [0]
    // (§9; current implementation uses pure thunk semantics, no memoization).
    scf.yield %result : i64
}
// %value is the forced result.

The target pathway commits this through its standard lowerings: on the LLVM pathway the memref reads become loads and func.call_indirect becomes an llvm.call through the function value. A different pathway realizes the same middle-end IR its own way.

9. Memoization Strategy

9.1 Current Implementation: Pure Thunk Semantics

The initial Clef implementation provides pure thunk semantics:

• Forcing always executes the computation
• No memoization state is updated
• Correct for pure computations (same result each time)

let expensive = lazy (printfn "Computing..."; 42)
Lazy.force expensive  // Prints, returns 42
Lazy.force expensive  // Prints again, returns 42
 

9.2 Storage Placement

A lazy value is a flat closure, so its storage is placed by the same four-point lifetime lattice that governs closures (see Closure Representation §2.3, §3.3). Escape analysis classifies the lazy value by how long it must live and places it in the storage whose lifetime covers it:

1. Scope-bounded: on the stack (memref.alloca), reclaimed when the enclosing scope exits.
2. Region-bounded: in a region whose lifetime covers it, when it escapes the scope but lives within a region’s lifetime.
3. Program-lifetime: in static storage, emitted as a memref.global, when it is constructed once and held for the life of the program with no free: the platform’s declared mutable program-lifetime space for a mutable lazy value, or its declared immutable program-lifetime space for one that is never written (on an MCU the Sram and Flash regions; the data and rodata sections on an ELF target; constant memory on a GPU).
4. Dynamic: on the heap, when its extent is genuinely dynamic.

Escaping the defining scope does not imply the heap. A lazy value returned from a function and held for the program’s life has a statically knowable, program-long lifetime and belongs in static storage, in the same sense a fixed-address register or a linker-carved buffer is a global. On a target with no allocator, only the scope-bounded and program-lifetime placements have a home; a lazy value that classifies as dynamic there is a compile-time lifetime error, not a silent heap allocation.

Memoization is a mutation-in-place property that interacts with this placement, because in-place update of the computed flag and the value slot requires a stable address:

• A scope-bounded or program-lifetime lazy value already has a stable address (its alloca slot or its memref.global), so memoization writes directly to value at index [1] and sets computed at [0].
• Under concurrent access to a program-lifetime lazy value, the write-once obligation is discharged at compile time by the single-forcer discipline of §11: ownership establishes one semantic forcer, so the race is resolved in the proof before it is resolved in the code. Beneath that discharged proof, the target realization is a compare-and-swap on the computed flag (one force wins) and a memory barrier that makes the memoized value visible across threads.

The current implementation (§9.1) uses pure thunk semantics and updates no state, so it is insensitive to placement. Memoizing semantics are placement-sensitive precisely because they mutate the struct in place.

9.3 Thread Safety Considerations

For memoizing lazy values with concurrent access:

10. Type System Integration

10.1 Lazy Type Constructor

type NativeType =
    // ...
    | TLazy of elementType: NativeType

At the source level:

let x: Lazy<int> = lazy 42

At the native level, the actual struct type includes captures:

// No captures
TStruct [TInt I1; TInt I64; TPtr]

// With captures [a: int; b: int]
TStruct [TInt I1; TInt I64; TPtr; TInt I64; TInt I64]

10.2 Lazy.create and Lazy.force

The Lazy module provides two intrinsic operations:

module Lazy =
    /// Create a lazy value from a thunk
    val create: (unit -> 'T) -> Lazy<'T>
    
    /// Force evaluation of a lazy value
    val force: Lazy<'T> -> 'T

The lazy expr syntax desugars to:

Lazy.create (fun () -> expr)

11. Normative Requirements

1. Flat Representation: Lazy values SHALL use flat closure representation with captures inlined
2. Struct Layout: Field order SHALL be: computed, value, captures; no code pointer SHALL be stored in the environment
3. Capture Indices: Captures SHALL begin at index 2
4. Module-Level Exclusion: Module-level bindings SHALL NOT be captured
5. Thunk Convention: Thunks SHALL receive their environment as the sole environment parameter; a lazy value SHALL be the two-value pair (thunk, env) of Closure Representation §6.3, with the thunk elided where the force site knows it
6. Lifetime-Driven Placement: A lazy value’s storage SHALL be placed by escape analysis in the storage whose lifetime covers it, per the four-point lattice of Closure Representation §3.3: the stack when scope-bounded, a region when region-bounded, static storage (memref.global) when its lifetime is the whole program, and the heap only when its extent is genuinely dynamic. On a target without a heap, a lazy value that classifies as dynamic SHALL be a compile-time lifetime error, not a heap allocation. Lazy values SHALL NOT be placed on a GC-managed heap.
7. Pure Thunks Initially: Initial implementation SHALL use pure thunk semantics (no memoization)
8. Single-Forcer Memoization: A memoizing lazy value SHALL be forced under a single-forcer discipline: for each lazy value, exactly one semantic forcer performs the transition from unevaluated to computed. A lazy value whose force sites span threads or actor boundaries SHALL carry an ownership obligation discharged at compile time by establishing that single semantic forcer. This discipline keeps the write-once conditions on computed at [0] and value at [1] quantifier-free: each slot is written at one statically identified site, so the verification conditions quantify over enumerated structure only (Closure Representation §11).

12. Implementation in CCS/Composer Pipeline

12.1 CCS Phase

1. checkLazy in Coordinator.fs:

   • Checks the lazy body expression
   • Computes captures via computeCaptures
   • Creates SemanticKind.Lambda with LambdaContext.LazyThunk
   • Creates SemanticKind.LazyExpr with captures list

2. computeCaptures in Applications.fs:

   • Collects VarRefs in body
   • Excludes parameter names
   • Excludes module-level bindings (IsModuleLevel = true)
   • Returns CaptureInfo list

12.2 Alex Preprocessing Phase

1. SSAAssignment (interim — this computation is a closure-hyperedge consequence and moves into CCS; Closure_Retooling_Plan):
   • Computes LazyLayout for LazyExpr nodes
   • Computes ClosureLayout for thunk Lambda nodes
   • Assigns SSAs for all construction operations

12.3 Witness Phase

1. LazyWitness:

   • Observes LazyLayout coeffect
   • Emits struct construction operations
   • Emits thunk function definition

2. BindingWitness:

   • Handles functions returning lazy values
   • Uses getActualFunctionReturnType for correct lazy struct type

References

• Tofte, M., & Talpin, J.-P. (1997). Region-Based Memory Management. Information and Computation.
• Elsman, M. (2021). Programming with Regions in the MLKit. IT University of Copenhagen.
• Appel, A. W. (1992). Compiling with Continuations. Cambridge University Press.
• Shao, Z., & Appel, A. W. (1994). Space-Efficient Closure Representations. LFP ‘94.
• Peyton Jones, S. L. (1987). The Implementation of Functional Programming Languages. Prentice Hall. (Chapter on lazy evaluation)