hanki

6. Effects

Effects are typed markers. They are checked statically. They are not algebraic - there is no handle/with; you cannot intercept io.print! at runtime.

Built-in effects:

EffectMeaning
[io]standard input/output
[net]network access
[fs_read]reading the filesystem
[fs_write]writing the filesystem
[db]embedded database access (see stdlib/extra/sqlite.hk); covers :memory: databases too
[process]subprocess spawn (see stdlib/extra/process.hk)
[time]reading the clock / sleeping
[env]environment-variable reads
[random]random-number generation
[throws E]may throw an error of type E
[state]inside an actor handler; reads/writes actor state

Multiple effects: [io, throws ParseError].

[fs] is an alias for [fs_read, fs_write] - sugar you may write in an effect row or an --allow/--deny atom, expanded to the two base atoms wherever effect names are interned. So --allow fs_read grants a read-only filesystem (a writer is refused), while [fs] on an action that both reads and writes is shorthand for declaring both.

User-defined effect groups:

struct Rows
  affected: i32
end

effect Database
  def query(sql: string) -> Rows
  def exec(sql: string) -> ()
end

The ops inside an effect block are declared as def (no !, no body - they are signatures, not implementations). At a call site they implicitly carry the [Name] effect, so the caller must declare it:

def run!() -> () [Database]
  exec("DELETE FROM things")    # legal: caller has [Database]
end

An op is bare-callable only within its declaring module or where that module is opened - like every other top-level name it lives at its module-qualified name (§14), so it is never a bare global that could collide with or shadow a same-named identifier in a file that did not open it (this matters because the stdlib is merged into every program). Unlike a function, an op is reachable only bare - there is no module.op qualified-call form; a file that wants another module's ops writes open db. Within its own module an op call is bare (exec(…) above), as is the matching provide op name.

Providing user effects - provide. An effect block gives its ops signatures, not behavior; a provide block binds the implementations:

provide Database [net]
  def query(sql: string) -> Rows
    Rows(affected=0i32)          # ordinary action body; its budget is [net]
  end
  def exec(sql: string) -> ()
    ()
  end
end

Effect variables. A function that performs whatever its callback performs is polymorphic in that callback's effects. Write the row as a single lowercase letter - an effect variable - in the callback's type, and again in the function's own row:

def apply_twice!(x: T, f: (T) -> () [e]) -> () [e]
  f(x)
  f(x)
end

e stands for whatever effects the callback performs. (A single lowercase letter is an effect variable exactly as a single uppercase letter is a type parameter - §11; built-in effects like io are multi-letter, so the two never collide.) Invoking f in the body charges [e], which apply_twice! declares. At each call site e is solved to the concrete effects of the callback passed for f and folded into the caller's required set - passing a closure that performs [io] charges the caller [io]; a pure callback charges nothing. A row may combine concrete effects with a variable, -> () [fs, e]: "I touch the filesystem, plus whatever the callback does." A variable may be forwarded - a higher-order action can pass its [e] callback on to another [e] action, and the row stays open until the outermost call site.

Effect-annotated function types. A function type may carry an effect row after its return type, exactly like a def: (T) -> () [io], (string) -> i32 [throws ParseError]. The row is the effects a value of that type performs when called. This matters wherever a function is stored or returned rather than invoked in place - a struct field, an annotated let, a function's return type:

struct Handlers
  on_event: (Event) -> () [io]   # calling on_event performs [io]
end

A variable row is not a concrete contract. A value whose type carries an effect variable may be invoked in place or forwarded to another polymorphic parameter, but it cannot be stored in a struct field, returned through a concrete return type, or bound to an annotated let - those slots demand a fixed row. Storing one is a compile error: a polymorphic callback could perform anything, so a later invocation from a pure or under-declared context would launder its effects. Use a concrete row ([io]) to store a real callback; keep the variable to call or forward it.

