# Language Invariants — Types, Effects, and Fallibility

> The core Zero language rules an agent must internalize to write correct .0 source: explicit capabilities via World, opt-in mutability with let mut, mandatory raises + check for fallibility, the Maybe<T> pattern, and why integer casts require as. These invariants are the checkpoints the compiler enforces before any code runs.

- Repository: vercel-labs/zerolang
- GitHub: https://github.com/vercel-labs/zerolang
- Human wiki: https://grok-wiki.com/public/wiki/vercel-labs-zerolang-9ab46b2a38e0
- Complete Markdown: https://grok-wiki.com/public/wiki/vercel-labs-zerolang-9ab46b2a38e0/llms-full.txt

## Source Files

- `skill-data/zero-language.md`
- `examples/fallibility.0`
- `examples/branch.0`
- `examples/memory-primitives.0`
- `examples/point.0`
- `examples/generic-pair.0`
- `conformance/check/pass`

---

<details>
<summary>Relevant source files</summary>
The following files were used as context for generating this wiki page:

- [skill-data/zero-language.md](skill-data/zero-language.md)
- [examples/fallibility.0](examples/fallibility.0)
- [examples/branch.0](examples/branch.0)
- [examples/memory-primitives.0](examples/memory-primitives.0)
- [examples/point.0](examples/point.0)
- [examples/generic-pair.0](examples/generic-pair.0)
- [examples/result-choice.0](examples/result-choice.0)
- [examples/direct-raises-basic.0](examples/direct-raises-basic.0)
- [examples/direct-rescue-basic.0](examples/direct-rescue-basic.0)
- [examples/direct-unhandled-error-exit.0](examples/direct-unhandled-error-exit.0)
- [examples/static-interface.0](examples/static-interface.0)
- [conformance/check/pass/checker-type-forms.0](conformance/check/pass/checker-type-forms.0)
- [conformance/check/pass/memory-types.0](conformance/check/pass/memory-types.0)
- [conformance/check/pass/payload-match.0](conformance/check/pass/payload-match.0)
- [conformance/check/pass/const-arithmetic.0](conformance/check/pass/const-arithmetic.0)
</details>

# Language Invariants — Types, Effects, and Fallibility

Zero is a systems language built around a small set of compiler-enforced invariants: all I/O and side-effects are accessed only through an explicit `World` capability, every binding is immutable by default, and every fallible call site must be marked with `check` or handled with `rescue`. Violating any of these rules is a compile-time error, not a runtime surprise.

This page documents each invariant precisely — what the compiler demands, what the syntax looks like, and what breaks if the rule is absent. It is the primary reference for writing correct `.0` source files.

---

## The `World` Capability: Explicit Effects

Zero has no global I/O. All effects — writing to stdout, reading files, accessing the network — flow through a `World` value that the runtime injects into `main`. Functions that need effects must receive `World` (or a derived capability) as an explicit parameter.

```zero
pub fun main(world: World) -> Void raises {
    check world.out.write("hello from zero\n")
}
```

`world.out.write(...)` is the only path to stdout. A function that does not accept `World` cannot produce observable output, making the effect boundary readable from the signature alone.

**What breaks without it:** A helper function that omits `World` cannot call `world.out.write` — the compiler will reject any attempt to use `world` outside its scope. Pure computation functions intentionally omit `World`, which signals their side-effect-free nature.

Sources: [skill-data/zero-language.md:12-18](), [examples/branch.0:1-8]()

---

## Mutability: `let` vs `let mut`

All bindings are immutable unless explicitly declared mutable with `let mut`. This is not a lint suggestion — the compiler tracks mutation and rejects assignments to immutable bindings.

```zero
pub fun main(world: World) -> Void raises {
    let message = "hello from a binding\n"     // immutable
    check world.out.write(message)
}
```

When a binding does need to change:

```zero
let mut point = Point { x: 1, y: 2 }
bump_x(&mut point)   // passes a mutable borrow
```

The same principle applies to function parameters: `ref<T>` is a read-only borrow (caller passes `&value`), and `mutref<T>` is a mutable borrow (caller passes `&mut value`).

```zero
fun read_x(point: ref<Point>) -> i32 {
    return point.x
}

fun bump_x(point: mutref<Point>) -> Void {
    point.x = point.x + 1
}
```

