# 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:

```rust
// 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

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

```c
// 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:

```c
// 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:**
```lux
fn greet(name: String): Unit with {Console} =
    Console.print("Hello, " + name)
```

**Generated C:**
```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:**
```lux
run greet("World") with {
    Console {
        print(msg) => resume(builtin_print(msg))
    }
}
```

**Generated C:**
```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:**
```rust
// 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 🔜 PLANNED

**Goal:** Thread evidence through effectful function calls.

**Required changes:**

1. Add `LuxEvidence* ev` parameter to effectful functions
2. Transform effect operations to use `ev->console->print(...)`
3. Generate handler structs for user-defined handlers in `run` blocks
4. Pass evidence through call chain

## 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](https://xnning.github.io/papers/multip.pdf) - ICFP 2021
- [Effect Handlers, Evidently](https://www.dhil.net/research/papers/effect_handlers_evidently-draft-march2020.pdf) - ICFP 2020
- [Koka Language](https://koka-lang.github.io/koka/doc/book.html)