15 Effects — the marks an op leaves on the world

15.1 Effects are closed words#

An effect is an influence an op has on the outside. Authors cannot invent new effects; the list is fixed by the language.

The nine io, alloc, heap, state, panic, atomic, concurrent, wait and unsafe have primitives that actually produce them, and the compiler enforces them — a body that does it must say so, and saying it without doing it is reported. The other six (lock, device, page_fault, blocking, cancel, detach) have no primitive yet. They are accepted as declarations and spread to callers, but whether the body really does it cannot be asked. A word not on the list is rejected.

module undef .
rem expect: E-EFFECT-UNDEF

proc checked input x u64 . output u64 . effects crash .
do
  return x .
end

$ lowentc --check undef.low
undef.low:4:0 E-EFFECT-UNDEF: unknown effect (the vocabulary is closed: none/alloc/heap/io/wait/concurrent/lock/atomic/unsafe/device/page_fault/blocking/cancel/detach/panic/state) — a typo here silently declares the op PURE

Quietly accepting a typo would make that op read as having no effect — the case the diagnostic describes as “a typo here silently declares the op PURE”.

15.2 Effects spread to the caller#

Calling an op adds its effects to the caller’s. Performing more effects than declared is rejected.

module spread .
rem expect: E-EFFECT

proc log_line input out cap io . input msg slice u8 . output u64 . effects io .
do
  return write_out out 1 msg .
end

proc compute input out cap io . input x u64 . output u64 . effects panic .
  requires le x 1000 .
do
  let n u64 be log_line out "computing\n" .
  if eq x 0 . do
    panic "zero" .
  end
  return mul x 2 .
end

$ lowentc --check spread.low
spread.low:11:1 E-EFFECT: this op performs `io`, which its `effects` clause does not declare — add it to `effects …`, or stop calling what needs it

compute declares only effects panic ., but calls log_line and so also performs io. The diagnostic says “add it to effects, or stop calling what needs it”. Conversely, the layers effects do not spread into are clear too.

module layered .
rem run: main

fn celsius_to_f input c i64 . output i64 .
  requires ge c -1000 .
  requires le c 1000 .
do
  return add (div (mul c 9) 5) 32 .
end

proc print_digit input out cap io . input d u8 . output u64 . effects io .
  requires le d 9 .
do
  let buf slice u8 be "0123456789" .
  return write_out out 1 (subslice buf (widen u64 d) (add (widen u64 d) 1)) .
end

proc main input out cap io . output u8 . effects io .
do
  let f i64 be celsius_to_f 100 .
  let n u64 be print_digit out (narrow u8 (mod f 10)) .
  let m u64 be write_out out 1 "\n" .
  return 0 .
end

$ lowentc --run main layered.low
2
main() = 0

celsius_to_f is a pure fn and can be called anywhere. print_digit performs io, so it can be called only from main, which declares io. The computing layer and the layer that touches the outside separate in the head. Good design keeps the pure layer wide and the effectful layer thin.

15.3 Declared but not done is reported#

Declaring an effect that is never performed is also a problem, because a declared effect is a cost the caller must bear.

module over .
rem expect: W-EFFECT-OVER

proc double input x u64 . output u64 . effects panic .
  requires le x 1000 .
do
  return mul x 2 .
end

$ lowentc --check over.low
over.low:6:1 W-EFFECT-OVER: this op DECLARES `panic` but never PERFORMS it. A declared effect is a cost the caller must budget for (a pure caller cannot call an `io` op). Drop it, or — if a future version will perform it — say so (RFC-0007)

double says it may stop, but it never stops. Then every op calling it must declare panic, and pure fns cannot call it — it exaggerated what it does. The diagnostic says to remove it, or to say so if a future version will actually perform it.

15.4 The effects line is a set#

The effects line is a set, not a list. Writing the same word twice is rejected.

module dup .
rem expect: E-EFFECT-DUP

