lux/docs/EVIDENCE_PASSING.md

Evidence Passing for Algebraic Effects

Overview

Evidence passing is a compilation technique that transforms O(n) runtime effect handler lookup into O(1) direct function calls. This document describes the implementation in Lux.

Background: The Problem

Current Approach (Stack-Based)

When an effect operation is performed, Lux searches the handler stack:

// interpreter.rs:2898-2903
let handler = self
    .handler_stack
    .iter()
    .rev()
    .find(|h| h.effect == request.effect)  // O(n) linear search

For deeply nested handlers or effect-heavy code, this becomes a bottleneck.

Evidence Passing Solution

Instead of searching at runtime, pass handler references directly to functions:

Before (stack lookup):
┌─────────────┐
│   greet()   │ ──► search handler_stack for "Console" ──► call handler
└─────────────┘

After (evidence passing):
┌─────────────┐
│ greet(ev)   │ ──► ev.console.print() (direct call)
└─────────────┘

Design

1. Effect Index Assignment

Each effect type gets a compile-time index:

Effect	Index
Console	0
State	1
Reader	2
Fail	3
...	...

2. Evidence Structure

// Interpreter representation
struct Evidence {
    handlers: HashMap<String, Rc<HandlerValue>>,
}

// C backend representation
typedef struct {
    LuxConsoleHandler* console;
    LuxStateHandler* state;
    LuxReaderHandler* reader;
    // ... other effects
} LuxEvidence;

3. Handler Structures (C Backend)

Each effect becomes a struct with function pointers:

// Console effect handler
typedef struct {
    void (*print)(void* env, LuxString msg);
    LuxString (*readLine)(void* env);
    LuxInt (*readInt)(void* env);
    void* env;  // Captured environment
} LuxConsoleHandler;

// State effect handler
typedef struct {
    void* (*get)(void* env);
    void (*put)(void* env, void* value);
    void* env;
} LuxStateHandler;

4. Function Signature Transformation

Functions that use effects receive an implicit evidence parameter:

Lux source:

fn greet(name: String): Unit with {Console} =
    Console.print("Hello, " + name)

Generated C:

void greet_lux(LuxEvidence* ev, LuxString name) {
    LuxString msg = lux_string_concat("Hello, ", name);
    ev->console->print(ev->console->env, msg);
}

5. Handler Installation

The run ... with {} expression:

Lux source:

run greet("World") with {
    Console {
        print(msg) => resume(builtin_print(msg))
    }
}

Generated C:

// Create handler
LuxConsoleHandler console_handler = {
    .print = my_print_impl,
    .readLine = builtin_readLine,
    .readInt = builtin_readInt,
    .env = captured_env
};

// Create evidence with this handler
LuxEvidence ev = outer_ev;  // Copy outer evidence
ev.console = &console_handler;

// Run body with new evidence
greet_lux(&ev, "World");

Implementation Status

Phase 1: Interpreter Optimization ✅ COMPLETE

Goal: Replace stack search with HashMap lookup.

Changes made to interpreter.rs:

1. Added evidence: HashMap<String, Rc<HandlerValue>> field to Interpreter
2. Modified handle_effect to use O(1) evidence lookup instead of O(n) stack search
3. Updated eval_run to manage evidence:
   • Save previous evidence values before entering run block
   • Insert new handlers into evidence
   • Restore previous evidence after exiting run block

Key code change:

// Before (O(n) search):
let handler = self.handler_stack.iter().rev().find(|h| h.effect == request.effect)

// After (O(1) lookup via evidence):
let handler = self.evidence.get(&request.effect)

Phase 2: C Backend Evidence Infrastructure ✅ COMPLETE

Goal: Generate evidence types for future use.

Changes made to c_backend.rs:

1. Added handler struct types to prelude:

   • LuxConsoleHandler with print/readLine function pointers
   • LuxStateHandler with get/put function pointers
   • LuxReaderHandler with ask function pointer

2. Added LuxEvidence struct containing pointers to handlers

3. Added default handlers that delegate to built-in implementations

4. Added default_evidence global with built-in handlers

Phase 3: C Backend Evidence Threading ✅ COMPLETE

Goal: Thread evidence through effectful function calls.

Changes made to c_backend.rs:

1. Track effectful functions in effectful_functions: HashSet<String>
2. Add has_evidence: bool flag to track context
3. For effectful functions:
   • Add LuxEvidence* ev parameter to forward declarations
   • Add LuxEvidence* ev parameter to function definitions
4. Transform effect operations:
   • When has_evidence is true: ev->console->print(ev->console->env, msg)
   • When has_evidence is false: lux_console_print(msg) (fallback)
5. Update function calls:
   • Effectful calls inside effectful functions: pass ev
   • Effectful calls outside: pass &default_evidence
6. Update main function generation to pass &default_evidence

Example generated code:

// Function signature includes evidence
void greet_lux(LuxEvidence* ev) {
    // Effect operations use evidence
    ev->console->print(ev->console->env, "Hello, World!");
}

int main(int argc, char** argv) {
    // Entry point uses default evidence
    greet_lux(&default_evidence);
    return 0;
}

Performance Characteristics

Metric	Stack-Based	Evidence Passing
Handler lookup	O(n)	O(1)
Memory overhead	Stack grows	Fixed-size struct
Function call overhead	None	+1 pointer parameter
Effect invocation	Search + indirect call	Direct call

Expected speedup: 10-20x for effect-heavy code (based on Koka benchmarks).

References

• Generalized Evidence Passing for Effect Handlers - ICFP 2021
• Effect Handlers, Evidently - ICFP 2020
• Koka Language