Toka Syntax Guide

This guide describes the public surface syntax of the current Toka implementation. It is intentionally conservative: examples here are limited to forms used by the compiler, standard library, or test suite. Short fragments may omit surrounding declarations, but the syntax shown is meant to match current Toka.

For a short project overview, see the repository README. For historical notes and internal pitfalls, see syntax_notes_zh.md.

1. Core Model

Toka separates two layers that many systems languages collapse into one notation:

Layer	Meaning	Examples
Payload / Soul	The object content being read, written, passed, or matched	x, x.field, x = value
Handle / Representation	The way an object is reached, owned, borrowed, shared, or rebound	&x, *x, ^x, ~x, *x = *y

Plain names operate on payload. Hats operate on handle identity. This is the key rule behind Toka's pointer and resource syntax.

auto ^p = new i32(100)
auto value = 10
auto &r = &value

In the example above, p is the payload view of a unique-owned object, ^p names the unique owning handle, and &value creates a borrow handle.

2. Files, Imports, And Entry Point

Toka source files use .tk.

Module-location paths follow filesystem-oriented spelling. Path segments may use kebab-case when they refer to directories or .tk file names:

import std/io::println
import core/types::{usize, Addr}
import ./third-party/http-client as http_client

fn main() -> i32 {
    println("hello")
    return 0
}

Hyphens are path-only. Any name newly created inside .tk source and entering Toka's semantic namespace must be a normal identifier: variables, functions, types, fields, import aliases, import item aliases, and selectable namespaces do not use kebab-case. Therefore as http-client, http-client::send(), and (package-name = "...") are invalid. In expression syntax, binary - is an operator and must be surrounded by spaces, as in a - b.

The entry point is main. Toka 1.0 accepts i32 or an omitted Unit result, including fn main() -> async { ... } for async main. A Result-returning helper must be handled at this boundary; main -> Result<...> is reserved for a future termination protocol.

Comments:

// line comment
/* block comment */

3. Bindings, Mutability, And Nullability

Local variables are declared with auto.

auto x = 1
auto y = 10:i64

An auto binding always has an initializer and never has a left-side type annotation. Use expression: Type to ascribe the initializer's type, or expression as Type for an explicit conversion.

An integer literal adopts the unique integer type supplied by its context, including a function or method parameter, assignment target, return type, or the typed operand of a comparison. Write an explicit type only when no unique context exists or when the width is itself part of the intended boundary. A literal that does not fit the selected type is rejected with E04598; Toka does not silently truncate contextual literals.

# on a binding grants mutation authority for that binding.

auto count# = 0
count = count + 1

# appears in declarations, explicit mutable method calls, and mutable call arguments (such as push(values#, 7)). Ordinary reads and assignments use the bare name.

