By Christian Findlay

Algebraic Effects

An effect declares typed operations. perform invokes the innermost matching lexical handler, which supplies the operation result. Default and ML syntax lower to the same effect, perform, handler, and resume AST nodes; their runtime semantics are identical.

The checker validates declared operations and their value types, infers the operations required by unannotated functions and callbacks, and propagates those requirements through calls. A handler discharges only the operation arms it actually supplies, for the same generic effect instantiation. Every requirement must be discharged before program entry. A missing handler is therefore a compile error, never a runtime abort.

Keywords

effect perform handle in resume

Effect Declarations

effectDecl ::= docComment? "effect" IDENT ("<" typeParamList ">")? "{" opDecl* "}"
opDecl     ::= IDENT ":" fnType

[EFFECTS-OP-TYPING] Every operation named by perform or a handler arm must belong to the declared effect. Perform arguments and handler parameters must match the operation's positional arity; performed values must also match its types. Named arguments are not supported on perform.

effect State {
    get: fn() -> int
    set: fn(int) -> Unit
}
effect State
    get : Unit => int
    set : int => Unit

Generic Effects

[EFFECTS-GENERIC-DECL] An effect may declare type parameters, including in and out variance. The checker validates operation parameters as input positions and operation results as output positions.

effect Stash<T> {
    put: fn(T) -> Unit
    take: fn() -> T
}

[EFFECTS-GENERIC-INSTANTIATION] Each handler site instantiates a generic effect independently. Handler arm values and performs in the handled body must agree on that instantiation. This handler instantiates Stash<string>:

let word = handle Stash
    put value => print(value)
    take => "ready"
in perform Stash.take()

[EFFECTS-GENERIC-RUNTIME] Generic operation payloads use an erased machine-word ABI. Code generation boxes and unboxes values using the type inferred at each site. Static discharge distinguishes resolved instantiations, so a Stash<string> handler does not discharge Stash<int>.put. Runtime handler keys also include the resolved instantiation, such as Stash$string; their null-lookup guard is a defensive backstop and must not be the normal rejection path for a checked program. Monomorphic effects use their declared name as the key.

Effectful Function Types

An effect row follows the return type. It contains one effect reference or a bracketed list; generic references may include type arguments.

effectSet ::= "!" effectRef | "!" "[" effectRef ("," effectRef)* "]"
effectRef ::= IDENT ("<" typeList ">")?
fn read() -> string !IO = perform IO.readLine()
fn fetch(url) -> string ![IO, Net] = perform Net.get(url)
read : Unit -> string !IO
read () = perform IO.readLine

fetch : string -> string ![IO, Net]
fetch url = perform Net.get url

[EFFECTS-GENERIC-ROWS] A row entry such as !Stash<int> pins the generic effect instantiation used by performs in that function body. A bare generic entry leaves its arguments to inference.

[EFFECTS-STATIC-DISCHARGE] Effect annotations are checked contracts, not handlers. Writing !Logger declares which effect the function body may require; it does not authorize Logger.log at the call site and does not discharge that operation. The checker rejects an operation outside a non-empty declared row. It infers requirements when annotations are omitted, propagates them through named calls and higher-order callback calls, and requires the selected program entry (main when present, otherwise the top-level executable statements) to have no remaining operation requirements.

Discharge is operation- and instantiation-specific. A handler for Pair.first does not discharge Pair.second, and a handler inferred as Stash<string> does not discharge Stash<int>.put. Complementary nested partial handlers may each discharge the operation they cover. Constructing a lambda is pure, but invoking it contributes its latent requirements; constructing one inside a handler does not give it authority after it escapes that handler's lexical region.

The current compiler realizes these rules with a closed-program operation summary and fixed-point call analysis. Explicit open effect-row variables are not surface syntax and effect rows are not yet exposed as independently quantified values in the Hindley–Milner type representation.

Performing Operations

performExpr ::= "perform" IDENT "." IDENT "(" args? ")"
fn increment() -> int !State = {
    let current = perform State.get()
    perform State.set((current + 1) ?: current)
    perform State.get()
}

