Hanki quickstart for AI agents

A compact bootstrap reference. Read this once and you can write Hanki. Deep dives and the full stdlib: https://hanki-lang.org/HANKI.md

Hanki is a statically typed language with Ruby and Crystal flavoured syntax, Erlang style actors, and typed effect markers. Pure functions and actions share the keyword def, and the ! suffix on the name tells the two apart.

The toolchain has two tiers over one front end: a bytecode interpreter with a REPL (hanki run), and an ahead-of-time LLVM compiler (hanki build). Both are production modes.

There are no warnings. Every diagnostic the toolchain prints is an error that fails the command, and a green command had nothing to say. There is no warning level to configure or suppress.

Requested information is not a diagnostic. --explain-copies advice and ??? typed holes answer a question you asked, and a note: line reports what the toolchain did. Holes remain non-blocking for check, the LSP and the REPL; executable commands reject them by default (§6). A module the entry cannot reach is error[H0627] and fails check and test; the manifest's exclude list names the modules a project leaves unreachable.

use io

def greet(name: string) -> string
  "Hello, #{name}"
end

def main!(args: List<string>) -> () [io]
  io.print!(greet("world"))
end

1. The ! suffix rule (read this first)

An identifier may end in ! or ?, and the suffix is part of the name.

• foo! is an action and may have side effects. Declare it def name!, and spell the ! at every call site.
• foo? is a predicate, enforced as H0621: a pure def or prop returning bool must end in ?, and a ? name must return bool. Write empty? and contains?; is_empty and is_empty? are both wrong. An action is exempt, since a name takes one suffix character and the ! has spent it. stdin_tty! returns bool and takes no ?.
• foo with no suffix is a pure function and cannot call any action.

Calling an action requires that the caller be an action. Pure code cannot reach a side effect, even transitively, and the type checker enforces it.

use io

def pure_add(a: i32, b: i32) -> i32
  a + b              # OK
end

def add_and_log!(a: i32, b: i32) -> i32 [io]
  io.print!("adding")   # OK — caller is an action
  pure_add(a, b)        # OK — calling pure from impure is fine
end

def bad_pure(a: i32) -> i32
  io.print!("hi")    # ERROR: pure fn cannot call an action
  a
end

The three layers

One effect system, the effect row […] of §7, spans three layers.

1. Pure functions, def foo, with no effects.
2. Actions, def foo!, with synchronous effects. This is the vocabulary of every side effect.
3. Actors, actor Foo (§15): concurrent share-nothing entities built from actions. Every on handler is an action, and only an action can spawn or send.

main! is the root actor, and every effect therefore runs inside some actor. Performing an effect is a synchronous call; being a concurrent entity means a mailbox, a thread, and deep-copied messages. The two remain distinct.

2. Lexical basics

• File extension .hk. One file = one module, module name = file basename.
• Comments: # line comment. No block comments. A # block directly above an item is its doc comment; a fenced ` block inside runs as a doctest (§17).
• Strings: "...". Escapes \n \t \r \\ \" \0 \#. Interpolation: "x = #{x}".
• Newlines terminate statements. A trailing \ continues to the next line, and so does a line starting with .name: nothing else in the grammar begins with ., so xs.filter(..) followed by a line reading .map(..) is one expression. hanki fmt keeps the break you wrote and sets the indent to two under the receiver. It never breaks a long single-line chain for you.
• Identifiers: [A-Za-z_][A-Za-z0-9_]* optionally followed by one ! or ?.

Keywords (reserved): def actor on match if else elif end then var type struct opaque impl trait throw try catch spawn async await move loop do break continue return use open meta true false self and or not where effect provide test with_budget.

3. Numeric types: two tiers

LOWERCASE TIER (exact, default):
  int        arbitrary-precision integer
  decimal    arbitrary-precision decimal
  rational   exact p/q

  Chain:  int ⊂ decimal ⊂ rational
  The OPERATORS widen; arithmetic NEVER rounds.

FIXED-WIDTH TIER (hardware, opt-in):
  i8 i16 i32 i64    signed   |  u8 u16 u32 u64    unsigned
  f32 f64           floats

  Same-width only. Cross-width / cross-tier needs an explicit method.

Defaults: unsuffixed integer literal → int; unsuffixed float → decimal, including literals passed through generic calls while later context may still pin their type. Annotation or suffix overrides; a pinned generic slot pins the literal too (o: Option<int> = Some(0), r.unwrap_or(0) on a Result<int, _>).

A literal pins anywhere at or above its own kind on the exact chain int ⊂ decimal ⊂ rational. 2 denotes the same value as 2.0 and 2/1; 1.25 denotes 5/4. A decimal or rational parameter therefore needs no conversion written at the call. f64 sits outside this: a fixed width is opt-in hardware semantics.

Widening elsewhere is operator-level. The arithmetic operators and the comparisons promote their operands. Every other position takes the type it declares: parameter, return, annotated binding, field, list element, branch, trait-method argument. A decimal value does not reach a rational parameter without d.to_rational(), and an int value does not reach a decimal one without n.to_decimal(). There is no value subtyping.

f32 values are single precision throughout. A literal, an f32.parse and an arithmetic result all land on the single-precision grid, which makes x.abs() == x true for a computed x and makes the same number reached two ways compare equal.

x = 5            # int
y = 1.5          # decimal
n = 42i32        # i32 via suffix
m: i64 = 7       # i64 via annotation
q: rational = 0.1  # exactly 1/10, not a binary float

Division

• / is true division: int / int -> rational, f64 / f64 -> f64, i32 / i32 -> i32 (truncating sdiv).
• // is floor division, defined on int and the fixed-width integers.
• % is modulo with the sign of the divisor, over the same domain as //.

Fixed-width /, // and % need a non-zero literal divisor. x / 2i32 compiles; x / 0i32 and a bare x / y are compile errors. For a runtime divisor use checked_div, checked_floor_div or checked_mod, each answering an Option. Flow narrowing is the other way through. A bare x / y is allowed in the then-block of if y != 0 … end, up to any rebind of y and inside a closure written there (closures capture by value), and after an early-exit if y == 0 … end whose branch diverges through return, crash!, throw, break or continue. The lowercase tier has no such rule.

Lowercase division is total through in-band sentinels: 1/0 = +inf, -1/0 = -inf, and 0/0 = undefined, which absorbs. They propagate through arithmetic, have a total order (-inf < finite < +inf < undefined) and reflexive equality (undefined == undefined is true, where float NaN is false). They render as inf, -inf and undefined.

Fixed-point rendering

d.to_fixed(places, mode) -> string is the %.Nf this tier otherwise cannot spell. It renders; the value is untouched, and the exact tier still never rounds.

mode is a RoundingMode: Up, Down, Ceiling, Floor, HalfUp, HalfDown, HalfEven. It has no default. Down goes toward zero and Floor toward negative infinity; they agree above zero and differ below.

Padding follows printf: 1.5 at 3 places renders 1.500, and 0 at 2 renders 0.00. Negative places clamps to 0 and an absurd one to a million, which limits the rendering and never the value. A result that rounds to zero has the input's sign, byte-identical to f64.to_fixed: (0 - 0.001).to_fixed(2, Down) is -0.00, and so is its Ceiling and every other mode.

Back down from rational

r.to_decimal(places, mode) narrows down the chain, the counterpart to decimal.to_rational. A division leaves you needing it before the result can go into a fixed-scale column. It cannot be exact for every value the way the widening is, and you therefore state the scale and the tie rule. r.to_fixed(places, mode) renders byte for byte the way decimal.to_fixed does.

Overflow

The fixed-width tier wraps, modular. +, -, * and unary - are total and never trap (200u8 + 100u8 == 44u8), which leaves pure functions total. To detect an overflow use checked_add, checked_sub, checked_mul or checked_neg, each answering an Option. There are no wrapping_* methods, since the bare operators already wrap. The lowercase int, decimal and rational tier is arbitrary precision and has no overflow.

Bitwise

Methods on the fixed-width tier, with no operator form: bit_and, bit_or, bit_xor, bit_not, bit_shl and bit_shr, with a u32 shift amount. All are total, and the shift is taken mod the bit width. bit_shr sign-extends for the signed widths and is logical for the unsigned ones. The lowercase tier has none of them. u32 also has count_ones, a popcount.

abs, min, max, clamp

min, max and clamp are default methods on Ord, defined once over cmp, which gives every Ord type all three: int and every fixed width (3i32.min(7i32)), decimal and rational, bool, string, bytes, and any user Ord type ("apple".min("banana")). An inherent impl overrides the default. clamp(low, high) limits to the closed range, and crossed bounds, low above high, answer high.

abs is inherent on the signed int, i8, i16, i32 and i64. Fixed-width abs is modular like the bare operators, and the most negative value therefore maps to itself; int.abs has no wrap case.

f64 and f32 each have their own min, max and abs intrinsics, since neither has Ord. They follow IEEE: min and max answer the non-NaN operand when one is NaN, and abs clears the sign bit.

f64 also has the libm surface: floor, ceil, round, trunc, sqrt, cbrt, pow, exp, ln, log10, log2, sin, cos, tan, atan2 and hypot. All are total in the fixed-width sense, answering NaN for a domain error, and identical on both tiers.

f64.to_fixed(places) is that tier's printf %.Nf. 1.0f64.to_fixed(2) is "1.00", which Display cannot spell, since it prints the shortest text that round-trips. Ties round half to even, where round goes half away from zero, and there is no mode parameter: a caller wanting modes crosses to decimal. Negative places clamps to zero and an absurd one to 1100. The non-finite values render as NaN, inf and -inf.

int.pow

int.pow(exp) answers a rational, which makes every exponent exact: 10.pow(3) is 1000, and 2.pow(-1) is 1/2 where an int result would be a lossy 0. The common case crosses back with 10.pow(3).to_int(). 0.pow(-1) lands on the p/0 sentinel. f64.pow is the inexact counterpart.

Generic numeric code: the Numeric trait

Core numeric declares the static identities zero() and one() plus add and mul, which mirror the native + and *, implemented for all 13 numeric types. List.sum() and List.product() are its stdlib consumers, folding from the identity: an empty list answers zero or one. They work on any concrete numeric list with no import. For your own generic, bound <T: Numeric> (open numeric to name it) and reach the identities as T.zero() and T.one(). The operator traits Add and Sub exclude the builtin numerics, which leaves this plain trait as the numeric bound. Fixed-width add and mul wrap like the operators, and the lowercase sentinels propagate.

Float assertions

Core test, whose module head is the keyword itself. Floats have no Eq, which makes assert!(a == b) on them a compile error. State a tolerance with test.within_epsilon?(a, b, eps) (absolute; within_epsilon32? for f32) or test.within_ulps?(a, b, n) (relative, exact over to_bits). test.diff(expected, actual) renders a readable delta for the assertion message. Full rules: hanki doc test.

Timestamp formatting

Extra datetime, with no strftime strings. The Format builder composes part constants (year through second, weekday_short_name, offset and offset_numeric, the numerics zero-padded), literal(text), and the iso_date and iso_time fragments, with Format.of([...]) or +. After a leading Format a plain string is a literal: STAMP: Format = iso_date + "T" + iso_time + offset_numeric. Render with STAMP.render(odt) against an OffsetDateTime. A top-level Format binding folds at compile time. Full rules: hanki doc --find Format.

Iteration

Stdlib, with no syntax: there is no for, no while and no ... Range.new(lo, hi) is the half-open [lo, hi) int range with List style combinators: each!(|i| …), map(|i| …) -> List, fold(init, |acc, i| …), length and to_list. An inclusive range comes from int.upto: 1.upto(3) gives 1, 2, 3. n.times!(|i| …) runs an action n times over the indices 0…n-1, and a zero or negative n does nothing. Bounds are int, which lets counters compose with no conversions.

Cross-tier and cross-width conversions

Every crossing is written as a method call:

a: i32 = 5
b: i64 = 10
a.to_i64() + b       # OK
a + b                # ERROR: width mismatch

n: int = 100
n.to_i64() + 5i64    # OK

x: f64 = 1.0
x + 1.0f64           # OK (both f64; a bare 1.0 is decimal)
x + 1.0              # ERROR: tier mismatch (1.0 is decimal by default)

Narrowing with i32.to_i8 truncates: modular, total, the low bits at the target width. Pair it with try_to_i8, which answers Option<i8> and gives None when the value does not fit, to detect an out-of-range value where the bare conversion would wrap through it.

The bridges: i32, i64, u32 and u64 have .to_int() and .to_f64(); int has .to_i64() and .to_f64(); f32.to_f64() widens losslessly and is the bridge for f32 + f64; decimal and rational have .to_int(), .to_i64() and .to_f64(); and f64.to_int() is the reverse crossing into the unbounded int. Which of them round, truncate or saturate, and what each does to a sentinel, is hanki doc <type>.

decimal.to_rational() is exact and completes the chain as a conversion. The implicit widening is arithmetic-only: a decimal does not reach a rational parameter on its own, and decimal / decimal yields a rational, which makes the conversion necessary for a mean. decimal also has abs, which Ord's min, max and clamp defaults do not supply.

Each exact type also decomposes losslessly into the pair it is stored as: decimal's unscaled and scale props with decimal.from_parts, rational's numerator and denominator props of the reduced p/q with rational.from_pair. Both are exact round-trips, sentinels included, and this is the seam a binary codec uses.

Text to value: all thirteen implement FromString, which makes .parse(s: string) -> Result<T, ParseError> a trait method and no inherent one. The core impls are ambient and need no import. Integers are base 10, f64 and f32 are correctly rounded, decimal is exact at the written scale, and rational takes a reduced p/q and every decimal spelling; the accepted sets nest like int ⊂ decimal ⊂ rational. Whitespace is trimmed. Underscore separators are literal syntax and no part of the data, and int.parse("1_000") therefore fails on all thirteen. The in-band sentinels have no spelling, and "inf" fails on the exact tiers.

The Err says which failure it was, which an Option could not: u32.parse("4294967296") reports out of range for u32 (0 ..= 4294967295), and u32.parse("nope") reports not a base-10 integer. An unsigned width refuses a leading - by spelling, and "-0" therefore fails even though 0 is in range.

4. Other built-in types

A resource type reads bare, or qualified under the module whose API hands it to you: fs.File, process.Child, net.TcpStream, net.TcpReadHalf, net.TcpWriteHalf, net.TcpListener, net.UnixStream, net.UnixReadHalf, net.UnixWriteHalf, net.UnixListener, bytes.BytesBuilder, bytes.BytesReader, bytes.ReadCheckpoint, str.StringBuilder, sqlite.SqliteConn, tls.TlsStream, tls.TlsReadHalf, tls.TlsWriteHalf, tls.TlsListener. The qualifier is the module you reach the handle through, and the module holding its methods may be a different one. The qualified spelling of an extra-tier resource needs use <module> like any other member. The two spellings identify the same type in annotations and impl heads, including method lookup and ownership checks.

bytes values come from encoding a string with s.to_bytes() or out of a codec. There are no bytes literals.

Byte-offset ops: length, empty?, slice(start, stop), view(start, stop), join(parts), get(i) -> Option<u8>, get_or(i, fallback) (the same read without the Option), and compare(other) -> i32 (lexicographic; bytes is also Ord and Eq). Decode with b.to_string() -> Result<string, Utf8Error>. The parameter is stop, since end is a keyword.

slice copies the visible range into an independent allocation; use it when a small result must not retain a large input. view is the explicit zero-copy form. Views flatten onto one owner, equality, hashing, decoding and rift serialization observe only the visible bytes, an empty view retains no owner, and a full-range view may reuse its input. A view retains its full backing allocation and byte ceilings conservatively charge that full backing to each holder. Sending a subview to another actor detaches its visible range, preserving actor isolation; both tiers have the same behavior.

Array<T> is the unboxed contiguous collection for hot numeric loops, limited to f64, f32, i64, and i32. Construct it with Array.filled(n: int, x) or Array.from_list(xs); it is fixed-size, has no push, and grows only by explicit copy_resize(n: int, fill). Its performance-facing index surface is i64: length, total get/get_or, and set. An out-of-range write leaves it unchanged. xs = xs.set(i, x) reuses a uniquely-held buffer in counting mode and copies a shared one, preserving aliases; tracing mode copies. Arrays are sendable COW values and are charged by --max-bytes. --explain-copies and --profile-allocs expose missed reuse. bytes remains a separate immutable type.

Scanning takes a (u8) callback and needs no index loop: any?(pred), all?(pred), position(pred) -> Option<int> (the first index passing), find(pred) -> Option<u8> (the first byte passing), fold(init, f), each!(f), try_fold!(init, f) and try_each!(f). The try_ twins take a Result-returning step and stop at the first Err.