counter#.inc()
increment(counter#)
counter = 3

Absence domains

Safe nullable payloads and owning handles have been permanently removed: T? reports E0484, nul ^T / nul ~T report E0485, none reports E0486, and nullable postfix/assertion syntax reports E0487. The parser recognizes these spellings only to provide migration diagnostics; they are not language types or values and have no Sema or CodeGen representation.

Toka distinguishes operation outcomes, explicit zero-or-one storage, and physical zero addresses:

Domain	Surface form	Empty state	Meaning
Raw may-zero address	nul *T	null	An unsafe/FFI address may physically be zero
Raw non-zero address	*T	none	The raw address is non-zero, although dereference still requires unsafe
Operation miss	T | miss	miss	An operation did not produce a T
General optional value	Option<T>	Option<T>::None	A stored value explicitly has zero-or-one cardinality

For example:

auto nul *ptr = null:nul *i32
auto value = lookup(key) // declared T | miss
auto result = Option<i32>::None:Option<i32>

Plain *T cannot be constructed from, assigned from, returned from, or compared with null. *T widens to nul *T; the reverse direction requires the explicit checked pointer.unwrap(). nul is therefore a raw-pointer physical property, not a general nullable type constructor. Borrow, unique, and shared handles always designate valid objects in Safe Toka.

When a persistent absence reason matters, define it nominally and keep the operation miss separate:

shape StoredValue (
    Empty = 1 |
    Present(string) = 2
)

fn lookup(key: str) -> StoredValue | miss

Move invalidation is not another Option result. A moved-from binding is tracked by PAL and cannot be observed by matching a public Moved variant; the standard Option<T> result domain consists of Some(T) and None.

Raw may-zero pointers use comparison, guard, or .unwrap() explicitly. Postfix ! applies only to Result and Option, as specified in the result-propagation section. T | miss is handled by return construction and matching; none of these mechanisms implicitly flatten another domain. The separate .await? spelling remains an async cancellation-outcome operator, not Safe nullable syntax.

An implementation may reuse a niche or another compact layout for more than one absence domain. Layout equality does not create type identity, an implicit conversion, or a stable cross-language ABI guarantee.

T | miss operation outcomes

T | miss is an operation-outcome type distinct from Option<T> and raw may-zero pointers. It is not a general union and is not an alias for Option<T>:

fn find_value(hit: bool) -> i32 | miss {
    if hit { return 42:i32 }
    return miss
}

It has exactly two special construction rules:

1. A new hit/miss state is introduced only at a return boundary of a function declared with -> T | miss: return value forms a hit and return miss forms a miss. An existing outcome follows ordinary argument, field, assignment, cede, and forwarding rules.
2. T | miss has no default value. A program may create a Never place with uninit:(T | miss), or initialize it from an expression returning the same outcome type. uninit itself forms neither state.

auto result = uninit:(i32 | miss)
init result = find_value(true)

match cede result {
    auto value => use(value)
    miss => handle_miss()
}

miss is a contextual keyword in these return and pattern positions, not an ordinary value or public constructor. There is no implicit conversion between T | miss and Option<T>; existing Option<T> semantics remain unchanged.

4. Hats And Handles

Toka uses hats to expose handle identity:

Hat	Role
&	Borrow / reference handle
*	Raw pointer handle
^	Unique owning handle
~	Shared owning handle

Examples:

auto value = 10
auto &r = &value
auto ^owned = new i32(5)

Payload assignment and handle rebinding are different operations:

p = value      // write payload
*p = *q        // rebind a raw pointer handle

For a handle binding that itself may be rebound, place # after the hat:

shape Node(val: i32)

auto ^#head = new Node(val = 0)
auto ^replacement = new Node(val = 1)
^head = ^replacement

A selected unique handle has affine value semantics. When ^source is used to initialize, assign, or return a unique value, that value use is intrinsically a move and the cede keyword is omitted:

auto ^next = ^head       // direct unique move; head is invalidated
return ^next             // unique value return; next is invalidated

This rule belongs to the value context, not to the ^source expression by itself. Passing ^source to an ordinary ^param is the normal logical handle capture and does not move it. A parameter declared cede ^param remains a consumption contract: the resolved formal moves an admitted bare or explicit-cede source, while the callee may discharge the obligation by a direct unique move such as auto ^owned = ^param or return ^param.

The position of # is semantic. ^#p, *#p, ~#p, and &#p mark the handle identity as rebindable. ^p#, *p#, ~p#, and &p# keep # on the binding name / payload side; they do not grant handle rebinding authority. When both permissions are needed, write both positions, such as ^#p#.

$ is the explicit read-only / blocked counterpart. Because ordinary payloads are read-only by default, $ is usually omitted and is rejected on ordinary locals and parameters as redundant. Its purpose is to block inheritance in places where an outer writable path would otherwise grant permission: field$ remains read-only even through obj#, and hatted forms such as ^$p or *$p keep the handle identity non-rebindable even through a writable parent.

Permission inheritance is layer-local. Writable access to an object payload can flow into ordinary fields, but a handle field forms an inheritance boundary: the parent may authorize rebinding the handle identity, while the pointee payload remains read-only unless the field or binding explicitly carries a payload-side #, such as ^p# or *p#.

5. Functions, Parameters, And cede

Function parameters are explicitly typed.

fn add(a: i32, b: i32) -> i32 {
    return a + b
}

For ordinary object parameters, Toka uses logical in-place capture. If the function wants the payload view, use forms such as x: T or x#: T.

This is a source-level semantic rule, not a promise about physical argument layout. A target ABI may pass scalar values in registers and lower aggregates, handles, closures, or return storage through different representations. Those choices do not create an implicit source copy or change PAL's call-borrow rules. Generated layout and calling convention remain compiler-, target-, and version-bound rather than a stable Toka 1.x binary ABI.

Use a hat on a parameter only when the function needs the handle itself, for example *p: T for a raw handle parameter or *#p: T when the callee must be able to rebind that handle.

At a call site, passing that handle itself also uses the hatted view, such as take(*p). A naked p remains the payload view.

For PAL, a function call is checked as a simultaneous group of temporary borrows. Passing x to a payload parameter is still a borrow event even though the source does not spell &x: x: T creates a temporary shared payload borrow (passed as read(x)), while x#: T creates a temporary exclusive payload borrow (passed explicitly as mutate(x#); passing bare mutate(x) emits warning W0408). The whole argument list is checked together, so read_twice(x, x) is valid for read-only payload parameters, but mutate_twice(x#, x#) and mutate_and_read(x#, x) are rejected when either parameter requires exclusive payload access. A cede argument is an invalidating transfer rather than a borrow and conflicts with any other overlapping argument in the same call.

cede on a formal is a resource-transfer contract. The resolved formal drives the call; repeating cede at the call site is optional but remains legal.

shape Resource(val: i32)

fn keep(cede r: Resource) -> Resource {
    return cede r
}

If a parameter is declared cede, an admitted bare or explicit-cede actual transfers to it. A transferred named place is unavailable afterward. The function body must explicitly complete that transfer by consuming, forwarding, storing, returning, or otherwise ending the resource path. Merely reading the payload does not satisfy the contract. A parameter that was not declared cede cannot be ceded inside the function body.

Default arguments are supported. A call that chooses defaults must include ...

fn test_val(x: i32 = 42) -> i32 { return x }

auto a = test_val(..)

Borrow-like values that escape a function boundary must declare their dependency path in the signature. For Toka 1.0 this is required for private and public functions alike: callers consume the signature, and the callee body must prove that any escaped borrow comes only from the declared dependency sources. This keeps .tki interfaces and source builds aligned.

Reference returns can use effect routing:

fn choose(a: i32, b: i32) -> &res: i32
effects:
    &res <- a | b
{
    if a > b {
        return &a
    }
    return &b
}

Ordinary and extern fn declarations share the same return-signature syntax: both accept async/wait effects and an optional named return binding. Dependency routing (<- and effects:) is a Toka-function contract and is not valid on an extern fn declaration.

The same rule applies to other borrowed views that cross the boundary, including str, bytes, records or shapes containing & fields, and closures or async values that capture borrowed state. The compiler may use local control-flow analysis inside a function, but a call site never depends on inspecting the callee body. Ownership and sharing handles such as ^T and ~T are not borrow-like dependencies by themselves; any dependency comes from borrowed state inside the returned value.

Shape-level header dependencies are not part of the 1.0 syntax. Write the borrow-like field itself:

shape RefInt(
    &val: i32
)

Do not write shape RefInt <- val. The field morphology and the initializer carry the dependency fact; returned-member dependencies are expressed with function effects: routing.

Toka 1.0 also does not support shape-internal member dependency declarations such as &view: i32 <- owner; the parser rejects them as unsupported. That relation would make a shape internally self-referential and needs a stable placement model before it can be safe. Return borrowed views from functions and declare their dependencies there instead. Shape-level effects: blocks are not part of the shape grammar.

Execution boundaries are stricter than ordinary local calls. For Toka 1.0, thread/task handoff must not carry hidden borrowed state: a closure passed to thread_spawn cannot implicitly capture outer variables, and .start follows the same rule. A started task may receive non-borrowing scalar arguments by value. Any shape or resource crossing .start must be transferred through a cede parameter; caller cede spelling is optional. Copyable shapes are not copied implicitly because ordinary object parameters are logical in-place captures. References, str, bytes, raw pointers, and task values carrying PAL dependencies cannot cross .start. Async return dependencies such as fn f(x: str) -> async str <- x remain ordinary signature dependencies; they do not authorize detached tasks to keep an undeclared borrow.

Inside a function declared -> async T, .await is the source-level suspending consumer. Using .await in a function that is not declared async is rejected; using the blocking .wait consumer inside an async function is also rejected. Suspension does not end the current scope or reset semantic state. Locals needed after .await remain coroutine-frame state, and init, move, and PAL borrow facts continue through the suspension point and the surrounding if, match, loop, break, and continue merges. A dependency obtained from an awaited async result remains active after resume, so replacing, moving, or ceding its source is checked exactly as it is in synchronous code. These guarantees do not extend PAL to raw pointers, which remain inside the explicit unsafe/FFI boundary.

Ordinary .await propagates a canceled task as a terminal cancellation and never fabricates a T value. .await? is the explicit recoverable boundary: for a non-void TaskHandle<T> it produces Option<T>, with Option<T>::Some(value) for a normal result and Option<T>::None when either the current task or the awaited task was canceled. Code using .await? must make its cancellation policy visible, for example by mapping None to a domain Result error. It is not an implicit conversion performed by ordinary .await.

PAL (Path-Anchored Ledger) Static Safety Boundary

For Toka 1.0, PAL is frozen as Path-Anchored Ledger: a local, path-based safety checker for the safe language subset. It records borrow, ownership-transfer, and invalidation facts against source-level storage paths, tracking borrowed paths, payload mutation, handle rebinding, resource moves, uninitialized state, and the analysis state produced by if, guard, match, loop, for, break, and continue.

The stable contract is governed by four core rules:

1. Unique ownership is exclusive: A ^ resource is owned by one valid handle at any time.
2. Transfer authority is explicit: Local assignment, return, and capture handoff remain syntactically explicit. At a call, the resolved cede formal is the visible ownership boundary, so caller cede is optional. A unique handle used in a unique value context moves directly (auto ^to = ^from, return ^from) and omits cede; every callee transfer obligation must still be fulfilled.
3. Borrow validity is protected: Operations that can invalidate an active borrow (such as moves, cede, drops, handle rebinding, or reallocations of the underlying storage) are rejected.
4. Exclusive mutation requires exclusive permission: Exclusive/mutable borrows conflict with other overlapping active borrows. A standard immutable borrow is a read-only capability of that borrow view, not a global freeze promise for all storage reachable from the original path. Ordinary payload writes, exclusive mutations, and invalidating operations are classified separately.

Under these rules:

• A function call declares all argument borrows at once; call-site payload passing is not invisible to PAL.
• Implicit dereference or borrow-based argument passing may not raise write permission: a read-only &T view cannot satisfy a T# payload parameter.
• A shared borrow blocks invalidating or exclusive mutation of the same path or an overlapping parent / child path.
• Ordinary payload writes do not by themselves count as invalidation, but writing a parent path that would replace storage containing an active borrow remains invalidating and is rejected.
• A mutable borrow blocks both reads and writes through overlapping paths unless the access is proven disjoint.
• Terminal member borrows such as obj.&field and obj.&#field are recorded against the selected member path, just like &(obj.field).
• Moving or cede-ing a borrowed resource path is rejected.
• Moving a resource path defined outside a loop from a loop backedge is rejected; this includes paths that reach the backedge through continue.
• Interior-mutable fields marked with # may be updated through the explicit field rule, but ordinary fields remain protected by the active borrow.

PAL does not infer hidden lifetime relationships across a function boundary. Escaping borrowed views must be declared in the signature, so source builds and .tki interface builds agree. Raw pointers and unsafe code are outside this safe-borrow guarantee unless wrapped by a safe API whose signature exposes the required dependencies.

6. Shapes, Enums, And Initialization

shape defines aggregate data and tagged enum-like variants.

shape Point(x: i32, y: i32)

shape State(
    On |
    Off |
    ErrCode(i32)
)

Shape fields are named. Shape construction uses named arguments or same-name field punning in multi-field / mixed argument lists:

auto x = 10
auto y = 20
auto p = Point(x, y)             // Field punning (desugars to x = x, y = y)
auto p2 = Point(x, y = 99)       // Mixed pun and explicit override
auto cfg = Config(x, ..)         // Mixed pun and default elision
auto w = Wrapper(value = x)      // Single field requires explicit form

Pure-syntax punning rules:

• When an argument list contains $\ge 2$ bare identifiers, or contains explicit fields (=) / default elision (..), bare identifiers read same-name local bindings.
• A single bare argument (e.g. Wrapper(w)) preserves existing isomorphic copy construction or diagnostics; it never triggers field punning.
• Positional initialization using non-bare expressions (e.g. Point(10, 20) or Point(x + 1, y)) is strictly rejected with E042A.

An initializer creates a new field owner. An existing owned local, field, or fixed-array element must therefore use cede when it initializes an owning field; otherwise the compiler rejects the implicit duplicate cleanup owner. Fresh constructor and call results remain valid directly.

shape Message(body: string)

auto text = string::from("ready")
auto message = Message(body = cede text)

Shape definitions remain compiler-visible type contracts even when some fields are private through @Encap. Interface files must preserve the structural facts needed for semantic checking, including field morphology, mutability, nullability, layout-relevant attributes, and borrow-like member types. Visibility controls user access; it does not erase compiler knowledge.

Fields may have defaults. Use .. to accept remaining defaults.

shape Config(host: i32, port: i32 = 80, debug: i32 = 0)

auto cfg = Config(host = 127, ..)

Position-based struct initialization is not the public style and is rejected by current diagnostics for shapes that require named fields.

Aliases and new nominal types:

alias ID = i32
type UserID = i32

alias is a transparent spelling for its target: values are assignable in both directions, and a shape alias can use the target's constructor. type declares a distinct nominal type: it is not implicitly assignable to or from its target. Construct a shape-backed nominal type with its own name, and use as Target for an explicit conversion when the representation is compatible. Trait implementations are looked up on the nominal type and do not automatically apply from its target. Both forms currently lower with the target's native layout and calling ABI; equal representation does not erase type identity.

7. Methods, Traits, And Encapsulation

Methods are defined in impl blocks.

shape Rect(w: i32, h: i32)

impl Rect {
    pub fn area(self) -> i32 {
        return self.w * self.h
    }
}

Trait implementations use impl Type@Trait.

trait @Shape {
    pub fn area(self) -> i32
}

impl Rect@Shape {
    pub fn area(self) -> i32 {
        return self.w * self.h
    }
}

Traits may declare associated types. A plain type associated type is stable for the whole trait family on a shape: once Data@Mapper<i32>::Output is bound, another Data@Mapper<bool> implementation must use the same Output. A per type associated type is bound per trait instance, so different trait arguments may choose different output types.

trait @Readable {
    type Item
    pub fn read(self) -> Item
}

shape IntBox(value: i32)

impl IntBox@Readable {
    type Item = i32
    pub fn read(self) -> Item {
        return self.value
    }
}

trait @Slot<K> {
    per type Value
    pub fn get(self) -> Value
}

shape IntSlot(value: i32)

impl IntSlot@Slot<i32> {
    per type Value = i32
    pub fn get(self) -> Value {
        return self.value
    }
}

Inside the defining trait or impl block, the associated type name may be used directly in method signatures and local type annotations. Outside the block, use projection syntax: IntBox@Readable::Item or IntSlot@Slot<i32>::Value.

Dynamic trait objects use dyn @Trait in type positions. A concrete value whose type implements the trait may be passed to a parameter expecting dyn @Trait; no & is needed for ordinary parameter passing because Toka parameters capture in place.

fn print_area(item: dyn @Shape) -> i32 {
    return item.area()
}

auto rect = Rect(w = 10, h = 20)
auto area = print_area(rect)

Method calls through dyn @Trait are dynamically dispatched through the trait interface. Outside the defining module, only pub fn methods in the trait are callable. The stable trait-object syntax is a single trait facet such as dyn @Shape; dyn @{A, B} is not part of the current public syntax. Dynamic closures use the separate dyn fn(...) -> T syntax.

Not every trait can be used as dyn @Trait. The 1.0 rule is that a trait object must erase to a fixed receiver handle and a fixed vtable ABI. Therefore, generic traits, traits with associated types, traits with generic methods, and traits whose method signatures use Self outside the receiver position are not valid as dyn @Trait in 1.0.

Toka 1.0 also does not support associated-type binding syntax on dynamic trait objects. Forms such as dyn @Readable<Item = i32> are rejected. Use a concrete generic parameter, a wrapper trait without associated types, or a concrete adapter until this is designed after 1.0.

Trait bounds must use @Trait for a single facet and @{Trait1, Trait2} for a trait facet set. The names inside a trait facet set are bare because the leading @ places the whole set in trait context.

fn draw_one<T: @Drawable>(item: T) {}
fn draw_and_fly<T: @{Drawable, Flyable}>(item: T) {}
fn convert<T, E1: @ErrorInto<E2>, E2>(value: T) {}

Forms such as T: {Drawable, Flyable}, T: {@Drawable, @Flyable}, and T: @{@Drawable, @Flyable} are rejected. path::{...} in imports is an import item list, not a trait facet set.

The standard prelude makes exactly four semantic-core traits implicitly visible: @Encap, @Send, @Sync, and @Callable. All other trait names use the ordinary lexical module namespace and must be declared in the current module or selected by an import. Loading a module does not make its unselected traits visible.

For declarations with non-trivial constraints, use a where: block. Each line is one compile-time constraint. The form matches generic parameter bounds: T: @Trait or T: @{Trait1, Trait2} means the corresponding trait implementation must exist.

fn copy<T>(io: T)
where:
    T: @{Reader, Writer}
{
}

trait @Ord
where:
    Self: @{Eq, PartialOrd}
{
}

@Encap is an explicit resource-policy marker. A resource-owning shape may define one private lifecycle hook, fn drop(self#), in its impl Type@Encap block. The compiler owns the field-cleanup tail; drop is not an ordinary callable method.

The lowercase bare word encap is reserved for a future dedicated language construct. It cannot be used as an identifier; the current trait spelling is always @Encap.

Copying is determined by the compiler's @Copy proof. Non-copyable values simply have no copying capability. A type that intentionally creates another resource-owning value implements @Dup with pub fn dup(self) -> Self. An ordinary method named clone remains possible, but has no ownership, copying, lowering, or trait meaning.

Visibility has two syntax layers:

pub import std/io::{println}
pub shape Device(
    id: i32,
    secret: i32,
    public_config: i32,
    shared_state: i32
)
pub trait @Readable {
    pub fn read(self) -> i32
}

At declaration level, leading pub exports imports, constants, functions, shapes, traits, aliases, and nominal types from the module interface. Omitting pub keeps the declaration module-private.

Inside normal impl and trait blocks, method visibility is written with pub fn. A method without pub is private to its defining module/interface context.

@Encap blocks additionally control member visibility. Once a shape has an @Encap block, its fields are private outside the defining module unless an @Encap visibility entry grants access.

impl Device@Encap {
    pub public_config, shared_state

    fn drop(self#) {}
}

pub field exposes that exact field globally. Parenthesized and wildcard forms are not part of @Encap: pub(crate), pub(path), and pub * are rejected.

Every @Encap field grant is explicit. The grammar has no catch-all member grant, so adding a field later cannot publish it accidentally:

impl PublicRecord@Encap {
    pub visible_name, visible_id, cache_slot
}

8. Member Access And Morphic Fields

Normal member access requests the payload view.

auto x = point.x
point.x = 3

For a member whose declared shape is a handle, place the hat at the member name when the handle itself is needed.

shape Data(^p#: i32)

auto d# = Data(^p = new i32(100))
d.^p = new i32(300) // rebind the member handle
d.p = 500           // write through the payload view

Morphic fields preserve handle shape inside generic code. The quote is written on the binding name, not on the type side.

shape Box<'T>(
    'data: T
)

fn take_identity<'T>(cede box: Box<'T>) -> 'T {
    return cede box.'data
}

Use box.'data when the generic code must preserve the abstract handle shape. Use box.data when the code intentionally requests the payload view.

9. Generics

Rigid generic parameters describe payload types.

shape Box<T>(data: T)

Morphic generic parameters preserve handle shape.

shape Box<'T>('data: T)