proc checked input x u64 . output u64 . effects panic panic .
do
  if eq x 0 . do panic "zero" . end
  return x .
end

$ lowentc --check dup.low
dup.low:4:0 E-EFFECT-DUP: an effect atom appears more than once in the `effects` clause — the row is a SET, not a list. A repeat says nothing the first one didn't, and the reader has to decide it's noise (RFC-0057 E3)

The second panic says nothing the first did not. none cannot appear with any other atom.

module nonemix .
rem expect: E-EFFECT-NONE-MIX

proc checked input x u64 . output u64 . effects none panic .
do
  if eq x 0 . do panic "zero" . end
  return x .
end

$ lowentc --check nonemix.low
nonemix.low:4:0 E-EFFECT-NONE-MIX: `none` sits in the `effects` clause ALONGSIDE a real effect — `none` means this op performs no effects, so it cannot co-occur with one. Say the effects, or say none; not both (RFC-0057 E2)

An op cannot both have effects and have none; write the effects or write that there are none. And a fn does not even carry effects none (chapter 5).

Some effects bring others with them. Today there is one such rule — writing concurrent counts as writing wait too, since waiting for another flow’s progress may mean being suspended. Two sets are therefore compared after applying this closure. Writing concurrent means wait need not be written separately, but writing only wait and doing something concurrent is rejected.

15.5 via — a type argument decides the effects#

Generic containers are in an awkward spot, because their effects depend on which allocator they receive. Opened on a bump allocator over borrowed bytes, the effect is just state; opened on an allocator standing on the growing heap, heap appears. Always declaring the largest effect any allocator could produce is a lie, and declaring only the smallest is a hidden allocation.

export proc append
  input comptime t type .
  input comptime a type .
  input g mut vec t a .
  input x t .
  output bool .
  effects state via a .
  requires allocs.byte_allocator a .

This is the head of append in the standard library’s vecgen. effects state via a . means “the allocation-family effects (alloc, heap, atomic) declared by the ops of type a are also this op’s declaration”. Each monomorphised instance has its effects decided by that type. Generic containers return in chapter 34.

15.6 What purity allows#

A fn — an op whose effects are none — satisfies three properties.

• The same inputs always give the same result.
• Changing the order of calls does not change the program’s result.
• If its result is unused, it need not be called.

These three allow optimisations. Two pure calls with the same arguments can be reduced to one (common-subexpression elimination), results can be remembered (memoisation), unused calls can be removed, and calls that do not depend on each other can be reordered or split up. That these optimisations do not change a program’s meaning is proven in Coq (chapter 44). Call boundaries and the timing of traps are outside that proof.

15.7 Common mistakes#

module mistake_fnpanic .
rem expect: E-EFFECT-CALC

rem ✘ a pure `fn` uses `panic` --- stopping the program is an effect too
fn nonzero input x u64 . output u64 .
do
  if eq x 0 . do panic "zero" . end
  return x .
end

$ lowentc --check mistake_fnpanic.low
mistake_fnpanic.low:6:1 E-EFFECT-CALC: this fn is declared pure but performs `panic` — make it a `proc` with `effects …`, or remove the effect

module fnpanic_fixed .
rem run: nonzero_checked 5
rem trap: nonzero_strict 0

rem fix 1 --- a `proc` that declares stopping as an effect
proc nonzero_checked input x u64 . output u64 . effects panic .
do
  if eq x 0 . do panic "zero" . end
  return x .
end

rem fix 2 --- move the condition into a contract and it stays a `fn`
fn nonzero_strict input x u64 . output u64 .
  requires ne x 0 .
do
  return x .
end

$ lowentc --run nonzero_checked fnpanic_fixed.low 5
nonzero_checked(5) = 5
$ lowentc --run nonzero_strict fnpanic_fixed.low 0
== ir diagnostics (1) ==
0:0 E-VM-CONTRACT: `requires` violated at entry — the caller broke the contract