Assemble in O(n) with a BytesBuilder resource: new!(), then push!(b: u8), extend!(b: bytes), push_be_u16! / push_be_u32! / push_be_u64! for big-endian fixed widths, the push_le_* mates with the low byte first (what a GPU buffer wants), push_be_f32! / push_le_f32! / push_be_f64! / push_le_f64! for IEEE bits via to_bits, which preserves a NaN payload, reserve!(n) for room for n more bytes up front (a hint that moves no byte), spare_capacity!() for the room already there (only >= n is promised), and finish!() -> bytes. Out-of-order writes have length!() -> int, fill!(b: u8, n: int) to append n copies, and set!(i, b) -> bool to write one byte at an index. set! answers false where i is past the last written byte and changes nothing: the buffer never grows to meet an index, and fill! is how it reaches a size first.

Read back with a BytesReader cursor: new!(input), then copying take!(n) -> bytes, zero-copy take_view!(n) -> bytes, take_be_u16! / take_be_u32! / take_be_u64! with their take_le_* mates, take_be_f32! / take_le_f32! / take_be_f64! / take_le_f64!, each answering Option<T> with None on a short buffer and the cursor unmoved, peek!() -> Option<u8> for the next byte with no advance (None at the end), take_u8!() for the same byte taken (the tag byte or varint a self-describing format reads singly), remaining!() and position!().

These ops are actions whose row is [local] (§7) and nothing further. They mutate runtime-managed state and no OS capability; the ! marks impurity and no capability. Value-level mutability still does not exist: bytes, structs and lists never mutate in place.

string has the same arrangement one level up. Accumulate in O(n) with a StringBuilder resource: new!(), then push!(s: string), push_display!(v) and finish!() -> string. finish! needs no Result. It replaces rebinding acc = "#{acc}#{x}" in a loop.

Three ways to assemble text, all single-pass: interpolation for a fixed number of parts, sep.join(parts) for a list, and the builder for pieces that arrive one at a time. Interpolation lowers to one build over its parts, one allocation and no fold; a many-hole literal copies its bytes once and adds nothing per hole.

string has no concat, and neither does bytes. A call to either is H0406, which names the tool for the case at hand. List has its concat: no list literal interpolates.

Pair<A, B> is in stdlib pair outside the prelude, and open pair names it. It is the two-field product, first and second, standing in where another language has a tuple; Hanki's product type is the struct. It is List.zip's element: xs.zip(ys) -> List<Pair<T, U>> stops at the shorter list, and zip_with(other, f) is the Pair-free form. Construct it call-style, Pair(first=1, second="a"), and annotate the binding as p: Pair<int, string> = …: a generic constructor call infers no type params from its arguments, as with List.empty(). Eq and Display synthesize on demand like any struct's, which makes == field-wise and the render Pair(first=1, second=a). Naming your own type Pair is fine: impls key on the module-qualified head, and yours and pair.Pair are then distinct types that each derive their own.

Secret<T> is in stdlib secret outside the prelude, and open secret names it. It contains a key, a token or a password. Secret.hide(v) wraps and s.reveal() reads back; reveal is the only way in.

It has three refusals a hand-rolled wrapper does not get.

1. dbg! and the crash-time state dump print <redacted> on both tiers. They render from a type's structure and never through Display, and omitting a Display impl does not stop them.
2. It implements no traits at all, which makes a @derive or an on-demand derivation reaching a Secret field H0405 at that field, where otherwise a generated body would walk the material into a wire format.
3. It is not Sendable (§15).

== is absent: a byte compare returns at the first difference, and the timing leaks the material. Compare by revealing both sides to sha2.constant_time_eq?, which takes bytes; a Secret<string> therefore needs .to_bytes() on each side.

Three limits are worth stating. A closure's captures are a hole in the Sendable rule that no static rule can close, since they are absent from its type; resources and Futures are read the same way, and a closure type naming a Secret is refused like any other mention. Nothing wipes the material: a value has no destructor, and the pool clears a cell when it hands it out. reveal() yields a plain value with none of the guarantees. Naming your own type Secret is fine, as with Pair, since the refusals key on the module-qualified head.

Resources

File, Child, TcpStream, TcpReadHalf, TcpWriteHalf, TcpListener, UnixStream, UnixReadHalf, UnixWriteHalf, UnixListener, TlsStream, TlsReadHalf, TlsWriteHalf, TlsListener, BytesBuilder, BytesReader, ReadCheckpoint, StringBuilder and Module<T> are handles to live native state. The state is released the moment the last handle drops, or eagerly through close! (a Module<T> through module.unload!). Dropping a live Child terminates and reaps its subprocess. Memory is per-actor reference counting; values are acyclic, and there is therefore no cycle collector and no collection pause.

A resource has one owner and is never copied. It cannot be deep-copied across a send, and it can be moved into a receiving actor: a resource-typed handler parameter is a move-in, and the sender writes move x, as in async w.serve!(move sock), which consumes the binding. Four spellings are refused: a resource as a return type, as a throws type, nested inside an aggregate parameter, and passed to a send without move (as is move on anything else). A long-lived resource goes in actor state.

Open a file with fs.open_file! -> Result<File, FsFailure>, then f.read_all!() and f.close!(). Open TCP with net.connect! or net.listen!. Open a pathname Unix-domain socket with net.connect_unix!(path) -> Result<UnixStream, NetError> [net] or net.listen_unix!(path) -> Result<UnixListener, NetError> [net, fs_write]. Unix bind never unlinks an existing path first, and close/drop closes only the descriptor. The pathname remains until an explicit fs.delete!(path, false) after the shutdown protocol excludes concurrent replacement; metadata-check-then-unlink cannot prove ownership atomically. The listener exposes no local_address!, and abstract-namespace addresses are out of scope. A non-Unix host returns NetError.Other. Full TCP, Unix and TLS streams use read!, write!, split! and close!; listeners use accept! and close!. TCP and TLS client connect! starts one absolute 60-second deadline across resolution, connection, handshake where present, and later I/O; connect_with_deadline! chooses another budget, full streams and a TCP/TLS http.Client reset it with set_deadline!, progress never refreshes it, negative is an immediate poll, and accepted streams remain unbounded. The separate DeadlineStream capability leaves custom streams clock-free, and HTTP normalizes either transport's expiry to HttpError.TimedOut.

TcpStream.split!() -> Pair<TcpReadHalf, TcpWriteHalf> and UnixStream.split!() -> Pair<UnixReadHalf, UnixWriteHalf> invalidate the full handle. The returned Pair cannot cross a mailbox while it contains resources; extract its fields before sending them. Each half is a distinct single-owner resource and can move to its own actor, making one actor per I/O direction the full-duplex pattern. Closing or dropping the read half performs SHUT_RD, and later local reads return empty bytes. Closing or dropping the write half performs SHUT_WR, later local writes report BrokenPipe, and the peer sees EOF. Either close is idempotent, the sibling direction remains live, and the descriptor is released after the final half.

TlsStream.split!() -> Pair<TlsReadHalf, TlsWriteHalf> has the same ownership shape, but its resources are application capabilities over one shared TLS record layer. The mapping is one record layer to two application-operation faces. Either half may service either underlying socket direction because TLS reads can require transport writes and TLS writes can require transport reads. The runtime releases that shared state before parking an actor; a blocked reader never locks out the writer whose request makes the peer answer. Closing the read half rejects later local reads but preserves transport reads the writer needs; closing the write half rejects later local writes, queues close_notify best-effort and leaves the reader live.

ReadStream.read!, WriteStream.write! and the separate duplex Stream trait are the core transport contracts. Full TcpStream, UnixStream and TlsStream values implement all three; TCP, Unix and TLS read/write resources implement only their direction. net.write_all! and http.write_response! take S: WriteStream; http.read_request! and http.read_response! take S: ReadStream. Those directional traits retain sys.NetError and [net]. Duplex Stream instead declares type Error, and its methods carry [e]: TCP and Unix bind sys.NetError, TLS binds sys.TlsFailure, and a pure in-memory implementation may bind its own error. Code needing duplex I/O and close! names the row with <S: Stream[e]>; Hanki cannot express Stream as formal composition of the two narrow traits.

For several HTTP/1.1 requests on one connection, wrap a caller-opened transport with http.Client.from_stream(s). Its operations require <S: Stream[e], S.Error: Into<HttpError>>, own that concrete stream and leave it open between requests. Framing pays the transport row [e] and converts the projected transport error explicitly; Client<TcpStream> and Client<TlsStream> remain distinct. Code supporting both retains its two connect arms. Because a resource nested in a value cannot cross an actor message, move the bare stream to its worker before constructing the client there; actor death then drops the held stream normally. A server close surfaces as a typed HttpError (Net for an OS refusal, Incomplete for a clean EOF before a response head), and a Stream.write! count outside the offered nonempty buffer is InvalidWriteCount(count); neither is retried automatically. render_request preserves the caller's Connection field and otherwise uses HTTP/1.1 persistence; the one-shot top-level request! supplies close itself. Response rendering still sends Connection: close, matching http.serve!'s one-request loop.

Naming convention: the lowercase types bool, string, int and i32 are the ubiquitous primitives, and PascalCase covers the abstract, generic and user-defined ones. A bare single uppercase letter such as T, K or V is always an implicit type parameter, and a struct, type or actor may not take one as its name; call it Point. The rule runs the other way too: a type parameter is a single letter wherever it is declared, and def pick<Item>(…), struct Box<Item> and impl<Key, Val> are rejected at the declaration as H0634. A trait's own parameter list is the one exemption, as in trait Add<Rhs = Self>, where those bind correctly and longer names remain legal.

5. Bindings and mutability

x = 5            # immutable; type inferred
n: i32 = 7       # immutable, annotated
var y = 0        # mutable
y = y + 1        # OK

Shadowing is allowed while the type does not change.

A name starting with _ is private to its module, and the compiler enforces that as H0622 in every spelling. A module's public surface is its names without the underscore. Another module cannot reach a private name by qualifying it, through an open, as an assoc fn on a type it declares, as a method, prop or handler through a value receiver, or as a field. A struct with a _ field is constructible and destructurable only by its own module, since patterns and construction supply every field, positional spellings included; its public fields stay readable everywhere. A _ trait member belongs to the trait's module, whichever module wrote the impl.

Structs are values, and a field write rebinds

q = p copies the binding, and nothing is aliased (unlike Python or JavaScript). p.x = v, or the nested p.a.b = v, rebinds p to an updated copy and so needs var p; writing through a = binding or through a parameter is H0207. q is untouched.

The compiler turns the per-write copy into an in-place write where it proves p unshared. Where it cannot prove it, single- and two-level writes check the actual handle count at run time, mutating in place when unique and copying when shared. Array.set obeys the same rule: same-binding reuse can be allocation-free, while a shared receiver copies its contiguous buffer. An accumulator loop is therefore allocation-free on both paths, with the value semantics unchanged. hanki check --explain-copies reports the field or Array writes the proof missed as H0564, which does not block, and adds an O(n) note when the write sits in a loop. hanki run --profile-allocs counts what one bytecode run rebuilt and prints it per write. hanki build --profile-allocs writes an instrumented AOT executable to the distinct out/<name>.profile-allocs; ordinary native binaries carry no profiling overhead. Both print the same stderr table at orderly exit. A profiled AOT image that can run dynamically loaded bytecode names those allocations as excluded from its table. Actor state fields rebind the same way.

Values are acyclic. No sequence of writes makes a value reference itself: the right-hand side is evaluated before the write, and an attempt to tie a knot therefore nests a copy. Model a cyclic structure with keys in a Map<Id, Node>, or with ActorRefs, which are identifiers; reference cycles between actors are fine.

6. Functions and actions

use io

def add(a: i32, b: i32) -> i32
  a + b
end

def main!(args: List<string>) -> () [io]
  io.print!("hi")
end

• Types are mandatory on every parameter and on the return type. There are no silent defaults.
• A function body's value is its last expression. An explicit return <expr>, in statement or tail position, exits early, and a bare return exits a () function (§7). A return in tail position is redundant and a compile error. Keep return for early and guard exits.
• An if/elif chain comparing one binding against three or more constant values (if c == Some(1u8) elif c == Some(2u8) elif c == Some(3u8) …) is the compile error H0618. Write it as match c, which binds the payload once and covers the rest with _. Only == against a constant counts; !=, or compounds and comparisons against runtime values are fine.
• Actions list their effects in [...] after the return type. [io, throws E] reads "may do io, may throw E".

Exit codes

main must return () or an integer; any other return type is a compile error. An integer return becomes the exit code's low byte. () is 0 and is never printed; stdout receives only what io.print! writes.

The four language faults are identical on both tiers. The resource bound is the bytecode tier's alone, and it wins over the four: a spawned actor spending the last of the whole-program budget exits 250 and not 253.

An escalating actor death also outranks the faults it causes. A sender that reaches the now-dead actor gets SendFailed::Died, and when that propagates past main! uncaught the program still exits 253.

Deep recursion is the other runtime fault. The AOT tier compiles calls to native calls, which bounds recursion by the OS stack, and an actor thread's stack is about a quarter of the program thread's. Past the bound the program prints hanki-runtime: stack overflow and exits 1. That is uncatchable and program-dependent, and no depth is promised. The bytecode tier recurses on its own frames and continues. Write a loop where the depth is unbounded.

A lost consumer and a failed write

The two are different events and end differently.

Nothing reading the output any more, as in prog | head giving EPIPE, is the reader's ordinary termination. head closing the pipe is head doing its job, and the program ends with exit 0 through the normal shutdown path, printing nothing.

Any other write failure, a full filesystem or a failing device, means output was lost that nobody wanted lost. That is a runtime fault: both tiers name which write failed and take the actor down, exiting 253 when unsupervised in a spawned handler and 1 in main!, which sits outside the 250 to 254 language-fault block. A failed flush is classified the same way, since a write with no trailing newline only reaches the OS there.

Three things follow. Neither tier dies of SIGPIPE: a kernel-delivered signal would skip the exit hooks that restore the terminal (§17). The exit is 0 and not 141, which would claim a death that did not happen and is a reachable main return here anyway. A lost consumer ends the program and not one actor: a spawned writer does not die and no supervisor sees it. And io.write!(s) -> Result<(), sys.WriteFailure> is the same write with both outcomes as values, ConsumerGone and Failed(msg), for the daemon that must notice its reader leaving and carry on. io.print! remains unit-returning. Each of the four has a bytes twin (print_bytes!, eprint_bytes!, write_bytes!, ewrite_bytes!) under the same rules, for output that is not UTF-8.

7. Effects

Built-in effects:

Multiple effects read [io, throws ParseError]. Effects are typed markers, checked statically. They are not algebraic: there is no handle and no with. [fs] is an alias for [fs_read, fs_write], expanded wherever effect names are interned, including in --allow and --deny; --allow fs_read grants a read-only filesystem.

Spawning a subprocess

process.run! charges [process]. run_with! adds a per-spawn environment overlay, and run_in! adds a working directory as well; both charge [process, env]. run_attached! hands the child this process's terminal in place of pipes, answers a bare sys.ProcessOutcome, charges [process, io], and is refused under --deterministic. run_opts! and run_attached_opts! take a SpawnOptions carrying cwd, env, env_remove and env_clean, for a spawn that needs a directory and an environment together, or that needs to take a variable away: an overlay cannot do that, since setting a variable to "" sets it empty and leaves it set.

For output before exit, process.start!(cmd, args, opts) -> Result<Child, sys.ProcessFailure> returns immediately with piped stdin, stdout and stderr. The name is start!, since spawn is the reserved actor keyword and cannot name a callable. Child.read_stdout! and read_stderr! use sys.StdinRead's Bytes / TimedOut / Eof / Failed shape and timeout convention; its Resized arm is terminal-stdin-only and child reads never produce it. Child reads follow the native-call deadline rule in HANKI.md §6; retries do not restart a finite read timeout. write_stdin!(data, timeout_ms) returns the accepted prefix length; zero timeout polls, positive bounds the whole call, and negative waits for progress. Expiry returns Ok(0) and preserves the child. Retain the unwritten suffix, alternate with output reads, and return between bounded actor handlers to service resize and control messages. write_all_stdin! waits for the whole buffer and can deadlock if this actor must drain output. try_wait! returns sys.ChildPoll: Running, Exited(code), or Failed(ProcessFailure). It polls once, caches a reaped exit, preserves the output streams on errors while releasing an unwaitable process handle, and rejects closed handles. close_stdin!, wait!, kill! and close! drive the rest of the lifecycle; drain output before a potentially blocking wait. SpawnOptions.with_merge_stderr(true) joins stderr into stdout, avoiding a two-pipe deadlock when separation does not matter. A Child is actor-owned and single-owner; final drop, actor death and program exit terminate and reap it on both tiers.