**What breaks without it:** Passing a `ref<T>` where a `mutref<T>` is required is a type error. The conformance suite explicitly tests this boundary — `conformance/native/fail/mem-copy-immutable-dst.0` demonstrates the "immutable storage passed to a mutable API" error.

Sources: [skill-data/zero-language.md:51-52](), [conformance/check/pass/checker-type-forms.0:20-26](), [examples/direct-raises-basic.0:1-15]()

---

## Fallibility: `raises`, `raise`, `check`, and `rescue`

Zero makes failure explicit at every function boundary.

### Declaring a fallible function

A function that can fail must carry a `raises` marker in its signature. The error set can be open (bare `raises`) or closed (a named set in braces):

```zero
// Open: any error may propagate
pub fun main(world: World) -> Void raises { ... }

// Closed: only InvalidInput can be raised
fun validate(ok: Bool) -> i32 raises { InvalidInput } {
    if ok == false {
        raise InvalidInput
    }
    return 42
}
```

The closed form `raises { Name }` constrains what the function is allowed to raise; the compiler verifies the set is accurate.

### Calling a fallible function: `check`

Every call to a function marked `raises` must be wrapped in `check`. `check` propagates failure upward — the enclosing function must also be marked `raises` to accept that propagation:

```zero
fun run() -> Void raises { InvalidInput } {
    check validate(true)   // propagates InvalidInput if raised
}
```

Omitting `check` is a compile-time error. There is no implicit propagation.

### Handling failure at a boundary: `rescue`

At a non-fallible boundary (e.g., a C-exported entry point), use `rescue` to convert a raised error into a return value:

```zero
export c fun main() -> u8 {
    return parse(false) rescue err { 9_u8 }
}
```

`rescue` turns the error into a local binding (`err` here) and evaluates the block as the function's return value.

### The error propagation chain in practice

```
validate(ok: Bool) -> i32  raises { InvalidInput }
         ↓ check
run()               -> u8   raises { InvalidInput }
         ↓ check
main(world: World)  -> Void raises          (open)
```

Each layer either propagates via `check` or terminates with `rescue`. No intermediate layer can silently discard an error.

Sources: [examples/fallibility.0:1-15](), [examples/direct-raises-basic.0:1-15](), [examples/direct-rescue-basic.0:1-10](), [skill-data/zero-language.md:113-127]()

---

## The `Maybe<T>` Pattern: Representing Absence

Zero has no null. Optional values are represented as `Maybe<T>`, inspected through `.has` (presence) and `.value` (payload). The pattern appears naturally in memory and buffer types:

```zero
shape BufferView {
    bytes: Span<u8>,
    allocator: Maybe<ref<Alloc>>,   // optional read-only allocator
}

shape EditableBuffer {
    bytes: Span<u8>,
    owner: Maybe<mutref<Alloc>>,    // optional mutable allocator
}
```

`Maybe<T>` composes with both `ref<T>` and `mutref<T>`, so optionality and mutability are orthogonal concerns that combine without special syntax.

**What breaks without it:** There is no nullable pointer syntax. Code that needs an "absent" state must use `Maybe<T>` explicitly; the compiler does not permit null to flow through any other type.

Sources: [examples/memory-primitives.0:1-10](), [conformance/check/pass/memory-types.0:1-7](), [skill-data/zero-language.md:133-141]()

---

## Integer Types and Casts: `as` Is Mandatory

Zero has a full numeric tower with explicit widths:

| Category | Types |
|----------|-------|
| Signed integers | `i8`, `i16`, `i32`, `i64`, `isize` |
| Unsigned integers | `u8`, `u16`, `u32`, `u64`, `usize` |
| Floats | `f32`, `f64` |
| Other | `Bool`, `char`, `String`, `Void` |

Integer literals are checked against context. When the type cannot be inferred, a suffix disambiguates:

```zero
let pair: Pair<i32, u8> = makePair(40, 2_u8)   // _u8 suffix
```

Widening or narrowing between integer types is **never implicit**. The `as` keyword is the only mechanism for an intentional cast:

```zero
let byte: u8 = first_byte(readonly)
let widened: u32 = byte as u32    // explicit widening
```

**What breaks without it:** Writing `let widened: u32 = byte` (without `as`) is a type error even though `u8` always fits in `u32`. Zero treats every numeric conversion as a decision the programmer must make deliberately.

Sources: [conformance/check/pass/checker-type-forms.0:53-54](), [skill-data/zero-language.md:63-65](), [examples/generic-pair.0:11]()

