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:
| program | error |
|---|---|
| a handler missing an arm for one of the effect's operations | NonExhaustiveHandler |
| an arm naming an operation the effect does not declare | UndeclaredEffectOp |
one handle whose arms name operations from two effects | MultiEffectHandle |
a top-level fn/let/export/import shadowing an operation name | BinderShadowsOperation |
| an operation sharing a name with an in-scope trait method | OperationShadowsTraitMethod |
| an operation declared twice in one effect, or two effects sharing a name | scope errors |
| a bare call whose name two in-scope effects declare | AmbiguousEffectOp |
| an operation applied to too few arguments | PartialOperationApplication |
| an operation of arity > 0 used as a value | BareOperationReference |
an operation used with >> or << | OperationInComposition |
resume after which more code follows in a ctl arm | ResumeNotInTailPosition |
resume outside a ctl arm | ResumeOutsideHandler |
resume inside a lambda written in an arm | ResumeNotInTailPosition / ResumeOutsideHandler |
a ctl arm that can return without resuming | CtlArmMustResume |
a handle inside a module function | HandleInsideModuleFunction |
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
| Concept | Syntax |
|---|---|
| Declare effect | effect Name with op list |
| Effect row | ->{IO} on arrow, or ->{IO, Net} |
| Pure function | bare -> |
| Call operation | opName args (like a function) |
| Install handler | handle body with arms |
| Tail arm | op args -> body |
| Control arm | ctl op args -> body |
| Resume continuation | resume 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:
| form | meaning |
|---|---|
->{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.