process.start_pty!(cmd, args, opts, columns, rows) is the streaming pseudoterminal face for preserving colour and isatty behaviour without handing over this process's terminal. The fresh POSIX terminal starts at the given cell size, and Child.set_size!(columns, rows) resizes it and causes the kernel to deliver SIGWINCH. Stdin, stdout and stderr share one bidirectional terminal: write with write_stdin!, read merged output with read_stdout!, and expect read_stderr! to return Failed; merge_stderr is irrelevant. A terminal has no half-close; close_stdin! hangs it up and also loses later output. The handle has the ordinary actor ownership and reaping rules. Dimensions fit u16; non-Unix hosts return Err.

process.spawn_detached!(cmd, args, opts) -> Result<(), sys.ProcessFailure> is the explicit exception to those ownership rules. It reports successful exec and returns no Child, streams or exit status; actor death and program exit cannot reclaim it, and all three standard streams are the platform null device. POSIX starts a new session and double-forks so the final child cannot later acquire a controlling terminal. It charges [env, process]: no stronger-looking atom could form a real boundary when [process] already permits a shell child to background its own grandchild. merge_stderr is irrelevant.

[local] and [runtime_state]

[local] marks mutation of state the computation owns. It is implicit in every action's row, which leaves no action's row empty, and any other effect absorbs it, which leaves an [io] action listing nothing extra. The one place to write it is a function type: (u8) -> () [local] is the type of a slot holding an action closure. Writing it on a declaration is rejected as redundant, the ! being that spelling. It is no capability.

[runtime_state] marks observing process-global runtime state the program does not own. Today that is the log-threshold trio log.min_level!, log.set_min_level! and log.enabled!, with the sys intrinsics under them. It is viral like any effect and is not a capability: --allow and --deny cannot name it, and @encapsulated refuses it. Declaring an effect with that name is rejected, as for every built-in name.

User-defined effect groups:

struct Rows
  affected: i32
end

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

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

Built-in effect names are reserved. An effect block may not take one of the nine capability atoms, the [fs] alias, state, local, runtime_state or Crash. Effect names are one flat vocabulary: a same-named user effect merges with the builtin and never shadows it (H0632).

An op is bare-callable inside its own module and under open db. Like every top-level name it sits at module.op and is never bare-global, which leaves a merged module's op unable to collide with your identifiers.

There is no module.op qualified call: db.exec(…) is an error. An op's qualified spelling goes through its effect's name, Database.exec(…) wherever that name is in scope and db.Database.exec(…) under use db, and the call therefore spells the atom it charges. Both spellings are the same reference as the bare op, with the same row, the same purity wall, the same provider and the same behaviour on both tiers, and both work in value position: f = db.Database.exec. Where a module declares an effect Foo beside a type Foo, Foo.member searches both surfaces, and a member both supply is H0633 and never a silent pick.

An application may answer an effect with Rust through a rift (§18, HANKI.md §6): the same ops, a crate in its own repository, values crossing as bytes. Only an application root may open one. State is per actor, a panicking op is an actor death, and --allow must name the atom.

Providing user effects

The effect block declares the signatures, and a provide block binds the implementations. The provide head's row is the shared effect budget of every op body; ops carry no rows of their own. A module-qualified head lets an application provide a library's effect: provide db.Database [net] … end.

A program that uses an effect's ops needs one provider and no more. A missing or duplicate provider is a compile error, as a missing main is. A declared but unused effect needs none.

A library root, one the manifest lists under exports and not under programs, defers: its unprovided effects are its capability interface, and the application that links it answers them. A path in both lists is run and answers its own. --deny net counts the provider's row:

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

Effect variables

A higher-order action that performs whatever its callback performs writes the row as a single lowercase letter, an effect variable, in the callback's type and in its own row: def each!(f: (T) -> () [e]) -> () [e]. At each call site e solves to the callback's concrete effects: an [io] closure charges the caller [io], and a pure callback charges nothing. A single lowercase letter is an effect variable as a single uppercase letter is a type parameter; io and fs are multi-letter, and no name collides.

Function types carry effects

A function type may annotate its effect row after the return type, as a def does: (Event) -> () [io]. An unannotated function type is pure, in every position: parameter, field, let, return. It matters where a function is stored or returned, in a struct field, an annotated let or a return type.

struct Event
  name: string
end

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

Storing, returning or passing a closure that does more than the slot permits is an error; annotate the slot. Doing less is fine. A closure calling any action does more, even one with no world effect: || b.push!(1u8) performs [local], which makes a pure () -> () slot reject it and leaves a pure def unable to invoke it. Annotate the slot [local] to hold it, and read it back from an action or an @encapsulated def.

"Doing less is fine" applies to a closure literal, which is checked against the slot. A function value must match the row, and a [local] field therefore refuses a plain pure function too. Annotate a slot for what it takes and not for the widest thing it might.

Invoking a stored function value charges its declared effects to the caller: reading h.on_event and calling it requires [io]. A value whose row is a variable, [e], may be invoked or forwarded and not stored into a concrete slot, which would launder its effects. Store a real callback under a concrete row such as [io].

The bang must be earned

An action whose row is only the implicit [local], and whose parameters, self included, and result are all deeply immutable, is a pure function of its inputs, and H0630 refuses the !. Drop it, and add @encapsulated where the body mutates state it allocates itself.

Only concrete boundary types are judged. A trait's Self and a generic parameter tell the checker nothing, which leaves Serializer.put_u8! its bang. Entry points retain theirs, and a trait member is flagged at the declaration and never at an impl.

To reserve the ! for a world effect you will add later, write @reserved_effect def f!(…). That marker is itself H0631 anywhere H0630 would not have fired.

@encapsulated, checked local mutation

A ! marks a world effect such as [io] or [net], or mere non-substitutability, [local] alone as on BytesBuilder.push!. A pure def can call neither. Mark a def @encapsulated, with no !, and it may perform [local] on locally-allocated state and stay callable from meta, from a where block and from pure code.

Three things are checked: the row is [local] only, with no world effect, throw, crash! or spawn; no parameter is deeply mutable, since it allocates its own state, and a bounded generic parameter is checked at the call that instantiates it (H0629); and the result is deeply immutable, which lets no live builder, cursor, resource, Future or closure escape, while the bytes from finish!() is fine.

Debugging: observe, do not interrupt

Every diagnostic writes to stderr, outside the effect contract: dbg! for an inline print, and sys.actors! and sys.get_state! for live actor observation, in the BEAM's observe-and-do-not-stop shape. There is no stop-the-world step debugger. A capturable bug gets deterministic replay instead, through hanki run --deterministic, hanki test --deterministic and --seed.

dbg!(expr) is the one effect exemption. It evaluates expr, prints [file:line] <source> = <value> to stderr, and returns the value unchanged. Drop it around any subexpression, let y = dbg!(f(x)) + 1, and call it from a pure function: it adds no effects. It renders any value structurally, struct, sum, list or primitive, with no Display needed, identically on both tiers. That includes an un-monomorphised generic parameter, dbg!(x: T) and a nested List<T>, whose concrete shape the compiler threads from the call site as a hidden witness.

The command boundary is fail-closed where diagnostic output is security- or release-sensitive. check, the REPL, and unconstrained run, test and fuzz accept dbg!; any of those execution commands using --allow or --deny refuses a reachable site before execution, and every build refuses one before creating an artifact. Pass --allow-dbg explicitly to either boundary to retain the existing render. Reachability follows pure helpers and spawned actors while excluding dead code. hanki effects PATH --dbg --format=json lists {symbol, path, line, column} under hanki-effects-dbg-v1 and sets loads_modules when source is deferred to module.load!; loaded source inherits the host's choice and is checked at load time on both tiers.

struct Point
  x: i32
  y: i32
end

def slope(p: Point) -> Option<i32>   # pure — yet dbg! is allowed
  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

sys.actors!() prints a one-line-per-actor table to stderr, with the id, class, liveness, mailbox depth and capacity, and supervisor, and returns (). It is an ordinary [io] action and no exemption; pure code cannot call it, on both tiers. It is structural only and never reads actor state.

sys.get_state!(handle) prints one running actor's state, named by its ActorRef<T>, to stderr through the dbg! renderer, taken at that actor's next inter-handler safe point. It is the live counterpart to the crash-time dump. A wedged actor, self, and a dead actor are reported unavailable in place of blocking, which is Erlang's sys:get_state limit. It is [io], on both tiers, and is spelled get_state! after that Erlang call; state itself is contextual and not reserved.

crash!, assert! and ???

crash!(msg) -> Never is the divergence primitive. It never returns, and Never, the bottom type, coerces to any type, which fills an unreachable match arm. Its row has the uncatchable Crash atom, as in [io, Crash], and a pure def therefore cannot call it: pure functions are total. It is no throw, and catch e: Crash is a compile error. It kills the actor, reaching the supervisor's on actor_died, exits non-zero at the root, and fails a test. It is no capability: --allow and --deny cannot name Crash, and a Crash in the row never denies a program under an allow-list, while hanki effects still reports it. Both tiers behave alike. Write -> Never [Crash] for a never-returning action.

Calls to that action coerce the same way. A -> Never body cannot return an ordinary value, and a Never parameter cannot accept one. A callback may return Never for another expected result, but cannot require Never where callers supply a concrete value. Bottom-type coercion does not widen named type arguments; HANKI.md §4 gives the callback and container rules.

assert!(cond) has [Crash] for the same reason: a failed assert is an abort. A pure def cannot assert, a closure that asserts has the type () -> () [Crash], and an @encapsulated def, which asserts external purity, cannot assert either. A test block is a permissive context, and an assert is free there.

??? is the typed hole, and it is how a spec-first sketch is written. Its type is Never, as crash!'s is, and it is effect-free, which makes it legal in a pure def. hanki check reports every hole's expected type and effect budget as hole[H0250]; checking, the LSP and the REPL stay non-blocking. hanki run, test, fuzz and build reject holes in the selected checked program by default, before effects or output. --allow-holes is an explicit development escape, and a reached hole prints crash: hole reached and exits 252. A permissive AOT build writes only under out/holey/, never over a canonical artifact, and durably marks its executable, object or shared library in .hanki_holes, or IR in !hanki.holes metadata.

8. Errors

Failure splits two ways, along the functional core and imperative shell line, and the compiler enforces the split.

• A computed or logical failure in pure code is a value. Return Result<T, E>, which is Ok or Err, or Option<T>, and match it. A pure def is total (§5) and cannot throw. A parse that may fail, a smart constructor that may reject and a lookup that may miss all return a value the caller inspects.
• A world-coupled failure in the imperative shell is an effect: [throws E] on an action, for a failure inseparable from touching the world, such as an io error or an actor's [throws actor.SendFailed]. throws is action-only, and a pure function, with its empty row, cannot carry it.

Throw a struct or sum value with throw expr, and catch it with try and catch.

use io

open result        # bare Ok / Err below come from result (§14)

@derive(Display)
struct BadInput
  raw: string
end

def parse_int!(s: string) -> i32 [throws BadInput]
  match i32.parse(s)
    Ok(n)  -> n
    Err(_) -> throw BadInput(s)
  end
end

def main!(args: List<string>) -> () [io]
  try
    n = parse_int!("42")
    io.print!("#{n}")
  catch e: BadInput
    io.print!("bad: #{e}")
  end
end

• Only user-defined struct and type values can be thrown. Primitives are rejected. A callable’s type arguments also substitute inside its throws payloads, including Self and associated error types.
• A try may have several catch e: T arms, and the first match by source order wins.
• An uncaught throw propagates up through any caller declaring a matching [throws E].

The guard form

A chain of fallible steps has one dedicated statement: a refutable binding whose else arm is a match arm that must diverge.

open result
open option

type LoadError
  Missing
end

def first_line(lines: List<string>) -> Result<string, LoadError>
  Some(head) = lines.get(0) else None -> return Err(Missing)
  Ok(head)
end

There is no new keyword. It sits in statement position only, the else pattern must cover what the left one does not, and there is no var form. Every exit is spelled on the line with a real return, throw or crash!, which separates it from the postfix ? of §21. The binding takes the rest of its block, and a pattern with several binders therefore works. A sum whose variants each want their own treatment remains a match (§9).

9. Pattern matching

open result

struct Point
  x: i32
  y: i32
end

type LookupError
  NotFound(i32)
  Unknown
end

def classify!(r: Result<Point, LookupError>) -> string [Crash]
  match r
    Ok(Point(x, y)) if x > 0 -> "#{x},#{y}"
    Ok(p@_)                  -> "point #{p.x}"
    Err(NotFound(id))        -> crash!("missing ##{id}")
    Err(_)                   -> crash!("unknown")
  end
end

• Arms use ->. There is no of, => or :.
• A guard reads pattern if cond -> expr.
• p@Pattern binds the whole value and destructures it.
• Struct destructuring is positional, Point(x, y) in declaration order, or by name, Point(y=b, x=a) in any order and naming every field. An unknown, duplicate or missing field is an error. Structs only. It nests, and behaves the same on both tiers.
• _ is the wildcard.
• Numeric literal patterns compare in the scrutinee's tier. decimal uses exact numeric equality (1.50 matches 1.5). f32 literals round to the single-precision grid; f32/f64 use ordered IEEE equality, under which signed zeros match and NaN matches no literal. This is never bitwise equality.
• A named comptime constant is a pattern. Every top-level binding is compile-time evaluated (§16), and OP_CHAR -> … therefore matches its value and behaves as the literal it folds to: refutable, binding nothing, and still needing a catch-all. Primitives only; an aggregate is refused. Binders remain unambiguous, an uppercase-initial pattern being a constructor position: a name there resolving to neither a constructor nor a constant is an error, and a lowercase name binds.
• An arm body is one expression, as an inline closure body is. Arms have no end: the next pattern begins where the body stops. A single if, match, loop or try … end is fine as it stands, and so is the inline if: if c then a else b, one expression per branch, no end, with then selecting it. if c then a alone is the () statement guard, and a dangling else binds to the nearest if. To sequence a binding or a side effect and then a result, wrap the two in do … end, a block expression whose value is its last line. A bare statement followed by if … in one arm is a parse error.

use io

open result

def classify!(input: string, target: i32) -> string [io]
  match i32.parse(input)
    Ok(g) -> do            # do … end groups the two statements
      io.print!("checking\n")
      if g < target then "low" elif g > target then "high" else "hit"
    end
    Err(e) -> e.reason
  end
end

• match is exhaustive, and a non-exhaustive one is a compile error. Cover every variant; bool needs both arms and an open type needs _. The escape for a proven-unreachable arm is _ -> crash!(...). A guarded arm never counts toward coverage. Checking is complete: nested patterns count where they are exhaustive, which leaves Some(Red) | Some(Green) | None needing no _. The error names a concrete witness such as Some(Blue), and an arm already covered by earlier arms is a compile error.
• A two-outcome match whose failure arm only leaves, Err(e) -> return Err(e), is the guard form of §8: Ok(v) = f() else Err(e) -> return Err(e), after which the rest of the block reads on unindented. Same coverage rule, same patterns. A sum whose variants each want their own treatment remains a match.

10. Structs and sum types

struct Todo
  id: i32
  text: string
  done: bool
end

type Command
  Add(string)
  Done(i32)
  List
  Quit
end

Construct by positional or keyword:

def build() -> ()
  t = Todo(id=1i32, text="buy milk", done=false)
  cmd = Add("buy milk")          # Command::Add
end

Variants list one per line with no commas, the same shape as struct fields and trait items.

Declarations take generics: type Option<T> ... end. A variant payload is a positional payload list: Some(T) is a payload and never a type application.

A constructor that takes arguments is a value wherever the context types it: xs.map(Wrap), xs.map(Box), or a parameter or annotation naming the type. An argument-free constructor, a unit variant or a fieldless struct, has always been one. A bare constructor with nothing to type it, g = Wrap, is H0626, and a shared name the context cannot pin is H0624 and never a silent pick.

An inherent associated function is a value, as a top-level def is: xs.map(Colour.tag) and xs.each!(Colour.emit!) both read bare, and the action's effect row rides along. One reached through a trait impl is H0628, i32.parse from impl FromString<i32> being the example: dispatch settles which function the name means, and a bare reference has no arguments to settle it with. Write xs.map(|s| i32.parse(s)).

Planned representation: small scalar structs will cross direct, generic, trait and stored-callback calls without aggregate allocation on both tiers; Option<T> will use a discriminant and inline payload for every T. These targets are not implemented by the current native one-word ABI; HANKI.md §22 defines the classification, ownership and activation requirements.

opaque, the smart-constructor pattern

opaque is a standalone declaration keyword for a product type. It is no modifier: opaque struct, opaque type and opaque actor are parse errors.

opaque Email
  value: string
end

def parse_email(raw: string) -> Email
  # validation elided
  Email(value=raw)
end

Outside the defining file, construction and field access are rejected. A prop or def member read is allowed: a prop is mechanically a method, and e.domain therefore crosses the boundary as any accessor does. Opacity gates construction and field access, and leaves behaviour alone. The type name remains usable in signatures. A trait impl may live elsewhere, and cannot reach inside the fields.

where-block invariants (opaque type)