module mistake_fnmutwrite .
rem expect: E-EFFECT-PURITY

rem ✘ a `fn` writes into the caller's slice received as `mut`
fn clear input xs mut slice u8 . output void .
do
  var i u64 be 0 .
  while lt i (len xs) do
    set (index xs i) 0 .
    set i (add i 1) .
  end
end

$ lowentc --check mistake_fnmutwrite.low
mistake_fnmutwrite.low:5:0 E-EFFECT-PURITY: a `fn` WRITES through a `mut` parameter — that write is visible to the CALLER. A fn is an enforced purity contract (SPEC-003 §27): callers may memoise it, reorder it, or elide it. An op that changes caller-owned storage can do none of those. Declare it a `proc`. (Local mutation stays pure: storage confined to the op is not observable — a machine write is not an observable effect. RFC-0057)

module mistake_effcomma .
rem expect: E-VOCAB-REMOVED

rem ✘ a comma between effects --- just separate the words with spaces
proc greet input out cap io . input x u64 . output u64 . effects io, panic .
do
  if eq x 0 . do panic "zero" . end
  return write_out out 1 "hi\n" .
end

$ lowentc --check mistake_effcomma.low
5:68 E-VOCAB-REMOVED: `,` (R3) was removed — RFC-0103, 2026-08-27. It opened the NEXT operand of the same form, but nothing used it that way: every `,` in the corpus was a LINE CONTINUATION, and newlines no longer close a form, so continuing a line needs nothing at all. A form is `head operand*` and ends at its closer `.` — just write the operands, on as many lines as you like.

module pure_local .
rem run: sum_to 10

rem still pure with `var` and `set` --- the changes are visible only inside this op
fn sum_to input n u64 . output u64 .
  requires le n 1000 .
do
  var s u64 be 0 .
  var i u64 be 0 .
  while le i n do
    set s (add s i) .
    set i (add i 1) .
  end
  return s .
end

$ lowentc --run sum_to pure_local.low 10
sum_to(10) = 55

module fn_can_stop .
rem run: first [7,8]
rem trap: first []

rem a pure `fn`, yet it stops on an empty slice --- a bounds-check stop is not an effect the op performs
fn first input xs slice u8 . output u8 .
do
  return index xs 0 .
end

$ lowentc --run first fn_can_stop.low [7,8]
first([7,8]) = 7
  arg0 (written) = [7,8]
$ lowentc --run first fn_can_stop.low []
== ir diagnostics (1) ==
0:0 E-VM-BOUNDS: slice index out of bounds (panic)

module mistake_blocking .
rem expect: E-EFFECT-CALC

rem blocking: the head says it may hold the flow of execution
proc wait_for_device output u64 . effects blocking .
do
  return 0 .
end

rem ✘ a pure fn calls an op that may hold the flow; in this edition it slips through
fn ready output u64 . do
  return wait_for_device .
end

$ lowentc --check mistake_blocking.low
mistake_blocking.low:11:23 E-EFFECT-CALC: this fn is declared pure but performs (이름 없는 효과 비트) — make it a `proc` with `effects …`, or remove the effect

module blocking_wait .
rem expect: E-EFFECT-CALC

rem wait does spread; the same shape is refused with E-EFFECT-CALC
proc wait_for_device output u64 . effects wait .
do
  return 0 .
end

fn ready output u64 . do
  return wait_for_device .
end

$ lowentc --check blocking_wait.low
blocking_wait.low:6:1 W-EFFECT-OVER: this op DECLARES `wait` but never PERFORMS it. A declared effect is a cost the caller must budget for (a pure caller cannot call an `io` op). Drop it, or — if a future version will perform it — say so (RFC-0007)
blocking_wait.low:10:23 E-EFFECT-CALC: this fn is declared pure but performs `wait` — make it a `proc` with `effects …`, or remove the effect

15.8 This chapter’s syntax at a glance#