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 exception machinery required.

Declaring an effect

An effect block defines a named capability and its operations:

effect IO
    readLine  : String
    writeLine : String -> Unit

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} Unit
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). ->{IO} and -> Unit are different types — you cannot pass a pure function where an effectful one is expected, or vice versa.

Calling operations

Operations are called like ordinary functions:

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

If readLine and writeLine are not in scope (no IO handler installed), the compiler reports UnhandledEffect IO.

Handling effects

handle runs a body under a handler block. Each arm matches one operation:

let result =
    handle (greet "Alice")
        writeLine s -> ()
        readLine -> "default"

Tail arms (op args -> body) observe the result of the operation and provide a value to the caller. The computation continues with that value.

Control arms (ctl op args -> body) intercept the operation before it returns. Inside a ctl arm you have access to resume, a one-shot continuation that resumes the paused computation with a given value:

let logged =
    handle (greet "Bob")
        ctl writeLine s ->
            let _ = log ("output: " ++ s)
            resume ()
        ctl readLine ->
            resume "mocked-input"

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

Effect polymorphism

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

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

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

The effect variable e is inferred from the callback you pass. This means List.map never forces you to make your callback pure.

Compile-time safety

Unhandled effects are type errors:

fn badFn : Int -> Int
fn badFn x =
    readLine   -- compile error: UnhandledEffect IO

Passing a wrong-effected function where a specific row is expected is also an error:

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

-- Error: EffectRowMismatch — pureCallback has row {}, caller expects {IO}
let _ = List.map pureCallback someList

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