opaque Email
  value: string
where
  not value.empty?
  value.contains?("@") else "email must contain @"
end

Each line is a bool predicate over the fields, written with bare names and no self, no actions and no effects.

The compiler generates two functions. Email.new(value) -> Result<Email, validation.ValidationError> is pure and validates, answering Ok on success and Err at the first failed predicate, which makes the failure a value. The error names the failing predicate, a snapshot of the fields, and location, the construction call site as file:line:col, including the invocation of a stored or passed constructor. Email.unchecked(value) -> Email is file-local and bypasses validation.

An opaque type with a where block has no bare constructor: Email(value=…) is a compile error even in the defining module. Use .new for the Result or .unchecked for the file-local bypass. For Option-style use, match on it: match Email.new(s) ... Ok(e) -> Some(e) ... Err(_) -> None ... end.

A Type.new(literal) whose predicates provably fail folds to a compile error. That applies to comptime-known arguments; a non-literal argument checks at run time. where blocks are available on non-generic opaque types.

Derived Decode, explicit or on demand, calls .new after decoding the fields. A failed predicate returns deserializer.InvalidValue(validation.ValidationError, int) in the Err arm. The integer is the cursor position after the fields; the validation error preserves the predicate, label and field snapshot, with location identifying the opaque type declaration. Field and framing errors propagate before validation. Generated validation runs at decode time, including for a fieldless type. This applies to every format and both tiers.

11. Traits and impls

trait Display
  def to_string(self) -> string
end

impl Display<Point>
  def to_string(self) -> string
    "(#{self.x}, #{self.y})"
  end
end

impl Display<Point> reads "Display applied to Point". A generic impl introduces its parameter from the parameter position, impl Display<Container<T>>, and a constrained one reads impl<T: Show> Display<Container<T>>.

Signature conformance

An impl's method signatures must conform to the trait's. Parameter and return types equal the declaration, with Self the implementing type, and an action's effect row must be a subset of the trait method's row: fewer effects are fine and more are refused. A divergent type or a widened row is H0617, since bounded and static dispatch charge the caller the trait's signature and effects.

A call on a concrete receiver is charged the impl's row. The trait's row is a ceiling and no floor: a narrower impl row is what the call gets wherever the receiver's type is known.

A trait method may declare its row as a single effect variable, def read!(self) -> bytes [e]. No ceiling then applies: each impl declares concretely whatever it performs, and a variable in an impl has nothing to solve it (H0648). A bounded generic names that row through its bound, <S: Stream[e]>, and is charged the impl's own row at each call site. A row is one form or the other, and a variable among concrete effects is H0647. A bound may name a row only where the trait or a supertrait leaves one open (H0649), and calling such a method through a bound that did not name the row is H0650, in place of charging an atom the signature cannot name. Forwarding a generic argument to a callable whose bound names a row also requires that row on the enclosing bound (H0650), even when an unrelated callback happens to use the same letter.

Bound effect rows resolve after argument and result type inference, including numeric literal defaults. When a row variable is shared by bounds and callbacks, each call requires the union of all selected implementation rows and callback rows. This also applies to saved function values and higher-order arguments; their callback rows are solved separately at each invocation. Row names are local to each signature, and forwarding preserves independent caller rows even when a callee uses the same letters. A parameterized bound selects its implementation with the complete type argument tuple after expanding trailing defaults.

Default methods

A trait method may carry a default body: def greeting(self) -> string "hi, #{self.name()}" end. An impl that does not override it uses the default, and a default body may call the trait's other methods on self. An inherent or impl override outranks the default.

Bounds

A trait bound lets you call that trait's methods on the bounded parameter. def same?<T: Eq>(a: T, b: T) -> bool can write a.eq?(b), dispatching to the concrete impl, Eq<i32> or Eq<string> and so on. Under a Display bound, #{a} interpolation is a.to_string(). A bare T with no bound has no methods.

Bounds work on both tiers, on free defs, on impl heads (impl<K: Hash, V> Map<K, V>), on generic trait-impl heads, on a method's own generic (def both_eq?<U: Eq>(self, x: U, y: U)), and on static trait methods (def decode<D: Deserializer>(d) -> Self). Several bounds join with +: def f<T: Display + Eq>(…) brings both traits' methods into scope on T. Use + for an unrelated second trait; a supertrait comes free.

A bounded function value retains its bounds: f: (i32) -> string = render instantiates render<T: Display> at i32, rejects a missing implementation, and captures the dictionary, including one forwarded by a generic caller. This also applies to qualified references, higher-order arguments and inherent associated functions with impl-head or method-own bounds, on both runtime tiers and during constant evaluation. Its associated result type becomes available as soon as the arguments or surrounding function type select the implementation. A generic caller must carry the required trait with the same default-expanded type arguments; a missing or incompatible bound is H0555 at the call or function reference, including bounds forwarded through a generic implementation. A stored function's bound effect row follows the type that selects the implementation; a caller may forward it under its own row name and a concrete function annotation may select a concrete row.

Supertraits

trait Hash: Eq declares Eq as a supertrait. impl Hash<T> then requires impl Eq<T>, and a T: Hash bound brings Eq's methods, along with == and !=, into scope beside Hash's. A trait takes one supertrait, and the relation is transitive along the chain.

Trait type parameters and associated types

trait Combine<B> declares a per-impl type parameter, and type Out in the body declares an associated type. An impl supplies them positionally after Self, impl Combine<Thing, string>, and binds every associated type, type Out = bool. A trailing default, trait Add<Rhs = Self>, lets a homogeneous impl write impl Add<Period>, which is the same impl as the spelt-out form. A default is a bare type name, and a composite such as = List<Self> is H0569.

Inside the trait and its impls the names resolve to that impl's bindings, as in def mk(self, b: B) -> Out. An ordinary caller never names an associated type and observes one as the call's result type. A generic impl's binding projects through instantiation: impl<T> Un<Box<T>> with type Out = T.

A bounded generic is the exception. A trait declaring associated types can be bounded, <S: Stream>, and its associated types are reached by projecting off the parameter: def frame!<S: Stream>(s: S) -> Result<Frame, S.Error>, abstract in the body and the chosen impl's binding at each instantiation. The projection names the parameter and not the trait: two bounds declaring one name is the ambiguity H0302, and a bound the call cannot pin is H0555.

An associated declaration may bind every implementation, type Error: Display; each type Error = T must satisfy it, and <S: Stream> may rely on S.Error: Display. Add a use-site requirement in the same generic list: def serve!<S: Stream, S.Error: Into<HttpError>>(s: S) …. The dotted entry is a constraint subject. It adds no type parameter and changes no generic arity. It must carry a bound after :, cannot have a default, and an unsatisfied binding or instantiation is H0555.

Coherence and impl selection

Coherence is per slot: Add<Instant, Duration> and Add<Instant, Instant> coexist; nominal slots compare base names, while function and Future slots compare complete structural patterns, including repeated parameters and effect rows, and overlap only when a common instantiation exists. A duplicate or a wildcard overlap is H0516, and a shape error, wrong arity or an unbound or unknown binding, is H0570.

Where several impls share the receiver's type, the argument types select the impl. x.add(y) picks by y's type, and the winner's Output types the call. Arguments must be concrete, which means suffixing your literals, and must fit some impl, else H0571. A bare-dot prop read has no argument to select by, and multi-impl resolution of one is therefore H0619. That error names the competing impls, and renaming yours is the fix; one of them may be a stdlib impl from a module another file of the program imports, such as datetime's days and hours on int.

Operators ride on this. Non-numeric + and - dispatch through the core Add and Sub in module ops, which is in the prelude, selecting by the operand pair, and the result is the impl's Output. The numerics never route here, and a cross-width + therefore reports its conversion error. t += d inherits the dispatch, where §12 pins Output to t's type, and a field target folds the same way.

module.load! takes a plain trait, permanently: a handle's method result must be a type the host knows, and a loaded module's own associated binding is not one.

A bound supplies the trait's parameters the way an impl head does, with Self the bounded parameter and never written. <T: Add> is Add<T, T> through the Rhs = Self default, and <T: Add<Duration>> is Add<T, Duration>. The whole tuple selects the impl, including nested types and function or Future rows, with repeated parameters required to agree: at Instant the second resolves and the first reports no Add<Instant>. Inside the body Rhs is a type. Wrong arity is H0570, and two bounds on one parameter naming one trait are H0569. a + b with a bounded generic on the left dispatches through the bound, and p.f += d folds through it too, at any depth.

Core into declares Into<To>, with @transform def into(self) -> To. Self is the source and To the target; a bound such as S: Into<HttpError> fixes that target before generic code calls s.into(). One source may implement several target slots. A bare concrete call has no value argument to choose among several candidates and is then ambiguous, while bounded dispatch gets the choice from its dictionary. There is no reverse blanket twin and no derive; conversions are hand-written. The same trait dictionaries run on bytecode and AOT.

Four shapes are staged and report H0569 today: a generic parameter as the right operand of a concrete left (the pair selects the impl; call the method on the parameter), an operator on a parameter with no operator bound, static dispatch on a concrete type through a trait declaring type parameters (through a bound it resolves, since the bound supplies the arguments), and default bodies on such traits.

Inherent impls

impl <Type> ... end (no trait, no <...> args) attaches methods directly. Declaration order is free, as it is for actors: the impl may sit above the struct or type it is for.

impl int
  def parse(s: string) -> Result<int, ParseError>
    # ...
  end
end

x = int.parse("42")         # Ok(42) — associated fn dispatch, through a trait
e = Email.parse("a@b")

A method, whose first parameter is self, dispatches through value.method(). An associated fn, with no self, dispatches through <Type>.fn(args), for an inherent impl or for a no-self trait method. The same works through a bounded type parameter: in a <T: Trait> body, T.fn(args) dispatches to the concrete impl through the trait dictionary. That is the no-self counterpart of value.method(), and it lets a generic codec write T.decode(bytes, pos). The type is always named, there being no inline type arguments (§11), and the receiver therefore pins Self. Qualified types work in both calls and inherent function values: model.Colour.tag(x), xs.map(model.Colour.tag) and bytes.BytesBuilder.new!.

Properties

A prop is a pure, self-only value read with bare-dot syntax and no parentheses: 2.days, point.magnitude. Declare it prop name(self) -> Ret in a trait or impl body; prop is a contextual keyword, and a trait prop may carry a default body.

Each member has one spelling. Bare dot, x.name, is a struct field or a prop, a pure read where nothing happens. x.name() is a def method, an invocation. x.name!(…) is an action with world effects. Reading a prop with parentheses, 2.days(), is H0567.

The stdlib's own attribute reads are props: length and empty? on List, Map, Set, Range, string and bytes are bare (xs.length, s.empty?), while the computing members sort, trim and keys stay def. A prop must be self-only and may not declare method-own generics. It must not collide with a field name (H0566), including a hidden opaque field, where renaming the backing field re-exposes it; a compiler-derived prop such as Hash.hash is exempt, and the field wins the bare-dot read. An impl must match the trait's kind, prop against def, or H0568. Props are absent from actors and from top level. A bounded-generic receiver works: <T: Hash> x.hash dispatches through the bound's dictionary.

A pure, self-only, zero-argument def in an inherent impl or in a trait declaration is the should-be-prop error H0574, with a machine-applicable def to prop fix; it is downgraded to a suggestion when the name shadows a field. At a trait declaration the declared kind cascades to every impl (H0568). Hash.hash is therefore a prop: x.hash, never x.hash().

The exemption is a transformation: the to_, into_ and from_ prefixes by convention, and any other member marked @transform def, such as sort and trim, in trait declarations too. A misplaced @transform is H0620. Out of scope are trait impl members, whose kind the declaration mandates, meta, @encapsulated, @intrinsic (that surface is the primitive conversions and the maths, transformations by name), and method-own-generic members.

The cross-tier conversion methods, i32.to_f64 and int.to_i64 among them, are inherent methods on the source type.

A float's raw IEEE 754 bits are reachable with f64.to_bits() -> u64 and f64.from_bits(u64) -> f64, and with f32.to_bits() -> u32 and f32.from_bits(u32) -> f32. Each pair is an exact inverse over all patterns, signaling NaNs included. The f32 pair narrows to 32 bits first, an f32 being stored in an f64 slot, and moves a NaN's payload between the two mantissa widths where the conversion would otherwise quiet it. Arithmetic still quiets a signaling NaN, per IEEE. f32.from_bits is the only way to build an f32 from a computed value, since nothing in core converts into f32.

The same-width signed and unsigned reinterprets, i32.to_u32 and u32.to_i32, i64.to_u64 and u64.to_i64, keep the bit pattern and are total exact inverses. They are the seam a binary codec uses to reach a number's wire bytes. The bitwise ops are methods and not operators, as §3 says.

A generic inherent impl, impl<T> Option<T>, works the same way: the impl's type parameters unify with the receiver's concrete arguments at the call site.

impl<T> Option<T>
  def unwrap_or(self, default: T) -> T
    match self
      Some(v) -> v
      None    -> default
    end
  end
end

Some(7i32).unwrap_or(0i32)   # T = i32

There is one impl per base target type, and mixing a generic and a concrete impl on the same type is rejected. Likewise there is one trait impl per pair of trait and head type name. Overlapping impls are an error and specialization is unsupported; fold the concrete case into the generic impl. The head must name a type: impl Wrap<T> is a blanket impl, which Hanki does not have, and it is refused (H0570). A head that names one may still be generic, and impl<T> Base<Wrap<T>> resolves by Wrap. The head name is module-qualified, and a stdlib impl therefore never reserves its head's bare name for your own types.

12. Generics

struct User
  name: string
end

def first<T>(xs: List<T>) -> Option<T>
  xs.get(0)          # index is `int`, not a fixed-width literal
end

def demo() -> ()
  list: List<i32> = [1i32, 2i32, 3i32]
  m: Map<string, User> = Map.empty()    # type args inferred from the binding
  ()
end

Type arguments are inferred from a unique assignment, including constraints in a function slot's throws payloads, and are never supplied inline:

# ERROR — Hanki has no <T> at call sites; type args are inferred:
n = parse<i32>("42")
n = parse::<i32>("42")

# RIGHT — call the associated fn; the result is a Result:
n: Result<i32, ParseError> = i32.parse("42")

Where inference cannot pin a parameter, the compiler names the place to add an annotation.

13. Closures

use io

def demo!() -> () [io]
  [1i32, 2i32, 3i32].map(|x| x * 2i32)   # inline: `)` bounds the body, no `end`

  [1i32, 2i32, 3i32].each! |x|           # trailing block: `end` closes it
    io.print!("#{x}\n")
  end
end

• |args| body is the only closure form. It takes no effect marker, and effectfulness is inferred.
• Inline, f(|x| EXPR): a single-expression body bounded by ) or ,, with no end. The body may sit on the same line or begin on the next line indented under |params|, and in both placements it is one expression; use do … end for a sequence. A fold or map step with an if … end body therefore needs no helper. This form also serves a non-last argument: apply(|n| n * 2, 5).
• Trailing block, f |x| … end: the closure is the call's last argument and end closes it. The body is a do … end block with the do implicit, a statement sequence whose value is the last expression, or (). It suits builder blocks, a sequence of c.add!(…) calls, and a multi-line if, match or loop.
• Effectfulness is inferred and gated by the callee's bang. A pure combinator such as map or find rejects an action call in the body; an action combinator such as each! allows one and propagates its effects to the caller.
• Every List combinator taking a callback has a pure form and an effect-polymorphic ! twin: map!, filter!, fold!, find!, find_map!, any!, all!, flat_map!, partition!, take_while! and count!. An effectful traversal therefore needs no hand-rolled index loop.
• For a fallible effectful pass, try_fold! and try_each!, on List and on bytes, take a step returning Result and stop at the first Err. They are the way out where a failure mid-traversal would otherwise ride a poisoned accumulator or a hand-rolled loop with a flag. try_each! covers the common case: perform each element's effect, and stop at the first failure.
• Option and Result are paired the same way: option.map!, and_then! and or_else!, and result.map!, map_err!, and_then! and or_else!. Each is performed only on the branch its pure form would run, which leaves an effectful step over an absence or a failure needing no explicit match. Use the ! form where the callback needs an effect and the pure form elsewhere; only the pure form is callable from a pure def, a where block or a meta block.
• sort_by, min_by and max_by are pure-only. An effectful comparator need not be consistent between calls, which voids the sort's guarantees. Map the effect in first, then sort.
• Parameter types are inferred from the expected function type at the call site.
• An inline body is one expression, and anything else is a parse error; a trailing block may sequence. In both forms, a nested loop or a match with three or more arms wants extraction into a named def or def!.
• A closure captures by value, and assigning to a captured binding is therefore H0209. The write would hit the closure's own copy and be discarded, which would make var total = 0 with each! |x| total = total + x end print the pre-loop value. Accumulate with a loop in the enclosing body, or with a fold that returns the accumulator: xs.fold(0, |acc, x| acc + x). The closure's own parameters and var locals remain writable, and a parameter shadowing a captured name is its own. A field write rebinds its root (§5), and c.v = x through a captured c is refused too.