In binding positions, the quote belongs to the binding name:

fn id<'T>('x: T) -> 'T {
    return 'x
}

The same rule applies to local bindings: write auto 'local = expr:T, not auto local: 'T = expr. The quote remains binding-side; the type ascription belongs to the initializer.

In pure type positions, write 'T:

Vec<'T>
Option<'T>
-> 'T
sizeof('T)

10. Control Flow

Conditionals do not require parentheses.

if x > 0 {
    return 1
} else {
    return 0
}

Loops:

loop {
    break
}

loop count < 10 {
    count = count + 1
}

for auto x in [1, 2, 3] {
    println("{}", x)
}

for auto x# in [1, 2, 3] {
    x = x + 1
}

# makes the iteration binding writable. The binding keyword is always auto; for let is not part of Toka syntax.

Non-array iteration uses five ordinary traits from core/traits. They are not implicit prelude traits:

trait @Iterable {
    type Iter
    pub fn iter(self) -> Iter <- self
}

trait @Iterator {
    type Item
    pub fn next(self#) -> Option<Item>
}

trait @BorrowIterator {
    type BorrowedItem
    pub fn next_ref(self#) -> Option<BorrowedItem> <- self
}

trait @MutableBorrowIterator {
    type BorrowedItem
    pub fn next_mut(self#) -> Option<BorrowedItem> <- self
}

trait @PlaceIterator {
    type Item
    pub fn next_place(self#) -> __PlaceOutcome<Item> <- self
}

for auto item in values requires values: @Iterable and its Iter type to implement @Iterator. for auto &item in values additionally requires @BorrowIterator; further reference morphology, such as &&item, is preserved in BorrowedItem. The iter and next_ref dependencies are mandatory: PAL keeps the source collection borrowed while an explicit cursor is live and for the duration of a for loop. Mutating, replacing, moving, or ceding the source during that interval is rejected. The hidden cursor is a normal scoped value and is dropped on exhaustion, break, and function exit.

for alias P in values is the explicit element-place form. It creates no Item/reference value. For the qualified shared/read Array and Vec path, the compiler consumes the exact place supplied by @PlaceIterator; its __PlaceOutcome<Item> result is an internal protocol kind and cannot be named, stored, reflected, or constructed by ordinary source. P must exactly reproduce Item morphology: T uses alias x, &T uses alias &x, and so on. Adding or removing a hat is an error. Existing for auto forms remain unchanged and continue to use @Iterator / @BorrowIterator.

Write/rebind intent is declared on the alias pattern, not repeated on the source expression. alias x#, alias ^x#, and alias ^#x request the same payload/handle capabilities as ordinary bindings; each is admitted only when the original element place already has that capability. Alias never amplifies authority and container writability never crosses a handle boundary. A writable non-array alias currently uses the RC8 compatibility lane of iter_mut plus @MutableBorrowIterator::next_mut; both source-backed and TKI-imported signatures retain <- self. This compatibility carrier does not make writable alias part of @PlaceIterator P1 and grants no authority itself. For example, ^T# can supply pointee P, while a writable Vec slot can supply H for ^#x; these are checked independently.

Value iteration does not implicitly cede the collection or its elements. Its ownership behavior is exactly the declared Item returned by next, and the ordinary copy/resource rules still apply. Toka 1.0 does not define a consuming iterator or async-iterator protocol.

while is not part of the current syntax; use loop condition { ... }.

match supports literals, ranges, variants, guards, or-patterns, and the _ wildcard.

auto value = match x {
    0 => { pass 10 }
    auto v if v > 0 => { pass v }
    _ => { pass -1 }
}

For 1.0, enum matches are checked for safe exhaustiveness. Every variant must be covered by an unguarded exhaustive pattern or by _; guarded arms refine a case but do not count as exhaustive. For non-enum targets, use an unguarded wildcard or unconditional variable arm. The compiler does not try to prove full integer, range, or string value-domain coverage.

pass yields a value from a block expression.

11. Pattern Matching And Destructuring

Named destructuring and same-name field punning for shapes:

shape Point(x: i32, y: i32)

auto p = Point(x = 10, y = 20)
auto Point(x, y) = p                 // Same-name pun, declares locals x, y
auto Point(x, other = .y) = p        // Mixed pun and explicit renaming
auto Point(a = .x, b = .y) = p       // Explicit renaming destructuring

Use .. to elide remaining fields and _ to ignore a field.

auto Config(h = .host, ..) = cfg
auto Config(h = .host, _ = .port, d = .debug) = cfg

Variant matching and pattern destructuring:

match result {
    auto Result<i32, str>::Ok(v) => { pass v }
    auto Result<i32, str>::Err(&e) => { pass 0 }
}

Use guard auto for deterministic conditional destructuring and early-exit guards:

guard auto Option<&User>::Some(&user) = find_user(id) else {
    return Result<User, str>::Err("user not found")
}
// Bound variables safely enter the enclosing scope

Because the else block of a guard statement is statically enforced to diverge (return, break, continue, or panic), successfully bound variables enter the enclosing scope directly, eliminating the error-prone two-step status check and .unwrap() anti-pattern.

Or-patterns use |. Every alternative in an or-pattern must bind the exact same names with compatible types and modifiers, because the arm body sees one merged binding environment.

shape OpNode(
    Binary(string, Point) |
    Unary(string, Point) |
    Literal(Point)
)

match node {
    auto OpNode::Binary(&op, pos) | auto OpNode::Unary(&op, pos) => {
        pass pos
    }
    auto OpNode::Literal(pos) => { pass pos }
}

When destructuring resource-carrying values, use explicit borrowing in the pattern when the original value must not be moved.

Destructuring declarations are local in Toka 1.0. A module-level global may bind one value, but a destructuring declaration at module scope is rejected with E0744; destructure that value inside a function instead.

12. Closures

Closures use { ... => ... } syntax.

auto add = { a, b => a + b }:fn(i32, i32) -> i32
auto inc = { .a + 1 }:fn(i32) -> i32
auto zero = { => 0 }:fn() -> i32

Capture lists are written at the beginning of the closure body.

auto f = { [cede env] x => x + env }:fn(i32) -> i32
auto r = 10
auto g = { [copy ~r] x => x + r }:fn(i32) -> i32
auto h = { [dup resource] => resource.value }:fn() -> i32

copy capture is for compiler-proven @Copy values and never invokes user code. It cannot duplicate resource ownership. Use cede to transfer a value, or [dup value] to explicitly invoke that type's verified @Dup::dup provider once while building the closure.

When a closure is converted to dyn fn, any captured outer variable must be listed explicitly with cede, copy, or dup. This keeps owned, movable closures from silently storing borrowed references to local state.

Ordinary fn closures may use implicit borrow captures while they remain local. If such a closure escapes, for example by being returned from the current function, those implicit captures are checked as lifetime dependencies. Use [cede ...], [copy ...], or [dup ...] when the escaping closure should own, copy, or explicitly duplicate the captured state instead of borrowing it.

Callable permission follows Toka receiver morphology rather than a family of nominal Fn traits:

Callable type or receiver	Contract
fn(A) -> R / call(self, ...)	shared, repeatable invocation
fn#(A) -> R / call(self#, ...)	exclusive, repeatable invocation
cede fn(A) -> R / call(cede self, ...)	consuming invocation

The compiler infers a closure's least required permission from its body. Reading captures requires shared invocation, mutating captured state requires exclusive invocation, and transferring a captured value with cede requires consuming invocation. A [cede value] capture only gives the closure ownership; it does not make the closure consuming unless the body transfers that value.

Binding permission remains separate from callable permission:

auto counter# = { [cede state] value =>
    state.value = state.value + value
    state.value
}:fn#(i32) -> i32
auto next = counter#(1)

counter# on the declaration and call grants exclusive access to the binding; fn#(...) records that the callable requires that access. A consuming callable is invoked as cede take(). If the called value is not consuming, the same cede expression applies only to the returned value and does not consume the callable.

@Callable is the single implicit-prelude callable protocol. User-defined types implement a call method with self, self#, or cede self; values of the type then support ordinary call syntax. Generic bounds use F: @Callable. Callable receiver mode and returned lifetime dependencies are preserved in same-version TKI interfaces. Thread callbacks that mutate owned captures use the exclusive fn# contract; detached execution still applies the ordinary explicit-capture, dependency, and @Send rules.

Result propagation

Postfix ! consumes a Result<T, E> or Option<T>. Success moves out the payload. Failure returns Err or None after dropping every still-live local in reverse lexical order. The operand is evaluated exactly once. Propagation from a whole local binding marks that binding moved; partial paths such as holder.result! are conservatively rejected in 1.0 and should first be bound to a local value.

For Result<T, E1> inside a function returning Result<U, E2>, E1 and E2 must be the same resolved type or E1 must implement the ordinary, explicitly imported protocol below:

trait @ErrorInto<Target> {
    pub fn into_error(cede self) -> Target
}

The conversion consumes E1 and runs exactly once on the error path. It is a single direct conversion: Toka does not search conversion chains and does not use numeric widening, structural compatibility, or raw representation copying for errors. Parameterized bounds such as E1: @ErrorInto<E2> are valid in generic declarations and where: blocks. The selected implementation and receiver/return contract are preserved in same-version TKI interfaces.

std/error::ErrorContext<E> stores an owned message and the original typed error. with_context(cede result, message) returns a context-bearing Result without erasing the source. Async .await! applies these same conversion, move, and cleanup rules after resumption. Toka 1.0 has no throw/catch, automatic conversion chain, universal dyn error, or implicit cleanup-error replacement policy.

Typed todos for incomplete edits

todo is a reserved, expression-only keyword for an incomplete edit. It is not a value, variable, wildcard, ownership source, or permissive build mode. Every occurrence has its own diagnostic and keeps the check/build result nonzero.

auto answer = todo:i32       // a complete `i32` requirement is known
if todo {                    // a complete `bool` requirement is known
    return 0
}

The compiler records a requirement only when the surrounding context already determines it: an ascribed initializer, assignment to an existing binding, a boolean condition, an ordinary resolved call parameter, or an explicitly instantiated generic call. The program remains incomplete and reports E04603 in those cases. A context that would need inference, such as auto answer = todo or identity(todo), reports E04604 instead.

Holes cannot stand for a place, capability, provenance, or transfer. Prefix and postfix access, member/index access, guards, cede todo, and todos passed to a cede parameter are rejected with E04605. In particular, a todo never creates H/P authority or silently transfers a resource.

For editor and AI tooling, request deterministic requirement facts with:

toka todo-goals --json --check-only path/to/source.tk
# or: tokac --todo-goals=json --check-only path/to/source.tk

The output is a requirement-only protocol; it is not ordinary semantic evidence and must not be treated as compiler approval. A reachable todo emits no executable, object, TKI, or reusable compilation artifact. See Typed Todo v1 for the machine-readable schema and the RFC for the complete boundary.

13. Strings, Text, And Formatting

String-like values appear in several layers:

Form	Role
"..."	str text view
"""..."""	raw str text view
c"..."	C string literal
string::from("...")	owned mutable string

Raw str literals use a quote fence with three or more double quotes. The closing fence must contain exactly the same number of quotes as the opening fence, so a longer fence can contain a shorter quote run:

auto path = """C:\Users\toka\config.json"""
auto quoted = """"
    Markdown can contain """ without escaping.
    """"

Raw literals do not process escapes or interpolation and have the same static, read-only str representation as ordinary text literals. The fence has no prefix; in particular, c"""...""" is not a raw C string.

A single-line raw literal closes on its opening line. A multiline raw literal starts when only spaces or tabs occur between its opening fence and the next line break. Its opening line break and the line break immediately before the closing fence are structural and are not part of the value. The closing fence must appear on an otherwise blank line; its indentation is removed from every non-blank content line, while additional indentation is preserved. Blank lines are normalized to empty lines, and CRLF, CR, and LF source line endings become \n in the resulting str.

Formatting uses {} placeholders.

println("x={}, y={}", x, y)

Plain {} accepts String and str. Format specifiers for those text forms are outside the 1.0 surface; E04547 identifies that exclusion.

Equality between an owned string and a str view, including a text literal, uses the owned value's zero-allocation read-only as_str() projection. Both command == "scan" and "scan" == command compare contents without allocating, cloning, moving, or consuming command.

The same projection is available when a function or method parameter has the unique expected type str, so an owned string can be passed directly without an explicit .as_str(). It does not apply to *string: obtaining a text view through a raw pointer remains explicit because raw dereference, provenance, and nullability are outside PAL's safe-borrow guarantee.

String concatenation with + is not part of the public syntax. Build owned strings explicitly with string APIs such as push_str.

14. Unsafe And FFI

External functions use extern fn.

extern fn sleep(seconds: i32) -> i32
extern fn libc_free(nul *ptr: void) -> void

Raw allocation and deallocation are explicit and unsafe.

shape Node(val: i32)

auto *node = unsafe alloc Node(val = 1)
unsafe free *node

Built-in alloc is an infallible, non-zero allocation operation: allocation failure terminates instead of producing a zero *T. A fallible native allocator must expose its result as nul *T (for example libc_malloc) and the caller must check or unwrap it explicitly.

For a raw array, the count on free[count] is the number of live elements starting at index zero that must be dropped before the allocation is released. It is not the allocation capacity. A raw container with a contiguous live prefix uses free[len]; after every live element has been moved elsewhere it uses free[0] to release only the storage. Containers whose live elements are not a contiguous prefix must drop those elements themselves and then use free[0].

The compiler's lifecycle plan recurses through fields with ownership, including fixed arrays: dropping a live [T; N] drops each live T. An array element that is a shared or unique handle releases that handle; raw pointers and references remain non-owning. Each element counted by free[count] is likewise dropped as its complete declared type, so a live record element recursively drops its fixed-array fields. This does not make uninitialized raw slots live; raw containers must continue to use free[0] after manually moving or dropping those slots.

auto *buf = unsafe alloc [capacity] Resource
// initialize buf[0..len]
unsafe free [len] *buf

auto *old = unsafe alloc [capacity] Resource
// move every live element from old into replacement storage
unsafe free [0] *old

Pointer casts use as.

auto *ptr = unsafe addr as *i32 // caller asserts that addr is non-zero
auto raw = *ptr as *void

Unsafe code should stay at system and FFI boundaries. Public APIs should avoid exposing raw pointers unless the API is explicitly named as unsafe or raw. Raw pointers are outside PAL's safe-borrow guarantee unless wrapped by a safe library capability.

Core Runtime Contract

On normal scope exits, including structured control-flow exits and returns, every still-live owned value is cleaned up exactly once. A successful cede or move transfers that obligation and prevents cleanup of the moved-from path.

panic is non-returning process termination in Toka 1.0. It is not a catchable exception and does not promise stack unwinding or cleanup after the panic point. Bounds and null checks that fail through the safe runtime use this same non-returning failure boundary. Raw allocation, foreign calls, and raw-pointer validity remain obligations of explicit unsafe/FFI code.

15. Compatibility Contract

Toka 1.x preserves the source-level meaning of programs in the frozen 1.0 surface. Additive features and releases that relax a conservative rejection may be source-compatible extensions. A memory-safety or miscompile correction may reject code that depended on unsound behavior and is recorded as a safety fix.

Diagnostic codes are not reused for unrelated rules during 1.x. Diagnostic wording and source highlighting may improve. .tki, build-cache formats, generated object layout, and binary ABI are compiler- and format-version-bound and do not carry a cross-version compatibility promise.

16. Common Mistakes

Avoid	Use	Reason
let x = 1 / var x = 1	auto x = 1	Toka uses auto for local binding declarations
while cond { ... }	loop cond { ... }	Conditional loops use loop
for x in iter { ... }	for auto x in iter { ... }	Iteration bindings are explicit
for let x in iter { ... }	for auto x# in iter { ... }	# makes an iteration binding writable
Point(1, 2)	Point(x = 1, y = 2)	Shape initialization is named
*p to read the payload	p	Plain names operate on payload
*p = value to write payload	p = value	Hat assignment operates on the handle
p = q to rebind pointer identity	*p = *q	Rebinding is a handle operation
fn read(info: &Info)	fn read(info: Info)	Hats belong to binding names, and ordinary parameters use the payload view
fn inspect(&info: Info) when only reading payload	fn inspect(info: Info)	A hatted parameter is a handle contract, not a spelling for normal passing
shape Ref <- val (&val: T)	shape Ref(&val: T)	Borrow-like fields carry dependency facts directly; shape header dependencies are removed
fn id<'T>(x: 'T) -> 'T	fn id<'T>('x: T) -> 'T	In binding positions, the quote belongs to the binding name
shape Box<'T>('data: 'T)	shape Box<'T>('data: T)	The field name preserves morphology; the type side remains T