The operation result is the value returned by its active handler arm. The static effect-row check guarantees that a matching handler exists on every execution path.

Handlers

handlerExpr ::= "handle" IDENT handlerArm+ "in" expr
handlerArm  ::= IDENT IDENT* "=>" expr

A handler with no resume expression uses direct value substitution: the arm returns the operation result and execution continues after perform.

let result = handle State
    get => 41
    set value => print("set ${value}")
in increment()

Lookup is per effect and operation. Nested handlers may override selected operations; the innermost matching arm wins and an outer arm remains available for operations not handled by the inner region.

handle Logger
    log message => print("outer: ${message}")
in handle Logger
    log message => print("inner: ${message}")
in perform Logger.log("test")

A handler arm is not permission to perform its own active operation recursively. The checker rejects a perform with the same effect, resolved generic instantiation, and operation as the active arm. A different operation not covered by a partial handler, or a different generic instantiation, may instead be discharged by an enclosing matching handler. Every remaining arm requirement follows the ordinary entry-discharge rule.

Handler-Owned State

[EFFECTS-HANDLER-STATE] A handler arm may capture a mutable binding. Code generation promotes the captured binding to a shared heap cell, so every arm, the handled body, and code after the region observe the same location. This is the sanctioned form of mutation in Osprey: a mut cell is meant to change through an effect handler like the one below, not by free imperative reassignment in ordinary statement position (see Bindings). The checker enforces this boundary: assignment to a mutable binding outside a handler arm is a type error.

mut cell = 0
let result = handle State
    get => cell
    set value => { cell = value }
in increment()
print("result=${result} cell=${cell}")

Handler state is also preserved when a perform crosses a spawned-fiber or HTTP callback boundary. The native conformance cases are tests/regressions/effects/fiber_effects.test.osp and tests/regressions/effects/http_state_levels.test.osp.

Resuming Handlers

[EFFECTS-RESUME] resume(value) supplies the current operation result and runs the rest of the handled computation. It evaluates to that computation's answer, so the arm may execute code after the resumed computation returns. resume() supplies Unit.

resumeExpr ::= "resume" "(" expr? ")"
effect Ask { value: fn() -> int }

let answer = handle Ask
    value => {
        let completed = resume(21)
        print("completed=${completed}")
        completed
    }
in perform Ask.value() * 2

Resuming handlers have these rules:

  • They are deep: the same handler remains installed while the continuation runs.
  • They are single-shot. A second resume of one continuation aborts with fatal: continuation already resumed (multi-shot resume is not supported).
  • Handler mode is selected per region. With no resume in any arm, every arm directly supplies its operation result and the caller continues. If any arm contains resume, returning from the selected branch without resuming stops the suspended computation and its value becomes the result of the whole handler. A single operation arm may intentionally resume its success branch and return from its error branch; that is the exception-style early-exit pattern. The known deviation is across sibling operations: adding resume to one arm also changes a non-resuming sibling from substitution to early exit. This region-wide behavior is tracked as issue #177. Until it is fixed, keep sibling operations in the same mode.
  • resume is lexical to the arm. It is rejected at top level and inside a lambda declared in an arm, because that lambda has no live arm continuation.
  • Explicit resume is native-only. WebAssembly supports direct value-substitution handlers but not the pthread-backed continuation runtime.

Native resume uses one suspended pthread stack as the continuation. Regions whose arms contain no resume stay on the direct handler-call path.

Two critical implementation defects currently limit operation values:

  • issue #182: the native resumable-operation mailbox transports 16 arguments. The compiler accepts a 17th argument, but the runtime silently delivers zero for it.
  • issue #183: a direct handler corrupts an operation result whose type is Result<T, E>. Resuming handlers have separate passing coverage for complete Result values.
  • issue #185: under ARC, a resuming handler leaks one managed object when its completed continuation answer is a dynamic string.

Both defects have paired Default/ML known-failure cases under tests/effects.

[EFFECTS-FIBER-PERFORM] Concurrent performs into one resuming handler are serialized for the full suspend-to-resume round trip. This prevents arguments or results from being delivered to the wrong performer.