The package-manifest wire format encodes these rows on function-typed components of an exported signature, and the load-time compatibility check (module.load!<T>) compares them, so a callback slot's effects are enforced across a shared-module boundary. Source-level cross-package import reconstructs an imported signature by re-parsing and re-checking the dependency's cached source: hanki build resolves each declared universe dep into the content-addressed cache and binds use <alias> to that package's cached <alias>.hk module, so callers are checked against the dependency's real definitions (a fetched universe dep is inert source and carries no .hanki_manifest). Resolution is transitive: a resolved dependency's own manifest resolves too, and its own use binds its declared deps — each package sees only its own manifest's aliases, never the consuming project's, so a dependency's non-sibling use of an undeclared name stays an unresolved-import error rather than a silent reach into the project's deps. One version per source holds graph-wide (§21). Known limitation (tracked): as elsewhere in the manifest, a throws E payload is compared by name only (throws), not by error type.

Encapsulated purity - @encapsulated

! carries two distinct meanings. A world effect - a non-empty row (io/fs/net/db/process/time/env/random/throws E/Crash) - is a real, observable interaction. But an action with an empty effect row is ! only because it is not substitutable: BytesBuilder.push! mutates a builder, a BytesReader read advances a cursor (§4) - no world effect, yet two calls differ, so the operation carries !. A pure def cannot call any !, so this second class infects pure contexts (meta, where-invariants, content-hashing) even for code that is genuinely externally pure: a local builder created, written, and finalized inside a function never escapes, so the function is a pure function of its inputs.

@encapsulated is a def-level attribute marking a def (no !, externally pure) that may call empty-effect-row actions internally. The checker proves external purity from three rules; nothing is trusted:

  1. Empty-effect-row actions only. The body may call !-actions whose row is empty; any call to an action with a non-empty row - or any throw - is a compile error (H0607). The encapsulated def's own row is therefore empty: it performs no side effect, throw, or crash. World-effect safety is wholly untouched - you cannot launder one.
  2. No mutable inputs (H0609). Every parameter (and self) must be deeply immutable - the same lattice as rule 3. A def cannot capture an enclosing binding and there is no ambient global mutable state, so immutable parameters guarantee that every mutable value the body touches was allocated inside the function; the body can therefore only ever mutate local state. A foreign mutable is rejected outright rather than origin-tracked, because even reading one (advancing a cursor) is non-substitutable. So a helper that mutates a passed-in builder stays an ordinary empty-effect-row action - the @encapsulated boundary sits at the entry point that owns the builder.
  3. Deeply-immutable result. The return type must be transitively free of anything mutable - no resource, no live BytesBuilder/BytesReader, no Future - so no mutable alias to internal state escapes (H0608). Finalized bytes (Arc-shared, immutable) qualifies; a builder does not.

With all three, the function's only observable behavior is return = f(inputs): referentially transparent by construction, so a pure context may call it and the optimizer/comptime evaluator may treat it as any pure def (the usual non-termination caveat aside). It is the lightweight, checked subset of uniqueness/region types - Hanki's runST without the rank-2 machinery.

@encapsulated
def join_bytes(a: bytes, b: bytes) -> bytes
  buf = BytesBuilder.new!()   # rule 2: the builder is allocated *here*
  buf.extend!(a)              # rule 1: extend! is an empty-effect-row action
  buf.extend!(b)
  buf.finish!()               # rule 3: only the immutable bytes escapes
end

join_bytes has no !: it is callable from meta, where-invariants, and other pure code. The full design - the immutability lattice, the optimizer-soundness argument, and why serialization needs no Encode/@derive change - is in [docs/design/encapsulated.md](docs/design/encapsulated.md).

Debugging & observability