14. Modules and imports

One file = one module. Module name = file basename.

use io          # qualified: io.print!, io.read_line!

open option     # unqualified: Some, None drop into scope bare

def greet!(name: Option<string>) -> () [io]
  match name
    Some(n) -> io.print!(n)
    None -> io.print!("hello")
  end
end

• Canonical layout (hanki fmt): use section first, then open section, one blank line between them, none within a section, each sorted by dotted path.
• use NAME is qualified, and is the default. Members are reached as NAME.member. A function or action can be stored by its qualified name, as in f = io.print! after use io; its type includes the effect row. NAME is a file stem, flat across the project: the module is found wherever its file sits under the project root. A subdirectory organises files and appears in no import, and two files of one stem anywhere in the project are an error naming both. A directory with its own hanki.config.hk is another package.
• open NAME is unqualified and drops names bare. The core stdlib basics list, option, display, eq? and str are usually opened by user code; none of them is auto-opened. For bare Some and None, write open option; without it, the qualified option.Some and option.None are the only way to reach them.
• The same applies in patterns, arguments or not: a Some(v) -> arm needs the open as a bare None -> does, and one match never takes two import rules. A scrutinee's type picks between in-scope variants sharing a name and brings none into scope. The expression side mirrors it: a variant name that several sums of one module share resolves by the expected type, an annotated binding, a parameter or a return position, and with no type context it is the ambiguity error H0624, decided by nothing and never by declaration order.
• A bare use of a name two opens export is the ambiguity error H0306. So is one an open shares with a module in scope, whether from use util or from the ambient list. Co-opening remains legal: write the qualified module.Name. A name the file declares shadows all opens and is never contested.
• use NAME as n is a file-local module-rename alias: reach NAME's members under n, and use http as h then gives h.get! and h.Response, resolving as http.…, with the gating still applying to http. It resolves a clash where two dotted imports would land on one qualifier. It is use-only, and open NAME as n is a parse error. as is contextual and remains usable as an ordinary identifier.
• use DEP.NAME reaches a dependency's other exported module. DEP is a binding this package's manifest declares, NAME is one of the modules that package exports, and the qualifier is NAME: use entsoe.model gives model.Doc. open and as work as on any import. The head is never a stdlib module or a project module, and a path is at most two segments. Two imports on one qualifier is an error, and only an as can cause it. It does not rename the module: two model.hk modules in one program still collide, since items are keyed by module basename.
• Core is ambient-qualified and the extra tier is import-gated. A core module's qualified spelling, option.Some or list.map, resolves with no use or open. The extra tier (io, fs, net, http, time, datetime, json, xml, csv, terminal, random, env, process, path, cbor, vcs, supervisor, sqlite, log, base64, base32, hex, sha2, sh, flags, uuid, glob, parsecheck, diag, tls) resolves nothing, neither function nor effect-op nor constructor nor type, until the file uses or opens that module (H0301, H0302). The effect-row capabilities [io], [net] and [fs] are built-in atoms and no module's members, and they need no import; io itself is still import-gated, and is conventionally opened for a bare print!.
• The prelude is the pair of exceptions to "nothing is auto-opened". First, the trait names Eq, Ord, Add, Sub, Hash, Display, Encode and Decode, plus Ordering, Less, Equal and Greater so that cmp's result is matchable, are in scope unqualified everywhere; their behaviour through operators, rendering and serialization is already ambient. Only the Encode and Decode names enter from those two modules: a sibling such as decode.max_decode_depth remains qualified or needs open decode. Second, the container type names List, Option, Result and Map resolve to their stdlib types everywhere, which lets a face returning List<T> ship the real methodful type with no open list. The type names alone are covered: the variant constructors Some, None, Ok and Err and the bare stdlib functions still need open. A local declaration of the same name shadows the prelude.
• Every top-level item sits at its module-qualified name, option.Some or todos.Todos, and a cross-file reference either spells that or uses open.
• A name starting with _ is not exported.
• An unused import is the compile error H0625, and hanki check --fix deletes the line. A core-module use is never needed. Dispatch into a gated module counts as use, and an import of a module carrying test blocks or a provide is never reported: the lint may miss a dead import, and never deletes a live one.

Stdlib modules are auto-injected, and use io therefore resolves with no file on disk. They are not auto-opened: a program using a bare Some, None, Line or Eof opens the relevant module itself.

A local file may not shadow a stdlib module name. A list.hk or time.hk beside your code is refused: use list always binds the stdlib, and the workspace rejects the colliding file where it would otherwise be ignored. The 90 baked module names are therefore a compatibility surface. Adding one claims a basename no project may use, which makes a stdlib addition a source-breaking change announced with the name it claims, with a rename and a removal on the same footing, and the list is pinned in a test so it cannot grow by accident.

A local binding named after a module does shadow it in value position, whether a parameter, a let or a var. module.length is then the local value's length property under ordinary lexical scoping, and the module is unreachable by that name in that scope.

A module and a same-named type compose in member position. A type-named stdlib file such as i8.hk has both module-level defs and impl i8, and a user file does the same when point.hk declares type point. i8.name resolves against the module's exports first and falls through to the type's associated fns on a miss. Declaring a top-level item that a same-named type also supplies is the compile error H0623 at the declaration, and renaming one is the fix. An effect name composes with a same-named type the same way, checked at the use and not at the declaration (H0633).

15. Actors

The third of the three layers of §1: the unit of concurrency, isolation and hot reload, built from actions, since every on handler is an action. Each actor runs on its own OS thread with its own reference-counted heap, freed at the last handle drop. There is no tracing collector.

use io

actor Counter
  state n: i32 = 0

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

  on get() -> i32
    n
  end
end

def main!(args: List<string>) -> () [io, throws actor.SendFailed]
  c = spawn Counter           # ActorRef<Counter>
  c.increment()               # blocking send (parens required)
  c.increment()
  io.print!("n = #{c.get()}") # blocks, gets handler return
end

• state X: T = default declares per-actor mutable fields. state is contextual (like migrate, as, prop): a keyword only in actor-member position, an ordinary name anywhere else - def f(state: string) is fine.
• on name(args) -> Ret [extra effects] declares a message handler. [state] is implicit on every on; list only the other effects.
• spawn Actor returns an ActorRef<Actor>, a typed opaque handle. Declaration order is free: an actor may spawn one declared later, and mutually-spawning actors therefore need no forward declaration.
• spawn Worker(limit=5i32, mode="fast") replaces selected state defaults by field name. Names must be declared state fields, values must match their types, duplicates/unknown names and positional initialisers are errors, and omitted fields keep their defaults. Expressions evaluate in written order on the spawner and cross heaps like send arguments (field=move resource for a resource; no futures, secrets or nested resources); an overridden default is not run. The combined state then takes the initial where check. mailbox= and supervisor= remain reserved options and compose with state initialisers.
• c.method() is a blocking send, the counterpart of Erlang's gen_server:call, and the parentheses are required even for a zero-argument handler. It returns the handler's T. A bare c.method is a field read, and an ActorRef has no fields: the result is H0565, with a hint to add the parentheses.
• async c.method() returns a Future<T>, a linear one-shot. Extract it with await f, or with a deadline through actor.await_timeout!(f, ms). Await it at most once: a second await, plain or bounded, of the same binding is a compile error, best-effort, mirroring use-after-move. An await escape that slips past the static check faults the actor at run time with a future was awaited more than once, on both tiers, and never as a catchable Timeout. Discarding a future, with zero awaits, is free.
• async c.method() in statement position, which is to say not as the block's trailing expression, is fire-and-forget. The send's [throws actor.SendFailed] is demoted to the caller's row: declare it or wrap the send in try … catch. The handler's own throws stay with the receiver. A wildcard _ = async … and a never-awaited let-binding are both rejected, since either would swallow SendFailed.

What crosses a send

Mailbox values are deep-copied between heaps. Primitives, strings and actor handles pass cheaply, and tuples, lists and sum payloads are walked recursively, preserving internal aliasing; values are acyclic (§5), and the walk therefore terminates.

A resource is moved and never copied (§4). move x consumes the sender's binding. A resource as a return type, as a throws type or nested in an aggregate is rejected; put a long-lived one in state.

A Future is not Sendable and cannot cross a message boundary, as a parameter, a return or a throws: sharing one reply slot across actors would deadlock both. Await it in its origin actor and send the resulting value.

A Secret is not Sendable either (§4). Where a resource has something to move, the material here would be copied, and a Secret is therefore refused outright as H0635, nested as well as direct, and inside a closure type's signature. A closure's captures are outside the rule, since they are absent from the type (§4). Keep the secret in state, or reveal it and send what the handler needs.

Throws do not cross sends. A handler's [throws E] is the receiver's and never reaches the sender: an uncaught handler throw takes the actor down and surfaces as actor.SendFailed::Died. To return an error to a caller, a handler returns it as a value, -> Result<T, E>. The one throw a send raises is actor.SendFailed.

Bounded mailboxes

The default capacity is 1024 envelopes, and spawn Counter(mailbox=N) overrides it with a compile-time positive int literal. mailbox= and supervisor= are reserved spawn options; other keyword args name state fields.

Every send picks up [throws actor.SendFailed], a sum of MailboxFull when the receiver is at capacity, Died(ActorId, DeathCause) when it has terminated, and Timeout when an actor.await_timeout! deadline passed. A blocking send and a statement-position fire-and-forget throw at the call site; a let-bound async folds the throw into the Future and surfaces it at await.

Discriminate with an inner match, using open actor for a bare MailboxFull, Died or Timeout, or interpolate the value: SendFailed and DeathCause both carry Display and render mailbox full, reply timed out and actor <name> died: <cause>, in the words the runtime's own death report uses. The actor keyword doubles as the module name and serves as a qualifier head.

Bounded await

actor.await_timeout!(f, ms) is a compiler special form on the actor module head, and is await f with a deadline. It yields the future's T, counts as the future's await for the discard rule, and throws SendFailed::Timeout when no reply lands within ms milliseconds; ms is an i32, and a negative one counts as 0. A timeout cancels nothing: the handler still runs, and its late reply is abandoned.

Under --deterministic the deadline is virtual, on the same gate clock as time.sleep!: timing out takes no real time and replays per seed. The exception is a deadline bounding an actor parked in a real OS call, which retains its turn. The gate then spends the deadline on that call in real time, a peer answering within the bound still wins, and one that never answers still times out where it would otherwise hang the run (§17).

Supervision

Every actor has a supervisor link, by default the actor that spawned it. Override it with spawn Worker(supervisor=ref), where ref : ActorRef<T> and T declares on actor_died. Inside a handler, self is the actor's own ref and is a valid supervisor= target.

On a death the runtime fire-and-forget-casts on actor_died(who: actor.ActorId, cause: actor.DeathCause) -> () to the supervisor. The signature is fixed and the names are free. ActorId is opaque: handle.id() obtains one from an ActorRef<T>, and who.name reads the declared actor name. Store each spawned child's id and compare it with who to distinguish two children of the same type. Equality uses the packed slot-plus-generation identity alone, never the diagnostic name, and remains correct after slot reuse. Display freezes that full logical identity as <name> #<slot>.<generation>, for example Worker #1.0; the packed integer remains private. This death cast is capacity-exempt, following Erlang's exit-signal semantics: a supervisor at its mailbox= cap still receives every child's actor_died, serviced ahead of its queued messages; backpressure drops none of them and fails no run.

The fixed on signal(sig: sys.Signal) -> () handler is an ordinary actor action with its own declared effects. sys.watch_signals!(target, signals, grace_ms) -> Result<(), sys.SignalError> [process] requires a concrete actor declaring that handler, including when the registration function is stored as a value. Every registration watches SIGTERM and SIGHUP; including sys.Interrupt also watches SIGINT. Empty lists retain the defaults and duplicates have no additional effect. A successful call replaces the process-wide watcher; failure preserves it. Grace is i32 milliseconds: negative fails and zero guarantees no cleanup. Conflicting inherited dispositions and unsupported platforms return structured errors. Use hanki doc --find Signal for the signal variants and registration failures.

Terminal restoration precedes actor delivery. The lifecycle message is capacity-exempt and serviced ahead of ordinary mailbox work. Grace starts at the signal event and includes restoration, queueing and handler execution. A busy handler is not preempted. Completion, delivery failure or deadline expiry restores the original signal's default disposition and re-raises it, retaining conventional signal termination. A dead target cannot perform cleanup. With no registration, terminal restoration is followed by immediate re-raise. Both runtime tiers follow this contract. SIGKILL is outside the surface. Without an actor watcher, restore-byte output is best effort, with a 100 ms watchdog deadline starting after terminal state is restored, subject to OS scheduling. A blocked stdout may receive incomplete output. If the watchdog cannot be prepared or notified, signal restoration skips output and re-raises after restoring terminal state. Stdout file-status flags are unchanged.

The link is ownership downward too. When a supervisor dies for any cause, an explicit shutdown included, the runtime tombstones it and requests ExplicitShutdown of every live direct child before sending the supervisor's own death cast or escalating. Each child repeats the protocol; the whole subtree winds down, leaving no live actor linked to a dead supervisor. The cascade is asynchronous; sibling order and a per-child deadline are unspecified. A spawn naming an already-dead or stale supervisor is born shutting down: registration races atomically with the death scan. The child is either scanned or starts with ExplicitShutdown pending, never orphaned. Pending child callers see Died(_, ExplicitShutdown). A pending shutdown wins over a racing handler fault; if the fault began first and its cast finds the supervisor dead, the downward cascade already owns it and the death is not re-escalated to root.

DeathCause is a five-case sum.

• UncaughtThrow
• InvariantViolation(predicate, label, fields)
• HostPanic
• ExplicitShutdown, from an actor.shutdown! of the actor. A call to a shutdown-closed mailbox also fails Died(_, ExplicitShutdown) where it would otherwise hang, and a cast to it is absorbed.
• Gone, from a stale ActorRef whose actor died and whose slot a later spawn recycled. The original cause is no longer retained. A send to a still-dead and not-yet-reused actor continues to return its real cause.

An actor that spawns a child without supervisor= must declare on actor_died, since it becomes that child's supervisor. main! is the root: a fault reaching it exits the process non-zero, with a crash-time state dump of the dying actor on both tiers through the dbg! renderer. An ExplicitShutdown is orderly and reports nothing. The death sources are crash!, an uncaught throws, a violated state invariant, and actor.shutdown!. Arithmetic never dies (§3).

Timers

actor.send_after!(target.handler(args), ms) is the scheduler-side delayed-cast special form. The invocation is static delivery syntax and does not call the handler now. The form returns (), requires [time, throws actor.SendFailed], and takes an i32 delay; negative clamps to zero.

def schedule!(worker: ActorRef<Worker>) -> () [time, throws actor.SendFailed]
  actor.send_after!(worker.tick(1i32), 500i32)
end

Arguments copy or move when scheduled. One target-mailbox slot is reserved immediately and counts toward mailbox= capacity: a dead or full target throws synchronously, and an accepted timer cannot later fail for MailboxFull. Target death or program exit cancels the retained envelope, releases the slot, and drops its values and resources.

One scheduler timer wheel serves the program, with no actor parked. Under --deterministic, deadlines use virtual time and replay per seed; equal deadlines fire in registration order. At firing, the cast joins the regular mailbox tail. A message racing that instant follows the run's scheduler order.

A periodic handler re-arms with actor.send_after!(self.tick(), period) after its work and checks a state flag to stop. Backoff uses the same form with a growing delay. extra/supervisor.RestartPolicy(max_restarts, base_ms, max_ms) answers Restart(delay_ms) or GiveUp; its delay calculation clamps a non-positive base or ceiling to zero and saturates before i32 overflow; even an extreme restart count takes bounded work. For restart intensity, keep one RestartWindow per logical child slot or strategy group and configure RestartIntensity(max_restarts, within_ms). intensity.next(window) yields RestartAllowed(updated) or IntensityExceeded; store the update and carry its epoch in the delayed restart. After the replacement is spawned, schedule one expiry handler for within_ms; it applies window.expired(epoch). An old epoch is inert; the last expiry advances it, and window.reset() is reserved for discarding or reassigning the logical slot or group; an ordinary respawn preserves the window. Each charge expires independently; the sliding window has no fixed bucket, and a replacement that runs for the full interval clears its charge. Match same-type children by each current ActorRef.id(). Never charge or restart ExplicitShutdown. At the exact boundary the handler processed first decides: queued death mail has priority, otherwise deterministic scheduler order (and equal-timer registration FIFO) is replayable. The supervisor remains free to receive deaths throughout. Use time.sleep! instead when the current actor action itself must pause; messages then queue behind that sleeping handler.

