Esc
Start typing to search...

Algebraic Effects

Keel tracks side effects in the type system: a function's type includes which effects it may perform. You control effects by installing handlers — no monads, no async/await, no checked e-- rejected: the resume is inside a closure let r = handle (get 1) ctl get n -> let f : Int -> Int = |x| resume x resume (f 5)ception machinery required.

Declaring an effect

An effect block defines a named capability and its operations:

effect IO
    readLine  : String
    writeLine : String -> ()

Each operation name becomes a callable in scope when the effect is in scope.

effect Rng
    nextInt : Int -> Int -> Int

Effectful function types

A function that may perform the IO effect writes ->{IO} on the arrow:

fn greet : String ->{IO} ()
fn greet name = writeLine ("Hello, " ++ name)

Multiple effects are comma-separated inside the braces:

fn rollAndLog : Int ->{Rng, IO} Unit
fn rollAndLog max =
    let n = nextInt 1 max
    writeLine (Int.toString n)

A bare -> means no effects (pure). String ->{IO} Unit and String -> Unit are written differently and read differently — but the compiler does not yet keep them apart. Passing a pure function where an effectful one is declared, or the reverse, compiles today with no error. See Declared, not yet enforced below for exactly what is and is not checked.

Calling operations

Operations are called like ordinary functions:

fn askName : String ->{IO} String
fn askName prompt =
    writeLine prompt
    readLine

If readLine and writeLine are called with no IO handler installed, the VM raises UnhandledEffect IO at RUN time, with a hint naming the effect and operation to handle. The compiler does not catch a MISSING handler -- see What IS checked today.

Handling effects

handle runs a body under a handler block. Each arm matches one operation, and the arms must cover EVERY operation of the effect:

effect IO
    readLine  : String
    writeLine : String -> ()

let result =
    handle (askName "Name?")
        writeLine s -> ()
        readLine -> "default"

Tail arms (op args -> body) observe the operation and provide the value it returns. The computation continues with that value, so the arm's body becomes the operation's result.

An arm's parameters are typed from the operation's declared signature: in writeLine s -> () the parameter s is a String, because writeLine is declared String -> (). Use _ for a parameter you do not need:

handle (logAll [1, 2, 3])
    logItem _ -> ()

Control arms (ctl op args -> body) take the continuation themselves. Inside a ctl arm, resume is a one-shot continuation that resumes the paused computation with a given value:

effect Greeter
    greet : String -> String

let mocked =
    handle (greet "Bob")
        ctl greet name -> resume "mocked-greeting"

resume value continues the computation from the point where the operation was called. Each continuation may be used at most once.

resume must be the LAST thing a ctl arm does. An arm that resumes and then continues would need the VM to hand control back to the arm, which it does not do — so code after resume is rejected (ResumeNotInTailPosition) rather than compiled and silently skipped.

resume must also appear directly in the arm — not inside a lambda written in that arm:

-- rejected: the `resume` is inside a closure
let r = handle (get 1)
    ctl get n ->
        let f : Int -> Int = |x| resume x
        resume (f 5)

A closure looks like it defers the resume to whenever it is called, but the arm's continuation is not a value the closure can carry around: the call may happen after the arm has already returned, or never. Lambdas that do NOT resume are fine in an arm, and are the normal way to shape a resumed value:

let r = handle (get 1)
    ctl get n ->
        let double : Int -> Int = |x| x * 2
        resume (double 5)

Effect polymorphism

Higher-order functions like List.map are effect-polymorphic: if the callback performs effects, the map call does too.

An operation is NOT a value, though, so you cannot hand one to List.map directly — List.map writeLine is BareOperationReference (see What IS checked today). Wrap it in a function:

-- List.map : (a ->{| e} b) -> [a] ->{| e} [b]

fn logIt : String ->{IO} ()
fn logIt s = writeLine s

let writeAll : List String ->{IO} List Unit
    = List.map logIt

The effect variable e is inferred from the callback you pass. This means List.map never forces you to make your callback pure — the wrapper is about operations not being first-class values, not about effect polymorphism.

What IS checked today

Plan 217 made handlers RUN and added the compile-time checks that the handle construct itself needs. These are enforced now, each with an exact error:

programerror
a handler missing an arm for one of the effect's operationsNonExhaustiveHandler
an arm naming an operation the effect does not declareUndeclaredEffectOp
one handle whose arms name operations from two effectsMultiEffectHandle
a top-level fn/let/export/import shadowing an operation nameBinderShadowsOperation
an operation sharing a name with an in-scope trait methodOperationShadowsTraitMethod
an operation declared twice in one effect, or two effects sharing a namescope errors
a bare call whose name two in-scope effects declareAmbiguousEffectOp
an operation applied to too few argumentsPartialOperationApplication
an operation of arity > 0 used as a valueBareOperationReference
an operation used with >> or <<OperationInComposition
resume after which more code follows in a ctl armResumeNotInTailPosition
resume outside a ctl armResumeOutsideHandler
resume inside a lambda written in an armResumeNotInTailPosition / ResumeOutsideHandler
a ctl arm that can return without resumingCtlArmMustResume
a handle inside a module functionHandleInsideModuleFunction