Hanki's stance is observe, don't interrupt - and every diagnostic tool writes to stderr, the developer channel outside the effect-tracked contract with the world. Three tools cover it: inline print with dbg! (the one effect exemption, below), and live actor observation with sys.actors! and sys.get_state!, following the BEAM observe, don't stop model. For a bug you can capture rather than watch live, the complement is deterministic replay: hanki run --deterministic (and hanki test --deterministic) serializes the actor threads through a seeded scheduling gate, so the interleaving - and therefore the program's output bytes - is a pure function of (program, inputs, seed). --seed N picks a different interleaving (and implies --deterministic); the bare flag runs the canonical seed-0 schedule. The gate yields at every actor park point (mailbox wait, blocking send, await, actor.await_timeout!, spawn, time.sleep!) and at every sys.* OS-seam crossing, so seeds steer the order of observable effects, not just of message dispatches. Time is virtual under the gate: time.sleep! parks the actor on a deterministic clock that advances to the earliest sleeper's deadline only when no actor can run - a deterministic run sleeps in zero real time, and actors that are merely sleeping never count toward a deadlock. actor.await_timeout! deadlines live on the same clock, so a timed-out await also costs no real time and can never be misreported as deadlocked. Clock reads - time.now_ms! and time.monotonic_ms! - draw from this same virtual clock, so even a program that prints timestamps replays byte-for-byte under a fixed seed. Two things follow: a flaky interleaving bug reproduces exactly by replaying its seed, and a schedule on which every live actor is blocked is detected as a deterministic deadlock - reported to stderr instead of hanging (hanki run exits 251; a deadlocking test records one failure and the suite continues). Three scoping notes: external nondeterminism (subprocess output, network peers, stdin) is an input, not an interleaving - same bytes holds only when inputs are fixed; an actor blocked inside a slow OS call (a stdin read, a subprocess) holds its turn, pausing every other actor until the call returns; and actors that rendezvous through the OS rather than the mailbox (e.g. one actor's net server read blocking on another actor's write) can self-deadlock under the serialized schedule, since the gate only understands mailbox-level waits. Both tiers run it: hanki run/hanki test take --deterministic/--seed, and an AOT-compiled binary reads the same through HANKI_DETERMINISTIC=1 / HANKI_SEED=N in the environment (so a compiled program's main(args) argv stays untouched). The gate, the park points (mailbox wait, send, await, spawn, time.sleep!, and every sys.* OS-seam crossing), the virtual clock, and the seeded random stream are the tier-agnostic rtcore core, so a given seed replays byte-identically on both tiers - an AOT binary and hanki run produce the same interleaving for the same seed.

There is deliberately no stop-the-world step debugger. Hanki's bug classes are logic - caught up front by types, effects, and dbg! - and concurrency / lifecycle, which need observation, not stepping: stepping distorts the actor timing the bug depends on, and stop-the-world fits a share-nothing actor language poorly. Live-attach tooling beyond those two readouts - tracing, remote shell, state-replace - is staged by cost and extends this observe model rather than replacing it.

Debug-trace exemption - dbg!

dbg!(expr) is the one compiler-blessed exemption from effect propagation. It evaluates expr, prints [file:line] <source> = <value> to stderr, and returns the value unchanged - so it is drop-in around any subexpression (let y = dbg!(f(x)) + 1) and may be called from a pure function without forcing [io] onto its callers:

struct Point
  x: i32
  y: i32
end

def slope(p: Point) -> Option<i32>   # pure — no effect row
  dbg!(p)                            # stderr: [main.hk:7] p = Point(x=3, y=4)
  p.y.checked_div(p.x)               # a runtime divisor goes through checked_div (§3)
end

The rationale: effects track a program's semantic contract with the world (stdout, net, fs, throws); dbg! writes to a developer diagnostic channel outside that contract. Purity tracking and debug observation are orthogonal, and the exemption keeps them so - the same place every effect/purity-disciplined language ends up (Haskell Debug.Trace, Koka trace, Rust dbg!). The ! spelling is intentional: it reads as an action, so no one mistakes it for pure logic, and it flags itself for removal.

It renders any value structurally - structs (with field names), sum variants, lists, primitives - with no Display impl required; the names come from the argument's static type, which the runtime value representation itself erases.