Stopping an actor

actor.shutdown!(target) is a compiler special form on the actor head, as await_timeout! is. The optional deadline form is actor.shutdown!(target, kill_after=ms), with ms: i32; negative clamps to zero. It winds an actor down, including one parked in a cancellable OS call (accept!, read!, write!, connect!, stdin read_line!, the timed sys.stdin_read!, a process.run! awaiting a child, or a Child pipe read, write or wait) and one grinding inside a long SQLite statement, aborted between VDBE ops by the connection's progress handler. Dropping an owned Child terminates and reaps it.

It returns a total Future<actor.Shutdown>. Read the outcome with await or actor.await_timeout!, or drop it for fire-and-forget: it has no throw, and a send Future's discard rule therefore does not apply, which leaves statement-position actor.shutdown!(t) fine. It is still a one-shot, awaitable at most once.

The outcomes are Terminated, which was live and is now fully down, AlreadyDead, which makes the call idempotent, SelfScheduled, since actor.shutdown!(self) cannot wait on its own death and instead exits at the end of the current handler, and deadline-only TimedOut. A timeout says the target had not reached a shutdown safe point: the request remains active and the target may terminate later. The target's lifetime is unbounded by that timeout. The deadline begins with the request and is virtual under --deterministic. A death racing it resolves once as either Terminated or TimedOut. SelfScheduled is the clean self-stop, and crash! is the other thing. A supervised target's on actor_died receives ExplicitShutdown, and an unsupervised one dies with no report.

The bytecode VM treats each taken backward branch as one cooperative reduction. At the 16,384th reduction it checks actor-local and whole-program shutdown, unwinding normally to ExplicitShutdown when set; otherwise it yields the scheduler and resumes the same VM and handler, admitting no second message. Pure synchronous intrinsics do not reset the count. Under --deterministic this fixed control-flow point yields the seeded run token and replays identically; it remains runnable and does not advance virtual time. Straight-line compute and recursion reach no such point. Native AOT loops have no poll: the required back-edge countdown and scheduler handoff regressed tight-loop and allocation-heavy benchmarks before shutdown/unwind work; it failed the net-performance-positive gate and is omitted. Mailbox and blocking-call shutdown still work on both tiers, but a pure-compute AOT handler may time out. This is the intentional parity gap recorded in HANKI.md §22.

Request-scoped workers

An actor is independent of the stack frame that spawned it, and a handler that spawns workers, fans work out and returns has not stopped them. actor.stop_all!(targets: List<ActorRef<T>>, kill_after: i32) -> List<Shutdown> is the completion boundary such an operation returns through. It signals every target first and collects every outcome afterwards, which puts one deadline over the whole set, and answers one Shutdown per target in the order given. A stopped worker's handler unwinds as ExplicitShutdown and releases its owned resources, a resource moved into it included, before the call returns.

Four limits bound it. The stop runs where it is written, and Hanki has no exit hook. A return ahead of it, or a throw caught inside the same actor, leaves the workers running. A throw that escapes the handler kills the spawning actor, and the supervisor cascade then shuts its workers down without waiting. A failing worker does not stop its siblings; the failure arrives at the awaiting scope as SendFailed::Died, and the siblings run until the stop_all!. The spawning actor's on actor_died fires for every scoped worker that dies, after the current handler returns, and a restart policy tells a scoped worker from a long-lived child first. And TimedOut is a report and no guarantee: a target wedged in native compute on the AOT tier reaches no safe point and may terminate later, and a stopped actor's own children wind down asynchronously. An actor is an OS thread and two descriptors, which bounds this to a few workers per operation; per-item parallelism is a worker pool the operation sends to.

Program exit terminates spawned actors and does not wait

When main! returns the program is over. The runtime tears down every live spawned actor, interrupting a parked cancellable OS call (accept!, read!, write!, connect!, read_line!, sys.stdin_read!, process.run!, or a Child pipe operation) and a parked virtual sleep (the deterministic gate wakes the sleeper with ExplicitShutdown and does not advance the virtual clock), and any in-flight SQLite statement, as actor.shutdown! does, and dropping unprocessed messages and owned resources. A dropped Child terminates and reaps its subprocess; process.spawn_detached! is the explicit handle-free exception. A fire-and-forget handler that has not finished may therefore not run to completion. To keep work alive, block in main!, with await actor.shutdown!(s) or by awaiting a result. Both tiers release the root's and actors' owned resources before a fatal exit as well, preserving the fault's exit code (§6).

State invariants

An actor may end with a where block of bool predicates over its state fields, after the handlers and before end, mirroring the opaque-struct surface of §10.

actor Counter
  state n: i32 = 0
  on dec() -> ()
    n -= 1
  end
where
  n >= 0 else "count must never go negative"
end

The predicates run after each successful handler return and once after init. A violation terminates the actor with DeathCause::InvariantViolation and throws nothing to the sender. The predicate scope matches opaque types: state fields by bare name, with no self, no actions, no effects and no methods on the actor type. A spawn whose effective initial state (defaults after named overrides) is comptime-known and violates a predicate is a compile error (§16); an overridden default is neither folded nor run. Both tiers behave alike.

Hot reload

A handle takes its trait from the binding's annotation, m: Module<Greeter> = module.load!(path), and there is no call-site type argument. Interface matching treats bare and documented qualified native resource names as the same type, including inside collection and function types.

m2: Module<Greeter> = module.reload!(m, path) swaps a live loaded actor to recompiled code at its next safe point. The in-flight handler finishes under the old code and later messages run the new one; the actor and its mailbox survive.

The same state layout brings the state across. A changed layout needs a migrate(old: T) hook, which has an implicit [state] row and returns (), where T mirrors the previous state, built from defaults and then overwritten from old. Without the hook the reload throws module.ModuleLoadError::StateMigrationRequired and leaves the old code in place, atomically. Reloading a function-mode handle re-points its vtable at the recompiled code, with no actor and no migration, on both tiers.

Two failures no migrate hook can fix have their own variants: a mode switch between actor and function exports throws ModeMismatch, and a dead or unloaded handle throws InvalidHandle.

Use after unload!

A method dispatched through a handle that unload! has released throws a catchable module.ModuleHandleInvalid, whose sole variant is Released. It is a separate type from ModuleLoadError.

Every Module<T> method call therefore has [throws module.ModuleHandleInvalid] in its row, a pure def method included: the throw belongs to the handle dispatch and not to the method, the same universally-injected shape SendFailed has on sends. A trait prop is read bare-dot through the handle, m.answer and never m.answer(), which would be H0567, and that read charges the same throw. Declare it, or write try … catch e: module.ModuleHandleInvalid. The value is identical on both tiers, and a use-after-release therefore fails as a typed throw and never as a null-pointer dereference.

actor Counter
  state total: i64 = 0

  on add!(n: i64) -> ()
    total += n
  end

  migrate(old: CounterV0)   # old.* are the previous state's fields
    total = old.count
  end
end

struct CounterV0
  count: i64
end

Actor-mode reload is bytecode tier only in v0, since an AOT host cannot load actors yet and reloads function-mode handles there. A migrate covers one previous layout, and the hook is total, with no throws.

16. Comptime (meta)

Compile-time evaluation of ordinary functions, in the style of Zig's comptime.

meta def fib(n: i32) -> i32
  if n < 2i32 then n else fib(n - 1i32) + fib(n - 2i32)
end

MAX_TODOS: i32 = fib(20i32)       # 6765, evaluated at compile time

• Top-level value bindings are always comptime-evaluated; the meta keyword on the RHS is rejected as redundant.
• Function bodies read top-level constants freely: pure defs, impl methods, trait defaults and [local]-only actions alike. The resolved value folds in at runtime lowering. One restriction applies: a top-level binding's initializer cannot call a function whose own body reads a top-level constant, since the constants are still resolving. That is a compile error naming the function.
• meta def declares a function comptime-callable. Comptime has a fuel budget of 10M bytecode steps, and runaway recursion surfaces as a compile error.
• Comptime stores primitive and aggregate values inline, structs, sum variants and lists, constructing and reading them, which lets a .config.hk evaluate to a struct or a list (§21). It evaluates a vetted set of pure intrinsics, the string and List ops, which is enough to fold where-block predicates over comptime-known constructions into compile errors (§9, §15), reading any meta constant the predicate mentions. Effectful and resource intrinsics are not folded and fall back to the runtime.

Reading a config file

CONF: T = config.load(path), from core config, reads a .config.hk at build time. It type-checks and evaluates the file against the stdlib plus the module whose config.load this is, and the file may therefore open that module and build its types: the entry module when the entry has the call, and the sibling when a sibling's meta-const does. It folds the trailing value into a const, with T pinned by the annotation.

It is comptime-only. The path is relative to the entry file and confined to the enclosing project's root: src/main.hk reaches "../app.config.hk" beside the manifest. An absolute, root-escaping or symlink-traversing path is rejected, as is the manifest's own entry. Any value shape bakes to a runtime const, primitive, string, or struct, list or variant aggregate. A closure, bytes, a comptime resource and an in-band ±inf or undefined have no constant form.

config.parse(src) is the runtime half, and it is a parser. It reads the flat declarative subset, NAME = value over a string, a whole number, true or false, or a list of those, with # comments, out of a config the program found while running, and it evaluates nothing: a .config.hk from a peer or from a user's home directory is data. It answers Result<Map<string, ConfigValue>, ConfigError>, where ConfigValue is Str, Int, Bool or Items with the accessors as_string, as_int, as_bool and as_items, and ConfigError has line and reason. An open, a Dep(...) construction, a trailing expression, #{...} interpolation, a fractional or width-suffixed number, and the typed NAME: TYPE = value form are refused and never reinterpreted.

Derives

@derive(Eq, Display, Hash, Encode, Decode) attaches generated impls to a struct or type. On an actor it is refused (H0405) and never ignored.

• Eq compares structurally.
• Display renders TypeName(field=value, …), with sum variants positional, Circle(2) and a bare Nil, recursing through each field.
• Hash hashes structurally. Hash: Eq; derive Eq beside it.
• Encode and Decode generate the static encode!<S: Serializer> and decode!<D: Deserializer>(d, depth) -> Result<Self, DecodeError>, a format-agnostic structural serialization with the built-in BinarySerializer and BinaryDeserializer, on both tiers. Hand-write an impl for another format. A derive gives take_struct!(fields) the exact field count and take_variant!(payload_counts) the ordered payload arities, allowing framed formats to reject a shape whose declared length disagrees with its type. Standard containers and derived decoders reject depth > 128 with TooDeep and pass depth + 1 to children; custom recursive implementations must preserve this guard, and from_bytes seeds depth at 0. hanki cddl <path> emits the derived CBOR shapes as RFC 8610 CDDL. Every schema-reachable hand-written canonical Encode or Decode impl must carry impl-local @cddl("type-expression"); paired impls both carry it and their parsed forms must agree. The string is one RFC 8610 type-expression right-hand side, with no definitions, group entries or trailing text. A reference resolves to a generated project rule, the CDDL prelude, or a generic parameter on the target declaration's emitted CDDL rule. Such parameters bind by rule-head position, and peer parsed forms compare that position independent of source spelling. Invalid, missing or asymmetric metadata fails closed, naming the type and impl and writing no schema; impl bodies are ordinary code and are never inferred. A CBOR integer decoded into a fixed-width target must fit that target; overflow is a decode error and never an implicit modular conversion.

For per-field wire limits, call d.take_string_bounded!(max_bytes) or d.take_bytes_bounded!(max_bytes) before materializing a field. Limits count bytes, including UTF-8, and must be finite and nonnegative; zero permits an empty body. InvalidByteLimit(limit, offset) consumes nothing. ByteLimitExceeded(length, limit, header_start) leaves the cursor after the header and precedes body truncation or UTF-8 checks, without reading, copying, or retaining the body. Existing readers still own their input. Generic and derived Decode apply no automatic per-field byte limits; standard container count and depth guards still apply.

For aggregate accounting or selective decoding, use take_string_header! / take_bytes_header!, inspect the opaque BodyHeader's byte_length, offset, and kind, then call take_string_body!(header), take_bytes_body!(header), or skip_body!(header). Skipping does not materialize the body or validate UTF-8. Headers retain no input and are reader-bound, one-use checkpoints, including empty bodies; advancing through any alias invalidates one. Wrong-kind, foreign, stale, and reused headers return InvalidBodyHeader(current_position). A valid body attempt consumes its header even on truncation. This is a primitive for application policy; it adds no automatic aggregate budget or general nested-value skip. See HANKI.md §17 and hanki doc --find BodyHeader for format-implementor methods and the complete error and cursor contract.

Derives need no @derive. A non-generic struct or sum is synthesised on demand where it is used: Display at #{…}, Eq at ==, Hash at a .hash read, and Encode or Decode at .encode! or Type.decode!, recursing through the fields. A field that cannot carry the trait is a clear compile error, whether it is a resource, an actor, a closure, or a type lacking that impl. That includes a stdlib container field, whose own impl is hand-written and not synthesised: List, Map and Option all carry Display, and only Map implements Eq.

The exact tier encodes losslessly. decimal and rational go through their exact pairs (§3) and int through a class byte plus digits, and the in-band inf, -inf and undefined therefore survive. f32 encodes too. Generic types derive as well, one generic impl per type, through its type-param dicts.

The container types ship a hand-written Display: List<T> renders [e1, e2, e3], empty as [], and Map<K, V> renders {k: v, …}, each element through its own Display.

Three further derives are module-provided and @derive-only, with no on-demand synthesis. @derive(Arbitrary) gives property-test generators. @derive(FromRow), from sqlite, reads each struct field from the same-named column through req_* and opt_*, over scalar and Option<scalar> fields. @derive(FromXml), from xml, reads each struct field from the same-named child element through FromXml, where Option<T> is an optional child and List<T> is repeated children; attributes are read by hand with require_attribute.

There are no AST macros. Where @derive does not cover it, write the impl by hand.

Operators dispatch through traits

== and != always dispatch through a type's Eq impl, hand-written like Map's order-independent equality or synthesised on demand, structurally, when the parts are all Eq. So a == b agrees with a.eq?(b) on both tiers.

A type that cannot carry Eq makes == a compile error naming the part: a resource, an actor, a closure, f64, f32, or an aggregate containing one. The exact tier does carry it, and decimal and rational have Eq, Ord and Hash as int does, which lets a struct holding a price or a ratio derive and key like any other; decimal hashes scale-blind, 1.5 and 1.50 being one value. () has Eq, Hash and Display: a singleton equals itself, and it prints as the two characters (), which renders a derived Display over a unit field as the source wrote it. That is what makes Result<(), E> and Option<()>, which every try_each!-style action returns, comparable and keyable. ActorRef<T> is the one builtin exception and compares by identity. On a generic T, == and != need a T: Eq bound.

A structural == of an aggregate is depth-bounded. A comparison recursing past a fixed cap, on a value nested deeper than the stack guard, traps as a catchable actor death and not as a process abort, identically on all three tiers. Values are always finite, being acyclic (§5). The same bound governs the other structural trait recursions: Ord comparison, Hash, and Display rendering.

<, <=, > and >= dispatch through Ord.cmp, where a < b is a.cmp(b) tested for Less. Numeric operands keep their direct opcode, and bool, string, bytes and any Ord type route through cmp. There is no structural fallback: a non-numeric type with no Ord impl, and a generic T lacking T: Ord, are compile errors.

+ and - on non-numeric operands dispatch through Add and Sub the same way, where a + b is a.add(b) and the impl's type Output is the result type. A heterogeneous impl such as Add<Instant, Duration> -> Instant is what that allows. The numerics keep their opcodes and never reach the traits. impl Add<string> and its siblings are rejected as H0573, since text is joined by interpolation. No impl for the pair is H0572.

17. Tests

def double(x: i32) -> i32
  x + x
end

test "double doubles"
  assert!(double(2i32) == 4i32)
end

• test "name" ... end is a top-level item, like def.

Property tests

A test "name"(x: T, …) with typed parameters is a property test. The runner samples each x from its Arbitrary instance over many seeded cases, purely, with no [random] effect. The body is ordinary assert!, and a failing case shows the offending value, shrunk to a minimal still-failing input.

Arbitrary covers the fixed-width ints, the arbitrary-precision int, bool, f64, bytes, string, decimal, rational, Option, List and Map, and, through @derive(Arbitrary), structs and sums, generic, recursive and mutually recursive ones included; generation is size-bounded and terminates.

The f64 draw is a mixture: whole numbers, readable fractions, IEEE boundary values, and then bit-pattern coverage. A plain bit draw would shrink counterexamples toward subnormals where a reader wants readable values. It is finite by default, and any_f64() adds the NaNs and infinities. f32 has the same mixture through f32.from_bits, encoding whole numbers' IEEE patterns directly, since nothing converts into f32.