A ctl arm must resume on every path

A ctl arm intercepts the operation and has to hand control back. An arm that returns without resuming discards the computation it interrupted, so it is rejected rather than silently dropped:

handle (greet "Bob")
    ctl greet name -> "oops"            -- CtlArmMustResume

handle (greet "Bob")
    ctl greet name ->                    -- fine: every path resumes
        if name == "Bob" then resume "hi" else resume "hello"

"Every path" means both branches of an if and every branch of a case, not merely the last expression.

Where a handle may appear

A handle may not sit inside a module function body. PERFORMING an effect there is fine -- a module function can call an operation freely, and a handle at the call site will catch it:

module Store exposing fetch
    fn fetch : String ->{S} String
    fn fetch k = get k                   -- fine: performs

let r = handle (Store.fetch "key")       -- fine: handles at the call site
    get k -> "MOCK"

Handling inside the module is what is rejected. This is an implementation restriction, not a language design choice; it is tracked in the project's debt register.

A handle handles exactly ONE effect: the PushHandler instruction carries a single effect label. Nest handles to handle several.

An operation is not a VALUE. greet on its own performs a zero-argument operation; for an operation that takes arguments there is no way to write its name without calling it, and it cannot be passed to List.map or composed. That follows from the design choice that calling an operation IS performing it.

Compile-time safety — the EFFECT ROW is still unchecked

Everything above is about the handle construct and operation NAMES. The effect ROW on an arrow — the {IO} in String ->{IO} Unit — is still documentation the toolchain carries faithfully and does not verify. The two programs below still compile today. MEASURED against the current toolchain.

Unhandled effects are intended to be type errors:

fn badFn : Int -> Int
fn badFn x =
    readLine   -- planned: the row {IO} conflicts with the declared pure arrow.

Passing a wrong-effected function where a specific row is expected is intended to be an error too:

fn pureCallback : Int -> Int
fn pureCallback x = x + 1

-- Planned: EffectRowMismatch — pureCallback has row {}, caller expects {IO}.
-- Today: this compiles clean.
let _ = List.map pureCallback someList

Performing an operation with NO handler installed is caught at RUN time, not compile time: the VM raises VmError::UnhandledEffect, and its hint names the effect and operation you need to handle.

Built-in native effects

Native stdlib functions are annotated with their effect rows. Reading a file uses {IO}, HTTP calls use {Net}, spawning a process uses {Proc}, getting the current time uses {Clock}. These appear in the function types you see in documentation and hover tooltips.

Summary

ConceptSyntax
Declare effecteffect Name with op list
Effect row->{IO} on arrow, or ->{IO, Net}
Pure functionbare ->
Call operationopName args (like a function)
Install handlerhandle body with arms
Tail armop args -> body
Control armctl op args -> body
Resume continuationresume value

Declared, not yet enforced

Effect rows are parsed, preserved and rendered — you can write fn greet : String ->{IO} Unit, the formatter keeps it, hover shows it, and it round-trips through the compiler unchanged.

The formatter CANONICALISES a row rather than preserving its exact text: labels are reordered into name order (->{Net, IO} becomes ->{IO, Net}) and an empty row is elided (->{} becomes ->). Both are meaning-preserving — a row is a SET of labels, and ->{} and -> are the same type — and the name ordering is what stops the formatter rewriting one signature because of another one earlier in the file. No label is ever added or dropped.

They are not yet checked. Nothing today rejects a function declared pure that calls an effectful one, nor an undeclared effect label. The row is documentation that the toolchain carries faithfully; enforcement is separate work, tracked in the project's debt register.

The four forms an arrow can take — and the one pair worth keeping straight, because ->{e} and ->{| e} look alike and mean different things:

formmeaning
->{IO}the closed row containing IO
->{IO, Net}a closed row with two labels
->{| e}an OPEN row, polymorphic in e — note the |
->pure, identical to ->{}

Labels are CAPITALISED. e is not a valid label, so ->{e} does not parse at all -- MEASURED, it is a syntax error, not a row containing an effect called e. The label parser accepts only an upper-case identifier, so the row reads zero labels and then fails looking for the closing brace. ->{E} parses fine (a closed row with one label E); ->{| e} parses fine (an open row with the variable e). The PIPE is what introduces a row variable.

One rendering difference worth knowing: :doc List.map shows the DECLARED signature, (a ->{| e} b) -> [a] ->{| e} [b], while a diagnostic about the same function shows (a -> b) -> [a] -> [b]. They are the same function. Inference replaces the row variable e with a fresh INTERNAL one, and an internal tail is suppressed rather than printed, because it has no spelling a user could write back into a file.