dbg! works on both tiers: hanki run, hanki test, the REPL, and hanki build all accept it, and it renders identically (the AOT runtime shares the bytecode tier's structural renderer). It is not gated out of built artifacts - keeping it out of shipped code is the author's discipline, like any other stderr write. An un-monomorphised generic parameter still renders structurally: the compiler threads each rendered type parameter's concrete shape from the call site as a hidden shape witness, so dbg!(x: T) - or a nested dbg!(xs: List<T>) - prints field/variant names on both tiers, even though the bytecode tier lowers one generic body. *The narrow positional fallbacks: a type parameter that never appears as a direct value parameter (only nested in one, e.g. m: Map<K, V> with no k: K/v: V), and a generic function used as a first-class value (f = show!, called indirectly).*

Actor introspection - sys.actors!

sys.actors!() prints a one-line-per-actor table of the live actor system to stderr - each registered actor's id, class (when known), liveness, mailbox depth/capacity, and supervisor - then returns ():

def main!() -> () [io]
  sys.actors!()
end

Output on stderr:

actors (1):
  #0 <none> alive mailbox 0/1024 supervisor <root>

Unlike dbg!, it is not effect-exempt: it is an ordinary [io] action - it observes runtime structure and writes a diagnostic - so it carries [io] like any other output and cannot be called from pure code. It works on both tiers (bytecode and AOT), each labelling a spawned actor with its class name; the bare program actor (the root) has no class and shows <none>. It is structural only: it never reads an actor's state - live state inspection is sys.get_state!, below.

Live actor state - sys.get_state!

sys.get_state!(handle) prints the current state of one running actor - addressed by its ActorRef<T> handle - to stderr, its state fields rendered as a struct (field names recovered from the actor's static type, values rendered as dbg! would), then returns (). It is the live counterpart to the crash-time state dump (below): the same renderer, triggered on demand against a running actor rather than a dying one.

actor Counter
  state n: i32 = 0

  on increment() -> ()
    n += 1
  end
end

def main!() -> () [io, throws actor.SendFailed]
  c = spawn Counter
  c.increment()
  sys.get_state!(c)   # stderr: actor #1 (Counter): state: Counter(n=1)
end

The snapshot is taken at the actor's next inter-handler safe point: a priority request the actor services ahead of its pending mailbox messages, in the gap between handler runs. State is never reached for from another thread - Hanki actor state is share-nothing, and this preserves that (the BEAM observe, don't stop model). Outcomes other than a clean snapshot are reported on stderr, never by blocking:

Like sys.actors!, it is an ordinary [io] action (not a dbg!-style exemption) and works on both tiers. It is spelled get_state!, not state!, because state is a keyword.

Divergence - crash!

crash!(msg: string) -> Never is the divergence primitive: it never returns. Reach for it on a branch you have proven unreachable - the "this can't happen" assertion the type system can't express:

type Color
  Red
  Green
  Blue
end

def render!(c: Color) -> string [Crash]   # an action — a pure `def` cannot crash
  match c
    Red   -> "red"
    Green -> "green"
    _     -> crash!("Color had an impossible variant")
  end
end

Its result type is Never (§4), which coerces to any expected type, so a crash!(...) fits any arm without a placeholder. It carries the Crash effect - its own uncatchable effect atom, written in the effect row (e.g. [io, Crash]) - so a pure def (empty effect row) cannot call it: pure functions are total, they never crash. Crash takes no type parameter (unlike throws E), because it cannot be caught: catch e: Crash is a compile error.

When reached, crash! terminates like any other runtime fault (§15), not as a throw: inside an actor it kills that actor and fires its supervisor's on actor_died; at the program root it exits 252 printing crash: <msg>; under hanki test it fails the current test. It is a production construct, valid on both tiers (bytecode and AOT).

Typed holes - ???

??? is a typed hole: a placeholder for code you have not written yet. It type-checks anywhere an expression is expected - its type is Never (§4), so, like crash!, it coerces into any position - but unlike crash! it is effect-free: a hole charges no effect (not even Crash), so it is legal in a pure def as readily as in an action. Sketch the shape of a program and leave the gaps as holes:

def parse_user!(line: string) -> Result<User, FormError> [io]
  fields = ???              # what goes here?
  ???
end

hanki check type-checks the surrounding program and, for every hole, reports the type the context expects there and the effect budget - the effects permitted at that point:

parse_user.hk:2:12: hole[H0250]: this hole expects `List<string>`; effect budget here: [io]
parse_user.hk:3:3: hole[H0250]: this hole expects `Result<User, FormError>`; effect budget here: [io]

This drives spec-first development: write the types, let the compiler dictate each gap, fill it to fit. Holes are non-blocking - a program full of holes still type-checks (hanki check exits 0, reporting each hole as advice, severity hole on the --format=json envelope), runs, and builds. A hole has no runtime value, so if execution reaches one it diverges exactly like crash!: it prints crash: hole reached and exits 252, on both tiers. Fill holes in before shipping - the same discipline that keeps dbg! and crash! out of finished code.