@property(cases=N, seed=S) tunes the run with comma-separated options and no trailing comma. Each key may appear at most once. The default is 100 cases, and the seed derives from the name. The shrunk failing input is persisted to .hanki/corpus/<name>.txt and replayed before exploration, which catches a regression immediately; --no-corpus opts out. A parameterless test is an ordinary example.

Fuzz targets

@fuzz test "name"(x: T, …) is a property test whose oracle is "no crash": the body need not assert, and any fault on any input fails it. It takes the same Arbitrary draws, shrinking and corpus as a property.

Only hanki fuzz PATH runs it, and hanki test skips it, as hanki fuzz skips the ordinary tests. --cases N sets the inputs per target, defaulting to 1000, and --time SECONDS bounds by wall clock instead, which --deterministic refuses. The --stdlib, --deterministic, --deny and --max-steps knobs match hanki test. This is the totality defence for a core library. @fuzz and @property are mutually exclusive, and both need typed parameters.

Assertions

assert!(cond) is built in and needs no import. A false condition aborts the test with a file:line:col. Its row is [Crash], as crash!'s is. A test permits it unlisted, an action that asserts declares it, and a pure def or @encapsulated def cannot assert at all.

Where cond is a comparison, ==, !=, <, <=, > or >=, the failure renders both operands structurally, with named fields and variants for structs and sums, on both tiers: assertion failed: total == 42 (left: 40, right: 42).

Running tests

hanki test PATH runs every test block and exits non-zero on any failure. --format=json emits a hanki-test-v1 envelope, {summary, tests:[…]}, which lets an agent read pass and fail and each failure structurally; a compared assert! failure reports the rendered operands as failure.actual and failure.expected.

Test bodies are permissive actions: any effect a callee declares is allowed, and throw is permitted. The permission is type-level only. Under --deny and --allow a test's performed capabilities are still gated, as the restricted-execution section below says.

hanki test --coverage, and hanki run --coverage, writes target/coverage/lcov.info and a per-file terminal summary, covering lines and branches, where a branch is every two-way decision: an if, a match arm, an and or an or. Stdlib coverage needs --stdlib.

hanki test --deterministic, and hanki run --deterministic, fixes the actor interleaving to a seeded schedule: the same source, inputs and seed give byte-identical output. --seed N implies --deterministic and replays a different interleaving, which makes a failing seed the exact reproduction recipe. An all-blocked schedule is a deterministic deadlock and not a hang: hanki run exits 251 with deterministic deadlock on stderr, and hanki test fails that test and continues. An actor parked in a real OS call is not counted among the blocked, since the world can still answer it. Both tiers behave alike, and an AOT binary takes the same replay through HANKI_DETERMINISTIC=1 and HANKI_SEED=N in the environment.

hanki effects PATH prints the program's capability surface: every effect it can perform with the declaring rows, as in io: Logger.log!, main!, which is the set the --allow and --deny gate enforces. Each authority has a root → declaration/handler → concrete provider-row chain with source locations and root-or-dependency origin; dependency steps include the lock-approved effect surface, and rifts name the bound effect and crate while explicitly making no native-analysis claim. --format=json gives the versioned hanki-effects-v2 envelope {schema, entry, capabilities, loads, debugging}. Reachable load! / reload! entries name the host ceiling and mark runtime source unresolved and uninspected; debugging identifies dbg as a non-capability channel. --sys lists the reachable sys.* intrinsics as hanki-effects-sys-v1; and --dbg lists reachable diagnostic writes with locations as hanki-effects-dbg-v1.

Restricted execution

hanki run --deny net,fs and --allow io, both also on hanki test, refuse to run a program that can perform an effect outside the allowance; this is a Hanki-semantic gate, with no OS isolation against the trusted runtime, native rifts, inherited descriptors or allowed subprocesses. It is a static check over the effect rows before the program starts, exiting 1 with capability denied: on stderr, and it covers spawned-actor handlers.

Add --receipt PATH to a restricted hanki run or hanki test to write a canonical hanki-execution-receipt-v1 JSON sidecar. It requires an --allow or --deny policy and records the toolchain, content identities, requested and enforced policy, provider and rift identities, ordered authority-boundary events, and the terminal outcome. It records no environment values, raw arguments, current directory, hostname, time, duration or captured output, and does not change stdout or stderr. The write is atomic in PATH's directory. This receipt proves what the Hanki boundary observed; it adds no OS containment. HANKI.md §23 defines the complete field and identity contract.

Under hanki test and hanki fuzz it also covers what test blocks perform. A test has no declared row, and its capabilities are collected from the actions it calls: a test that writes is refused under --deny fs_write, and a read-only test runs.

The capabilities are io, net, fs, db, process, time, env and random, plus any user effect. fs is an alias for fs_read and fs_write. [db] is the distinct database-seam atom. sqlite charges [db] and not the general [fs] seam, and --allow db --deny fs therefore reaches a database and no fs.read! or fs.write!, and a :memory: database charges [db] with no file at all. --deny wins over --allow.

The gate is re-enforced at every module.load! and reload!, and a widening load is refused with a catchable ModuleLoadError, which leaves loaded code unable to escape it. With no flags at all, a module-loading program defaults its load allowance to its own declared surface, and a loaded module can then do only what the host advertised. To grant a plugin net, the host declares net on the trait method it calls; an explicit --allow overrides this. Both tiers behave alike: an AOT binary has that baseline baked in, and HANKI_ALLOW and HANKI_DENY in the environment, in the HANKI_DETERMINISTIC shape, narrow it and never widen it.

--max-steps N exits 250 once N bytecode steps across all actors are spent, never more than N, though concurrent actors may trip marginally early. --max-bytes N bounds the total bytes allocated across the run, which is no live-heap ceiling: freeing credits nothing back. Both bound how much a run may do, on the bytecode tier, and both are also on hanki test. They bound just-written Hanki code without creating an OS boundary.

with_budget(bytes, steps) BODY end is the scoped and catchable counterpart in the language. It carves a sub-quota from the parent's remaining step and byte budgets: a child can never exceed the parent, and its spend debits the parent. It evaluates to Result<T, sys.BudgetExceeded>: Ok(v), or Err(Exceeded) on overrun in place of faulting the run. A host therefore recovers from an over-budget nested computation, an embedded interpreter or an untrusted predicate. It nests, and a normal throw still propagates through it. It is bytecode tier only, and hanki build refuses to lower it, which fails a self-metering program at build time in place of shipping it unbounded.

Doctests

A fenced block inside a doc comment, a # run directly above an item, runs as a synthesized test, which tests the examples against the code.

# Doubles its argument.
#
# ```
# double(2i32) => 4i32
# ```
def double(x: i32) -> i32
  x + x
end