---

## Algebraic Types: `shape`, `enum`, and `choice`

Zero provides three composite-type forms with distinct roles:

| Keyword | Role | Matching style |
|---------|------|----------------|
| `shape` | Product type (named fields) | Field access, method receivers |
| `enum` | Enumeration with optional backing type | `match` without payload |
| `choice` | Sum type (tagged union with payloads) | `match` with payload binding |

```zero
shape Point { x: i32, y: i32 }

enum Mode : u8 { off, on }

choice Result { ok: i32, err: String }
```

### Constructing values

```zero
let point = Point { x: 40, y: 2 }     // shape: named fields
let mode: Mode = Mode.on               // enum: qualified name
let result: Result = Result.ok(42)     // choice: constructor with payload
```

### Exhaustive matching

`match` on a `choice` must cover all arms. The `.arm => binding { }` form binds the payload:

```zero
match result {
    .ok => value {
        expect(value == 42)
    }
    .err => message {
        check world.out.write("choice err\n")
    }
}
```

The wildcard `_` arm acts as a catch-all when exhaustive enumeration is unnecessary.

Sources: [examples/result-choice.0:1-23](), [conformance/check/pass/checker-type-forms.0:6-14](), [skill-data/zero-language.md:69-109]()

---

## Memory View Types: `Span<T>`, `MutSpan<T>`, and Fixed Arrays

Zero distinguishes read and write access at the type level for contiguous memory:

| Type | Meaning |
|------|---------|
| `[N]T` | Fixed-size stack array of N elements |
| `Span<T>` | Read-only contiguous view (borrowed) |
| `MutSpan<T>` | Writable contiguous view (borrowed) |
| `owned<T>` | Explicit resource ownership |

```zero
let mut bytes: [4]u8 = [1, 2, 3, 4]
let readonly: Span<u8> = bytes       // coerces to read-only view
let writable: MutSpan<u8> = bytes    // coerces to mutable view
let window = readonly[1..3]          // slice produces a Span<u8>
```

Passing `readonly` where `MutSpan<u8>` is required is a type error (confirmed by the error-tour's "immutable storage passed to a mutable API" example).

Sources: [conformance/check/pass/checker-type-forms.0:49-56](), [examples/memory-primitives.0:15-22](), [skill-data/zero-language.md:130-135]()

---

## Generics: Type and Static Parameters

Generic shapes and functions use angle-bracket type parameters. Zero additionally supports `static` const parameters for compile-time values such as array lengths:

```zero
shape Pair<T, U> {
    left: T,
    right: U,
}

fun makePair<T, U>(left: T, right: U) -> Pair<T, U> {
    return Pair { left: left, right: right }
}

shape FixedVec<T, static N: usize> {
    len: usize,
    items: [N]T,
}
```

Static parameters participate in type checking: `FixedVec<u8, 8>` and `FixedVec<u8, 16>` are distinct types. Interface constraints use the `T: Interface<T>` form:

```zero
fun readValue<T: Readable<T>>(value: ref<T>) -> i32 {
    return T.read(value)
}
```

Sources: [examples/generic-pair.0:1-17](), [skill-data/zero-language.md:145-164](), [examples/static-interface.0:1-24]()

---

## Invariant Summary

```text
┌─────────────────────────────────────────────────────────────────┐
│  Invariant             Rule                   Compiler enforces  │
├─────────────────────────────────────────────────────────────────┤
│  Effects               All I/O via World       Yes — type error  │
│  Mutability            let by default          Yes — type error  │
│  Fallibility (declare) raises on signature     Yes — type error  │
│  Fallibility (call)    check at every call     Yes — type error  │
│  Absence               Maybe<T>, no null       Yes — type error  │
│  Integer casts         as keyword required      Yes — type error  │
│  Match exhaustiveness  All arms required       Yes — type error  │
└─────────────────────────────────────────────────────────────────┘
```

Every row in this table is a property that Zero verifies before generating any output. An agent or programmer writing `.0` source should treat these as hard gates: code that violates any of them will not pass `zero check` and cannot be built or run. The design is intentional — Zero prefers a clear compile error over a runtime surprise, and the invariants are sized to fit in a single mental model.

Sources: [skill-data/zero-language.md:1-167](), [examples/fallibility.0:1-15](), [conformance/check/pass/checker-type-forms.0:44-71]()