• EXPR => VALUE becomes assert!((EXPR) == (VALUE)). Any other line, a setup binding for instance, runs in order. One fence is one test with one shared scope. A line carrying no assertion still runs, which catches signature drift.
• A bare fence and a hanki fence execute. A text fence, or any other tag, is an inert sample. A blank line or a non-item line below detaches the block. Methods inside an impl or a type` can be documented too.
• Doctests run under hanki test as test blocks do, with the stdlib examples under --stdlib, and a failure shows as doc example (line N).

Reading documentation

Doc comments attach to their item, and hanki doc FILE.hk renders the file's documentation as Markdown: a signature, the prose and the examples, per symbol. Add a symbol to narrow it, hanki doc FILE.hk map or hanki doc FILE.hk Option.map.

A bare name matching no file but naming a baked stdlib module renders that module, hanki doc list or hanki doc list map, which is how to recall a stdlib surface with no file to point at. An unambiguous public type name resolves to the module that documents it, as in hanki doc UnixStream. A shared type name reports the qualified candidates and requires the module form, such as hanki doc aead Key. A bare name matching no module or type is looked up among the project's declared dependencies: hanki doc tui reads the package use tui binds without your knowing where its source sits.

A leading comment split from the first item by a blank line documents the module. hanki doc DIR renders a whole project, every reachable module in topological order with dependencies first, as Markdown or as a JSON array of per-file envelopes.

hanki doc --check FILE lints, exiting non-zero and listing every exported callable symbol with no runnable example. The escape for a symbol an EXPR => VALUE cannot illustrate, a side-effecting primitive, is a # @no-doctest: <reason> line in its doc comment. A _-prefixed name and a program's entry point, a top-level main!, are outside the gate and need no such line. A compiler test applies this bar to every stdlib symbol, in core and extra alike.

In the REPL, help(TARGET) and :doc TARGET render the same documentation in session: help(list) for a module, and help([1,2].map), which resolves the receiver's type first. A surface is therefore recalled without leaving the prompt.

hanki doc FILE --format=json emits the surface as data, one hanki-doc-v1 envelope holding {module_doc, items: [{name, qualified, kind, signature, effects, doc, has_doctest}]}, which lets an agent learn a module's signatures in one structured read with no grep over the source. The symbol filter narrows items the same way.

18. Project layout

A Hanki project has a manifest (hanki.config.hk) plus one or more .hk source modules.

# hanki.config.hk
name        = "todo"
version     = "0.1.0"
programs    = ["src/main.hk"]
description = "A simple todo CLI"

• The manifest is itself a Hanki file. A bare IDENT = EXPR is sugar for a typed binding with inference, and the typed form IDENT: T = EXPR is also allowed. A binding that is neither a recognised field (name, version, programs, exports, description, hanki, deps, exclude, rifts) nor a declared dep's source is an error.

Rifts

rifts = [Rift(effect_name = "audio.Audio", path = "native/audio", deterministic = false)], with open pkg, binds an effect to a Rust crate in the application's own tree. This is a rift into native code, and only the root manifest may declare one; a dependency carrying one is refused.

The binding is checked before any cargo runs. The effect exists by that module-qualified name, there is one binding per effect, the path is a crate directory under the project, every name has a Rust spelling of its own, and some program references it. A bound effect needs no provide.

The op signatures stay in the representable subset: fixed-width numbers, bool, string, bytes, and Option, Result, List and Pair of those, plus non-generic structs and sums. Outside it are int, decimal, rational, Map (cross it as a List<Pair<K, V>>), resources, closures, futures and actor refs.

hanki rift generate writes the api and shim crates the author implements against, under a gitignored .hanki/rifts/. run and test build and load them, build links them in along with whatever the crate's build.rs asks for, and in both paths an artifact built against another declaration is refused. Rift state is per actor, opened on that actor's first call and dropped at its death. A panicking op is an actor death carrying the rift, the op and the message, and never an abort, while a declared failure remains an ordinary Result (HANKI.md §21).

Roots and the package boundary

exports is an enforced boundary, and a binding is a handle on the whole package. use <alias> reaches <alias>.hk there, and use <alias>.<module> reaches any other exported module, by stem, wherever the file sits under the package. A module outside the list is refused at the importing line, and the message says what the package does export. <alias>.hk need not exist: a package may export client.hk and model.hk and nothing named for the binding. The same applies to path deps.

programs and exports are the roots, and entry is retired. Both are a List<string> of project-relative module paths, confined under the root and required to name real files. A package that is run declares programs, a library declares exports, one that is both declares both, and at least one is required: a manifest naming neither is rejected with both named. entry is not accepted as an alias.

hanki build on a package emits one binary per declared program, in manifest order, and picks nothing. hanki run has to pick, and a package declaring several is therefore refused with them named. --program <name>, the file stem, says which, and narrows build to one as well. Only programs are offered, and exports are not. The binary takes the manifest name for a sole program; with several, each takes its own stem, dashes included: entsoe-fetch.hk builds out/entsoe-fetch.

Reachability is rooted at every declared root, which checks a package's second program and runs its tests with no exclusion needed. Each root is checked in its own workspace, and --coverage measures one program and refuses a package declaring several.

exclude names what is meant to be unreachable. hanki test and hanki check report every .hk file no declared root can reach: a module with no caller yet is a suite that does not run and says nothing. A project with fixtures, testdata, a vendored subpackage or a path dep under its own root says so once: exclude = ["testdata", "vendor"].

An entry is a path relative to the project root, either a directory, covering everything beneath it, or a single file, matched whole-component: "testdata" covers testdata/nested/a.hk and never testdatax/. An excluded file is never opened. The entries are plain paths and no globs, which leaves the manifest with no second matcher beside glob.

The single-file form is for a library another project consumes: imports resolve within their own project, and the file must therefore sit in one project and be unreachable there. Where it has tests, run them explicitly: an excluded module leaves the package's own hanki test. hanki doc --check skips excluded files, and hanki fmt does not.

Dependencies, frozen for 1.0

open pkg, then deps = [Dep(source, version)], a List<Dep> because Hanki has no map literal, plus one hanki = "^1.4" toolchain-version constraint that core and extra share.

A dep source is a contrib flat name, or a short name with a matching top-level binding. lexer = "path:../front" makes it a local path dep on a sibling project directory: the constraint is checked against that project's version and use lexer binds <dir>/lexer.hk. A target may sit beside or inside the graph root, but may not equal or enclose it, where its pin would recursively include the consumer's generated lock. Ordinary resolution reads the sibling live and freely refreshes its path:<dir> lock entry; --frozen instead requires that baseline and rejects version or source-tree drift. Any other binding is a universe git URL, http = "git.sr.ht/~user/http", which is also the use http alias (§17). The binding's presence and shape pick the tier, and nothing falls through. A constraint is ^1.2, ~1.2, >=1.2,<2, an exact 1.2.0, or * for any.

The generated text lock hanki.lock.config.hk records locked = [Locked(source, version, hash, api, effects)] and content-pins every dependency. Re-resolving the same third-party version to a new commit hash, from a moved upstream tag, fails resolution by default, and the message says whether the api digest and the effect surface moved with it. The lock also records the approved effect surface, and a grown third-party surface fails resolution until you approve it: edit effects in the review diff, or run hanki resolve --accept-effects '<source>=<eff>'.

The resolver has landed for all three dep tiers, is transitive, and is wired into build, run, check, test and resolve. Universe deps are fetched and imported, and their own manifests are then resolved recursively. There is one version per source graph-wide, the SemVer-max over the intersection of every requirer's constraint; an empty intersection or a dependency cycle is a hard error naming the requirers. Each dep's own use binds its own manifest's aliases and never the consumer's.

A contrib dep resolves from the toolchain's seeded contrib/<name>/ source, one shipped version per package, pinned as contrib:<name>@<version> with a deterministic sha256: tree hash. Locked.hash is a prefixed string, git: for a commit and sha256: for a tree, while Locked.api beside it remains fnv1a:. A path dep is pinned with the same package-tree hash; its root out/ and .git, .hg and .svn control entries at any depth are excluded. Build and checkout history cannot move the baseline. Only a workspace-local package may declare one. Normal resolution remains live and refreshes path pins without the third-party integrity or effect-growth refusal. A single-file entry is governed by a same-directory manifest where one exists. The full closure locks flat, including path deps. A path-only project has a lockfile. hanki build --frozen resolves offline from the lockfile and the warm cache, re-hashing seeded contrib trees, warm universe cache slots and live path trees and fetching nothing, which is what a hermetic CI build wants.

Four CLI verbs have landed. hanki resolve writes a standalone lock, and --frozen verifies it offline. hanki add <source> takes contrib by default, with --git and --path bindings picking the tier; it refuses a source it cannot find, writes ^major.minor of the version that source declares, and re-parses, which stops a bad edit from landing. hanki list [contrib] prints the curated packages the toolchain ships, name, version and description, one per line, with no network. hanki publish derives and validates the descriptor locally. The hosted registry upload remains planned tooling on this frozen contract (docs/design/package-manifest-schema.md).

• A .config.hk file is declarative, and strict mode rejects actor, def name!, test and provide. A config value may still invoke user-declared effect ops, where the host injects each op's behaviour and the unprovided effects the value references are its capability interface. A built-in ambient effect in a config value is H0614: io, fs, net, db, process, time, env, throws and Crash are all refused, and OS authority is therefore denied at the boundary.
• hanki check . type-checks (no artefact); hanki build . compiles to a native binary via LLVM AOT; hanki run . executes main! on the bytecode interpreter. Development toolchains use LLVM O1; release toolchains use O2, with IR verification in both. See HANKI.md §22 for policy selection, timings and runtime archives.

The build tool is the first capability host

hanki check, build, run and test inject a vcs effect, stdlib extra/vcs.hk, whose git-backed sha() and describe() let a manifest compute a field at build time: open vcs, then version = describe(), or use vcs and vcs.Vcs.describe(). hanki fmt evaluates nothing and remains pure.

In a git checkout the value resolves fresh from git. For a git-less source tarball, hanki build --refresh-manifest records the resolved values to a git-tracked hanki.vcs.lock.config.hk that a later git-less build reads in place of failing. With neither git nor a cached value, the op is an unsatisfied capability surfaced by name, and never a silent default.

Diagnostics for agents

A failed hanki check prints error[H####], a stable code, on the file:line:col: line, then the offending source line and a caret under the span. The caret is presentation only, and --format=json's rendered field still has the one line.

A line beginning error: internal compiler error says the toolchain panicked and says nothing about your code. It exits 70 and is worth reporting with the source.

hanki explain H#### gives the explanation and a fix recipe. hanki check --format=json emits a hanki-diag-v1 envelope, {code, severity, span, message, rendered, fixes}. hanki check --fix applies the machine-applicable fixes in place with comments intact, propagating a missing [net] up the call chain for instance. The loop is run, explain, fix, re-run.

• hanki query FILE --at LINE:COL answers what a position is: the signature, effect row included, or the name: type under the cursor, plus its definition site. It answers a semantic question with no file read in. --format=json gives a hanki-query-v1 envelope.
• hanki api-diff FILE [--against REF], defaulting to HEAD, classifies every public-API change as breaking, compatible or informational. An added effect, a T becoming a Result<T, E> and an added variant are breaking; a removed effect is compatible; a rename is informational. It exits 1 on any breaking finding. Run it before landing a change to a module others consume. --format=json gives a hanki-apidiff-v1 envelope. The native resource spellings from §4 compare as one type in signatures and impl heads; user types imported with open remain distinct. Public inherent methods, associated functions and properties on builtin and imported types use the callable rules; a prop/def change is breaking. Defaulted trait arguments expand in the declaring module's scope.
• hanki scoreboard PATH prints the package's un-gameable facts: the compiler-verified Guarantees (Pure Hanki, Crash-free, Effect bound, Throw surface, Docs complete) and the measured Metrics (the purity breakout pure def · @encapsulated · actions, the public-API size, the module, line and test counts, and an opt-in --coverage line percentage). It is a board of independent figures and no ranked score. --format=json gives a hanki-scoreboard-v1 envelope.
• main! has the signature def main!(args: List<string>) -> () [io], with whatever other effects you need. Returning a lowercase int makes the value the exit code. Argv is whatever trails an explicit path, as in hanki run app.hk a b, which makes a .hk file with a #!/usr/bin/env -S hanki run shebang an ordinary executable script. Use hanki run app.hk -- --flag for an argument starting with a hyphen.

19. Stdlib essentials

Auto-injected modules; no on-disk file needed.

Two baked tiers

core is the locked, opened-by-convention surface: option, list, str, display, eq?, hash, actor, the numeric tower, plus sys, the native seam, and module. extra has the evolving capability and utility modules and is import-gated, in scope only after a file uses or opens them. Core may not depend on extra, and user code uses either.

Seams and rifts are enforced. A seam is core's @intrinsic boundary and remains core-only: every @intrinsic sits in core, where the sys module owns the OS primitives, and the extra capabilities are pure-Hanki faces that declare an effect and delegate to sys. A non-core @intrinsic is a check error.

Two further tiers are never baked: the curated contrib, bundled with the toolchain as seeded source and resolved by the package manager, and the decentralized universe.

No package may add native code. The one thing outside core that can is an application-root rift: the program's own repository answers an effect declaration's ops with a Rust crate, bound by its own manifest and never by a resolved package at any depth, and a dependency that tries fails resolution. The surface it implements is a checked effect, values cross as bytes with message-send semantics, state is per actor, a panic is an actor death, and the effect it answers is a capability atom --allow names.

Compiler reflection

Core compiler is experimental. It is the seam the off-path dev tools are written through, fmt, doc, lint, effects and api-diff among them: it runs the in-process front end over a source string and hands back ordinary Hanki values. parse gives the shallow item headers and type_decls the deep structured declarations. diagnostics(src, module_name) gives what hanki check reports, where module_name names the stdlib module src is, which stands its shipped copy aside; pass "" for ordinary source. Beside them are effect_surface, doc_items, imports, stdlib_modules, project_modules!, diag_codes and the bundled-doc accessors. project_modules! includes the manifest's evaluated package name beside its entries, modules and unresolved imports. Relative and absolute spellings of a file path select the same entry and modules. A delegated tool never reparses a manifest as flat runtime config. project_diagnostics!(path, src) asks the same check inside the package, with src standing in for the file, which is what a two-revision diff needs: a module checked alone loses its siblings and the manifest's exports classification with them.

Record shapes are unstable until the tool ports settle them. api_version() -> int is the revision to check, and toolchain_version() -> string says which hanki wrote a generated file. It works on both tiers: an AOT build that calls one links the embedded front end, as load! does, and reflected values are therefore byte-identical across tiers. Full record shapes are in HANKI.md, and hanki doc compiler prints the live signatures.

The sibling core manifest module does the effectful artifact half: manifest.read!(path) decodes a built .so's .hanki_manifest section, the data behind hanki inspect. Its v7 required_host_symbols field is the sorted, deduplicated Hanki ABI import set the module needs from its host. A v7 payload must encode the field even when the set is empty; only v5/v6 artifacts, which predate it, default to an empty list. Native .sos leave those imports undefined, owning their Hanki code and rifts but resolving the one process runtime from an exact allowlist of symbols owned by the embedding executable's runtime archive. Host rift shims and user functions named hanki_* are never in that export set. Before dlopen, the native loader resolves every listed symbol from the live host; a miss raises module.ModuleLoadError::MissingHostExports(path, required, missing), listing the whole requirement and missing sets without running a module constructor. Every native AOT image has its own address-valued identity. Actor descriptors, shapes, throw types, positional actor-method names, the SendFailed tag and the actor_died method index register under it. Generated spawn, send, await, throw, module-loader and rendering calls carry the caller image, while a death cast resolves the supervisor image. Cast, delayed, blocking and async sends translate the caller-local method id through its stable name into the target image's local id; two loaded .sos can therefore intern methods differently and reuse every numeric id without replacing or misreading each other's metadata or the host's. The capability baseline remains executable-owned policy: a shared module never registers one. The native loader pins one mapping reference for every successfully loaded image until process exit: even an actor- and rift-free module can leave a closure trampoline, captured environment or layout descriptor in a host-owned resource such as a SQLite connection; later handles balance their own references and unload! still invalidates the logical handle. A foreign embedder must do the same or prove every image-owned callback and value retired before dlclose.

Extra modules

Each is import-gated and needs a use before its qualified name resolves. Terminal and files: io, fs, path, glob, terminal. Processes and environment: process, sh, env, flags, log. Network: net, http, url, tls. Time: time, datetime. Data formats: json, xml, csv, text, hex, render_pretty. Crypto and identity: sha2, aead, uuid, random. Parsing: regex, peg, parsecheck. Storage: sqlite. Actors: supervisor. The OS-capability seam (net/process included) runs on both tiers. json.parse_strict and json.parse_bytes_strict reject repeated decoded object keys with DuplicateKey(offset), containing the second key's opening-quote byte offset and no key text. json.parse and json.parse_bytes retain the final value for a repeated key.

fs.write_new! and fs.write_bytes_new! atomically create an absent file on both tiers, returning Result<(), sys.FsFailure> [fs_write]. Concurrent creators have one winner and AlreadyExists losers; existing final symlinks are refused, including dangling links. Creation precedes writing: a later error can leave an empty or partial new file. Directory listings describe symlinks themselves, including dangling links; path metadata follows them. For field units, raw Unix mode bits and metadata-failure fallbacks, use hanki doc sys DirEntry. Symbolic links have fs.symlink!, fs.read_link! and fs.is_symlink!; creation is Unix-only, while reading and detection use host operations on both tiers.

Terminal input is event-driven on Unix. sys.stdin_read! and terminal.read_key! append a dimensionless Resized result for SIGWINCH; the sole terminal reader queries terminal.size! once after it wakes. A burst therefore coalesces without idle polling. A negative timeout remains idle-quiet while still waking on input, actor shutdown, or resize. sys.stdin_read! follows the native-call deadline rule in HANKI.md §6; a finite timeout is a wall-clock bound across retries. Child-pipe reads share sys.StdinRead but never produce Resized.

terminal.read_key! bounds unfinished input and scans it in amortized linear time. KeyRead adds TooLarge(int) and Truncated(bytes): an oversized event enters a persistent constant-memory discard state across timeouts and resize wakes, drains to its syntactic boundary or EOF, then returns TooLarge(limit) carrying the enforced cap; EOF with bounded pending bytes returns Truncated(pending), while bare Eof means none were pending. The discard state never exposes a paste tail as later key events.

Names, signatures and doc prose are one command away. A listing here would go stale; the command cannot.

hanki doc                    # every baked module, one line each, grouped by tier
hanki doc --find TERM        # search names AND doc prose across all of them,
                             # and the CLI verbs; a miss is an authoritative
                             # "no stdlib symbol and no verb". Patterns with no
                             # symbol, the Delayer above, are not searched, and
                             # every answer names the tiers it did not cover
hanki doc <module> [SYMBOL]  # one module, or one member's signature and prose

The capability faces answer specific error sums, where a weaker bool or Option would lose the reason: fs a sys.FsFailure with the failing path, process a sys.ProcessResult, net and http their own. Each declares its effect, from the capabilities above, gated by --allow and --deny.

Traps a listing does not show

• string has no concat; text is assembled by interpolation, by join, or with a StringBuilder. The surface is length / slice / slice_from / find / split (non-overlapping pieces; an empty separator returns [self]) / split_whitespace (the words: splits on runs of the same ASCII whitespace set trim strips, empty pieces already dropped) / lines (LF ends a line; strips CR only before LF, omits one trailing empty fragment, and returns no lines for empty input) / repeat / pad_start / pad_end / starts_with? / ends_with? / strip_prefix / strip_suffix (the removing forms of those two, None when it does not match) / contains? / empty? / join / trim (+ trim_start / trim_end; space, tab, LF and CR only) / replace / to_ascii_uppercase / to_ascii_lowercase (ASCII-only fold) / eq_ignore_ascii_case? / to_bytes. All offsets are UTF-8 byte offsets, and a mid-codepoint offset rounds down to a character boundary. The whole index surface, lengths, offsets, indices and counts, is the scripting-default int, which lets unsuffixed literals and counters compose with no conversions. Out of range remains total: a slice clamps and a read answers None.
• list is immutable and persistent: xs: List<i32> = List.empty() fixes the element type without inline type arguments. List.repeat(x, n) gives n copies. Accumulate with append; no ListBuilder is needed. A chain of n appends from empty takes O(n) structural work on both tiers, including ownership, byte-budget accounting and final release. Earlier versions may remain live, including old = xs followed by an append and a read of old.length. Receiver uniqueness and payload representation impose no restriction. Indexed reads, callbacks, element construction and actor transfer have separate costs. List height remains logarithmic in its current length after slicing; unchanged interior subtrees are shared. The full reference §17 gives existing-list, independently forked-chain and indexed-combinator bounds; hanki doc --find list gives operation details.
• option's or_crash!(msg) is the one partial method. Its row has [Crash], which is viral and bars every pure def.
• Every callback-taking method on option and result has an effect-polymorphic ! twin (§13), and an effectful step needs no match.
• A number's parse is on the FromString trait. A concrete call such as i32.parse(s) needs no import because core impls are ambient. Generic code that names <T: FromString> opens from_string to bring the trait name into scope.
• io.read_line!() answers Line(string) | Eof: end of input is a value, never an error.

20. Common idioms

Read-loop on stdin until EOF:

open io

def main!(args: List<string>) -> () [io]
  loop    print!("> ")
    match read_line!()
      Eof        -> break
      Line(line) -> print!("got: #{line}\n")
    end
  end
end

Parse-then-act with Option / sum match (open option at the top of the file so Some/None work bare; see §14):

use io

def handle_positive!(n: i32) -> () [io]
  io.print!("positive: #{n}\n")
end

def handle_other!(n: i32) -> () [io]
  io.print!("other: #{n}\n")
end

def parse_then_act!(line: string) -> () [io]
  match i32.parse(line)
    Ok(n) if n > 0i32 -> handle_positive!(n)
    Ok(n)             -> handle_other!(n)
    Err(e)            -> io.print!("#{e.reason}\n")
  end
end

Struct + inherent method:

struct Point
  x: i32
  y: i32
end

impl Point
  def origin() -> Point
    Point(x=0i32, y=0i32)
  end

  def shifted(self, dx: i32, dy: i32) -> Point
    Point(x=self.x + dx, y=self.y + dy)
  end
end

def demo() -> ()
  p = Point.origin().shifted(3i32, 4i32)
  ()
end

Actor + blocking send:

use io

actor Counter
  state n: i32 = 0
  on bump() -> i32
    n += 1
    n
  end
end

def main!(args: List<string>) -> () [io, throws actor.SendFailed]
  c = spawn Counter
  v = c.bump()
  io.print!("first: #{v}\n")
end

21. Anti-patterns

Habits carried in from other languages, and what Hanki asks for instead.

22. Working in Hanki as an agent

The toolchain is one loop. The habits, in working order:

1. Sketch with typed holes. Write the program's shape and leave every unwritten expression as ???. hanki check reports each hole's expected type and permitted effects as hole[H0250], and the compiler therefore dictates the gaps with no placeholder value written.
2. Query semantics in place of reading source into context. hanki doc FILE --format=json is a module's API surface as data: signatures, effect rows, doctest presence. hanki query FILE --at LINE:COL answers what a position is. Grep is the fallback.
3. Check, explain, fix. A failed hanki check prints error[H####], hanki explain H#### gives the recipe, and hanki check . --fix applies the machine-applicable fixes, propagating a missing effect up the whole call chain. --format=json gives the structured envelope. The loop is run, explain, fix, re-run.
4. Test with structure, and reach for properties. hanki test --format=json gives per-test results with the failure operands. A claim that should hold for all inputs is a property test: test "name"(x: i32) samples through Arbitrary, and a failing case hands you the input. For actor code, --deterministic makes runs byte-identical, and a failing --seed N is the exact reproduction.
5. Run just-written code under least privilege. hanki effects . prints every effect the program can perform, the declaring rows included. hanki run . --allow <that set>, or --deny …, then refuses anything outside it, statically and before execution.
6. Classify the contract before landing. hanki api-diff FILE diffs the module's public API against HEAD and exits 1 on any breaking finding: an added effect is breaking, an added variant is breaking, a removed effect is compatible. Done means the tests pass and the surface change is intentional.
7. Format immediately after writing, and anchor only on canonical text. hanki fmt FILE rewrites a file into its one canonical form, and hanki fmt --check FILE exits non-zero when the file is not already in it. Run the check before composing a mechanical edit anchored on a file's text: the anchor can miss after a later format, and a missed anchor that no-ops with no error is how a check you wrote stops existing. Beyond whitespace, fmt normalizes the following.
   • Effect rows canonicalize. The bare tags sort alphabetically, case-insensitively so that a capitalized user effect does not jump the built-ins, then Crash, then each throws E, then the effect variable, and the fs_read and fs_write pair refolds to the [fs] alias. [io, fs_read, fs_write] therefore prints as [fs, io], and [e, net] as [net, e]. This rewrites what the row says, where the rest of fmt rewrites layout, and a grep for fs_write, or a tool anchoring on the row it wrote, then finds nothing.
   • if retains the form it was written in. The block form, if c … end, and the inline form, if c then a else b with one expression per branch, no end and then selecting it, are never folded into each other; a dangling else binds to the nearest if. An inline if that is an operator's operand is parenthesised, as a closure is.
   • A list literal past the line budget breaks to one element per line, with no trailing comma, which does not parse. One that fits remains on a single line.
   • Imports: the use section first, then open, one blank line between the sections and none within, each sorted by path.
   • Items are separated by one blank line; runs of blanks collapse.
   • Single-line strings re-escape canonically (a raw # becomes \#); multi-line strings are preserved verbatim.
   • Spacing in signatures, calls, and around operators is canonicalized (def f(a: i32, b: i32) -> i32).
   • Method-chain breaks are kept, never introduced; a kept break's indent is fixed to two spaces under the receiver.
   • A guard binding (§8) remains on one line whatever its width. Only a comment between the -> and the else body breaks it, onto its own indented line, the way a match arm breaks for the same reason.
   • A literal in a pattern loses its numeric suffix: 3i32 -> … prints as 3 -> …, and one in an expression retains it. A pattern is matched against a scrutinee whose type is already fixed, and the suffix there is decoration and no claim.
   • Comments re-attach at the item or statement they precede. One trailing code remains trailing, and one on its own line remains standalone.

Every envelope is versioned, hanki-diag-v1, hanki-test-v1, hanki-query-v1, hanki-doc-v1, hanki-effects-v2 and hanki-apidiff-v1: one JSON object on stdout, with stable keys, safe to parse.

23. Where to go next

• Comprehensive language spec + stdlib reference: https://hanki-lang.org/HANKI.md (shipped alongside this card)
• hanki check . to type-check; hanki build . to compile a native binary; hanki run . to execute; hanki test PATH to run tests.
• When unsure, read the project's existing modules before inventing a pattern. Hanki is small enough that grepping for def NAME, actor NAME or type NAME usually finds the answer.