prometeu-studio/docs/specs/pbs/4. Static Semantics Specification.md

# PBS Static Semantics Specification

Status: Draft v1 (Normative)  
Scope: binding, callable formation, type checking, and deterministic function application

## 1. Purpose

This document defines the static semantics of PBS core language.

It is intended to:

- give deterministic meaning to declarations accepted by the syntax specification,
- define callable identity and application rules,
- make type checking stable across implementations,
- preserve beginner-facing clarity without hidden callable behavior.

## 2. Core Semantic Model

### 2.1 Authority and precedence

Normative precedence:

1. Runtime authority (`docs/specs/hardware/topics/chapter-2.md`, `chapter-3.md`, `chapter-9.md`, `chapter-12.md`, `chapter-16.md`)
2. Bytecode authority (`docs/specs/bytecode/ISA_CORE.md`)
3. `3. Core Syntax Specification.md`
4. This document

If a rule here conflicts with higher authority, it is invalid.

### 2.2 Semantic namespaces

PBS distinguishes at least:

- type namespace,
- value namespace,
- callable namespace.

Rules:

- `declare struct`, `declare contract`, `declare error`, `declare enum`, and `declare callback` introduce names in the type namespace.
- `let`, parameters, and `declare const` introduce names in the value namespace.
- Top-level `fn`, service methods, and `host fn` participate in the callable namespace.
- `fn` declarations are not first-class values in v1 core and therefore do not become ordinary value expressions.
- `bind(...)` is a callback-formation construct, not a general function-value construct.

### 2.3 Tuple shapes

Static checking uses tuple shapes as semantic objects.

Definitions:

- Input tuple shape: ordered sequence of zero or more input slots.
- Output tuple shape: ordered sequence of zero or more output slots.
- Each slot has a type and a stable label.

Rules:

- Tuple shapes in PBS core are always named, except for unit `()`.
- Input slot labels come from parameter names and are local frame names.
- Output slot labels come from return annotations and are visible for multi-slot member projection.
- Tuple-shape identity for overload and resolution ignores labels.
- Tuple-shape compatibility requires matching arity and positional slot types.
- Labels must still be preserved as part of declaration surface and projection metadata.
- A single-slot tuple shape has a distinguished carrier value type equal to its slot type.
- In value positions, single-slot tuple values collapse to their carrier value type.
- Single-slot tuple shapes have no dedicated tuple-literal surface in v1 core.

## 3. Functions and `apply`

### 3.1 Canonical function model

Every callable `fn` in PBS is modeled statically as:

```text
Fn : InputTuple -> OutputTuple
```

Rules:

- `fn f(a: A, b: B)` has input tuple shape `(a: A, b: B)`.
- `fn f()` has empty input tuple shape `()`.
- `-> void`, `-> ()`, and omitted return annotation all denote empty output tuple shape `()`.
- `-> T` denotes a single-slot output tuple shape `(value: T)`.
- `-> (x: T)` denotes a single-slot output tuple shape `(x: T)`.
- `-> (x: T, y: U)` denotes a two-slot output tuple shape `(x: T, y: U)`.
- `-> T` and `-> (x: T)` are identical for overload identity and differ only in preserved label metadata.
- `optional T` is a regular value type and may appear in parameters, locals, fields, and plain returns.
- `optional T` with single-slot payload is internally normalized to `optional<(value: T)>`.
- `optional` and `optional void` are invalid type surfaces.
- `-> result<E> T` denotes a result return surface over payload shape `T` and error type `E`.
- `-> result<E> T` with single-slot payload is internally normalized to `result<E, (value: T)>`.
- `-> result<E>` is valid and denotes a result return surface with unit payload.
- A function return surface may be plain or `result<E>`.
- A function return surface must not combine `optional` and `result` in the same declaration.
- `result<E>` wraps the declared success payload; the payload itself may be scalar or a named tuple shape.

### 3.2 Callable categories

The following constructs are callable in v1 core:

- top-level `fn`,
- struct methods on concrete receivers,
- contract values,
- callback values,
- service methods,
- `host fn`.

Rules:

- All callable categories use the same input/output tuple model.
- A struct method is identified by `(struct type, method name, input tuple shape excluding the receiver slot, output tuple shape)`.
- A contract value is identified at the type level by its contract type and at runtime by an underlying concrete struct instance plus its selected implementation.
- A callback declaration defines a nominal callable type with exactly one input/output tuple shape.
- A service method is identified by `(service name, method name, input tuple shape, output tuple shape)`.
- A top-level `fn` is identified by `(name, input tuple shape, output tuple shape)`.
- A callback value is identified at the type level by its declared callback type and signature.
- A `host fn` is identified by `(name, input tuple shape, output tuple shape)` and has no PBS body.
- Contract signatures and barrel signatures must preserve the same callable shape.

### 3.3 Declaration validity

Rules:

- Parameter names in a single `ParamList` must be unique.
- Output labels in a named tuple return annotation must be unique.
- Error case labels in a single `declare error` body must be unique.
- Enum case labels in a single `declare enum` must be unique.
- Enum case integer identifiers in a single `declare enum` must be unique.
- Two declarations with the same callable name and the same input/output tuple shape are duplicates.
- Changing only parameter names does not create a new callable.
- Changing only input labels in `ParamList` does not create a new callable.
- Changing only output labels does not create a new callable.
- `mod.barrel` function entries are matched by callable identity, ignoring labels.
- Barrel labels may differ from implementation labels.
- Any return surface that combines `optional` and `result` is statically invalid.
- Any payload-less `optional` type surface is statically invalid.
- Any `optional void` type surface is statically invalid.

### 3.4 Enum declarations and values

Rules:

- `declare enum Name(case1, case2, ...);` introduces a nominal enum type `Name`.
- `declare enum Name(case1 = n1, case2 = n2, ...);` introduces explicit integer identifiers for enum cases.
- If no enum case uses an explicit identifier, identifiers are assigned as `0..n-1` in declaration order.
- If any enum case uses an explicit identifier, then every enum case in that declaration must use an explicit identifier.
- `Name.case` is a valid enum value surface only when `Name` resolves to a declared enum type and `case` resolves to a declared case of that enum.
- The static type of `Name.case` is the enum type `Name`.
- Error labels are not enum cases and must not be used where enum case values are required.

### 3.5 Structs, methods, and contracts

Rules:

- Struct values are heap-backed reference values in v1 core.
- `new Struct(args...)` allocates a new struct instance of the declared struct type.
- `new Struct.ctorName(args...)` invokes a named constructor declared in the enclosing struct body and produces a new struct instance of that type.
- Struct construction arguments are matched positionally to the declared struct field order.
- Assigning a struct value copies the reference, not the underlying field storage.
- Struct fields are mutable and accessible by default in v1 core.
- A struct method declared in a struct body has an implicit receiver binding `this` of type `Self`.
- `this` is valid only inside struct method bodies.
- `Self` is valid only in struct method and `ctor` declarations and denotes the enclosing struct type.
- A named `ctor` declared in a struct body is not a method and does not introduce `this`.
- `ctor` bodies return the enclosing struct type and may use explicit `return`.
- Methods declared in a struct body belong to the direct method namespace of that concrete struct type.
- `receiver.method(...)` on a concrete struct receiver resolves only against methods declared directly in that struct body.
- `receiver.ctorName(...)` is never valid on a concrete struct value.
- Contract implementations do not inject their methods into the direct method namespace of the concrete struct.
- `implements Contract for Struct using s { ... }` is unique per `(Contract, Struct)` pair.
- A contract for a struct may be implemented only in the module where the struct itself is declared.
- Contracts may be declared in other modules and implemented for the local struct in its owner module.
- An `implements` block has no independent visibility; its observability follows the visibility of the struct, and the contract must also be nameable at the use site.
- A struct value may be coerced to a contract value when exactly one visible `implements Contract for Struct ...` applies.
- Contract coercion may happen by explicit `expr as ContractType` or by contextual typing in assignments, parameter passing, and returns.
- A contract value carries the underlying struct reference together with the selected contract implementation for runtime dispatch.
- Calling `contractValue.method(...)` uses dynamic dispatch through the contract value.
- Calling `structValue.contractMethod(...)` is not valid unless that method is also declared directly on the struct.
- Structs do not have static methods in v1 core; named constructors are their only type-qualified callable members.

Example:

```pbs
declare contract StasisProcess {
  fn stasis() -> int;
}

declare struct Struct(a: int) {
  fn compute() -> int {
    return this.a;
  }

  ctor createWithSomethingSpecial(x: int) {
    return new Struct(x);
  }
}

implements StasisProcess for Struct using s {
  fn stasis() -> int {
    return s.compute();
  }
}

fn demo() -> int {
  let s = new Struct(1);
  let s2 = new Struct.createWithSomethingSpecial(2);
  let sp: StasisProcess = s;
  let sp2 = s as StasisProcess;
  let a = s.compute();
  let _ = s2.compute();
  let b = sp.stasis();
  let c = sp2.stasis();
  return a + b + c;
}
```

### 3.6 Nominal callbacks

Rules:

- `declare callback Name(params...) -> R;` introduces a nominal callback type `Name`.
- A callback type is not a `fn`, and a `fn` declaration does not implicitly define a callback type.
- A value of callback type may be formed only from a compatible top-level `fn` in v1 core.
- A value of callback type may also be formed by `bind(context, fn_name)` when the surrounding static type context expects a callback type.
- Service methods are not assignable to callback values in v1 core.
- `host fn` declarations are not assignable to callback values in v1 core.
- Callback values do not capture local environment implicitly.
- Assignment of a top-level `fn` to a callback type succeeds only when exactly one visible overload matches the callback signature.
- `bind(context, fn_name)` succeeds only when exactly one visible top-level `fn` overload matches after consuming the first parameter with `context`.
- Valid expected callback contexts for `bind(context, fn_name)` include variable initialization with an explicit callback type, assignment to an explicitly typed callback location, argument passing to a callback-typed parameter, and return from a callback-typed function.
- The context expression in `bind(context, fn_name)` is evaluated once at bind time and stored explicitly in the resulting callback value.
- The stored context follows normal value semantics for its type.
- `bind(context, fn_name)` does not introduce general closures; it is explicit partial binding of the first parameter only.
- Callback compatibility ignores labels and compares ordered input/output slot types plus the return-surface kind.

Example:

```pbs
declare callback TickCb(dt: int) -> void;

fn on_tick(dt: int) -> void {
}

let cb: TickCb = on_tick;
```

Bound example:

```pbs
declare callback UpdateCb(dt: int) -> void;

declare struct Enemy(hp: int);

fn update_enemy(self: Enemy, dt: int) -> void {
}

let cb: UpdateCb = bind(enemy, update_enemy);
```

Ambiguous overload example:

```pbs
declare callback TickCb(dt: int) -> void;

fn tick(dt: int) -> void {
}

fn tick(time: int) -> void {
}

let cb: TickCb = tick; // error: ambiguous overloaded fn assignment
```

### 3.7 Canonical application

The canonical surface form for function application is:

```pbs
callee apply arg
```

Rules:

- `apply` is an infix operator that is right-associative.
- `f1 apply f2 apply x` is defined as `f1 apply (f2 apply x)`.
- `f1 apply f2 apply f3 apply params` is defined as `f1 apply (f2 apply (f3 apply params))`.
- The left operand of `apply` must resolve to one of: a callable candidate set, a bound struct method target, a contract-method target, or a callback value.
- The right operand of `apply` is an argument expression.
- If the callable input arity is `0`, the argument expression must be `()`.
- If the callable input arity is `1`, the argument expression is checked against the carrier type of the single input slot.
- If the callable input arity is `2..6`, the argument expression must have a named tuple shape with matching arity and positional types.
- Input labels are not used for compatibility.
- No single-slot tuple argument literal is required or recognized in surface syntax.
- There is no partial application in v1 core.
- There is no currying in v1 core.
- Chained `apply` is nested ordinary application, not callable composition as a first-class value.
- Callback values, `host fn`, service methods, struct methods, and contract-method targets use the same `apply` rules as top-level `fn`.

### 3.8 Call sugar

The surface form:

```pbs
callee(arg1, arg2, ..., argN)
```

desugars to the canonical `apply` surface according to arity.

Rules:

- The desugaring is purely syntactic.
- `f()` is exact sugar for `f apply ()`.
- `f(x)` is exact sugar for `f apply x`.
- `f(x1, x2, ..., xn)` for `n >= 2` is exact sugar for `f apply (x1, x2, ..., xn)`.
- No semantic distinction exists between direct call sugar and its canonical `apply` form.
- When `(arg1, ..., argN)` is used as positional tuple sugar, the callee input tuple shape supplies the effective labels.
- All overload resolution, diagnostics, and type checking are defined on the canonical `apply` form.

### 3.9 Result type of application

Rules:

- If the selected callable output arity is `0`, the result of `apply` is unit.
- If the selected callable output arity is `1`, the result of `apply` is the carrier type of the single output slot.
- If the selected callable output arity is `2..6`, the result of `apply` has the named output tuple shape of the selected callable.
- Multi-slot output tuple results expose their labels for member projection.
- If the selected callable is a callback value, the visible multi-slot output labels come from the callback type rather than from the original source `fn`.
- If the selected callable returns `()`, the application result is unit.

Example:

```pbs
fn func(a: int, b: int) -> (c: int, d: float) {
  return (c: a + b, d: 2.0);
}

let params: (a: int, b: int) = (1, 2);
let r = func apply params;
let c = r.c;
let d = r.d;
```

In the example above:

- `func` has input tuple shape `(a: int, b: int)`,
- `func` has output tuple shape `(c: int, d: float)`,
- `r` has named output tuple type `(c: int, d: float)`,
- `r.c` has type `int`,
- `r.d` has type `float`.

Single-slot example:

```pbs
fn plus_one(x: int) -> int {
  return x + 1;
}

let r = plus_one apply 1;
if r == 2 { }
```

In the example above:

- `plus_one` has input tuple shape `(x: int)`,
- the argument `1` is accepted directly as the carrier value for the single input slot,
- `plus_one` has output tuple shape `(value: int)`,
- the value produced by `plus_one apply 1` has carrier type `int`,
- `r.value` is not required and should not be used.

### 3.10 Overload resolution

Rules:

- Overload resolution starts from the visible callable candidates with the selected name.
- Candidate filtering first uses callable kind and input tuple arity.
- Remaining candidates are filtered by positional input type compatibility.
- If exactly one candidate remains, resolution succeeds.
- If multiple candidates remain, expected output types or expected multi-slot output tuple shapes may be used as a tie-breaker when statically available.
- If multiple candidates still remain, the `apply` is ambiguous and compilation fails.
- If no candidate remains, the `apply` is unresolved and compilation fails.
- Overloads that differ only by labels are duplicates and are forbidden.
- Overloads that differ only by output positional types are permitted, but uncontextualized `apply` sites may become ambiguous.

### 3.11 Member access and projection

Rules:

- `TypeName.case` is valid when `TypeName` resolves to a declared enum type and `case` resolves to one of its declared enum cases.
- `TypeName.case` has static type `TypeName`.
- `expr.name` is valid when the static type of `expr` is a declared `struct` containing field `name`.
- For `struct` field access, the projected member type is the declared field type.
- `expr.method` is a valid method-call target when the static type of `expr` is a concrete struct type declaring method `method`.
- `expr.method` over a concrete struct receiver does not search visible contract implementations.
- `TypeName.ctorName` is not a general member access surface; named constructors are entered only through `new TypeName.ctorName(...)`.
- `expr.method` is a valid method-call target when the static type of `expr` is a contract value whose contract declares method `method`.
- `expr.name` is valid when the static type of `expr` is a multi-slot named output tuple containing label `name`.
- For named output tuples, the projected member type is the type of the corresponding output slot.
- Projection is label-based, not position-based.
- `expr.hasSome()` and `expr.hasNone()` are valid intrinsic method-call surfaces when the static type of `expr` is `optional<P>`.
- `expr.hasSome()` and `expr.hasNone()` both have static type `bool`.
- `expr.name()` and `expr.key()` are valid intrinsic method-call surfaces when the static type of `expr` is an enum type.
- `expr.name()` has static type `str`.
- `expr.key()` has static type `int`.
- Access to a missing output label is a compile-time error.
- Access to a missing struct field is a compile-time error.
- Access to a missing struct method is a compile-time error.
- Access to a missing contract method is a compile-time error.
- Member projection is not defined for single-slot collapsed carrier values.

### 3.12 Block expressions and function fallthrough

Rules:

- A block expression with a `TailExpr` has the static type of that final expression.
- A block expression without a `TailExpr` has static type unit.
- Only the final unsemicoloned expression in a block contributes to the block result.
- A function body does not implicitly return its trailing `TailExpr`; explicit `return` and ordinary control-flow rules still apply.
- Reaching the end of a plain non-unit function is a compile-time error unless all control-flow paths are proven to return explicitly.
- Reaching the end of a `void` or `()` function is valid and yields unit.
- Reaching the end of an `optional P` function yields `none`.
- Reaching the end of a `result<E>` function is a compile-time error.

### 3.13 Loop forms

Rules:

- `while cond { ... }` requires `cond` to have static type `bool`.
- `for i: T from start until end { ... }` is the declarative counted loop form in v1 core.
- `for i: T from start until end step s { ... }` is the explicit-step counted loop form in v1 core.
- In `for`, the declared iteration variable `i` introduces a loop-local binding of type `T`.
- `start`, `end`, and `step` expressions in `for` must be type-compatible with the declared iteration type `T`.
- If `step` is omitted, the loop uses the integer value `1` of the iteration type domain.
- `for` iteration proceeds by evaluating `start`, `end`, and optional `step` once before loop entry.
- `for ... until ...` uses an exclusive upper bound.
- `continue` inside `while` transfers control to the next condition check.
- `continue` inside `for` transfers control to the step update and then to the next bound check.
- `break` exits the nearest enclosing loop.

### 3.14 `if` and `switch` conditional expressions

Rules:

- In `if cond { a } else { b }`, `cond` must have static type `bool`.
- Only the selected branch is evaluated at runtime.
- The branch expressions `a` and `b` must have the same static type, subject only to ordinary contextual typing already defined elsewhere in the language.
- The static result type of the `if` expression is that shared static type.
- In `switch selector { pattern: { ... }, ... }`, the selector expression is evaluated once.
- `switch` accepts enum selectors and literal-comparable scalar selectors; `error` selectors are invalid.
- Each non-wildcard `switch` arm pattern must be unique within the same `switch`.
- Each non-wildcard `switch` arm pattern must be type-compatible with the selector expression.
- Enum-case switch patterns must resolve to declared cases of the selector's enum type.
- Error labels are not valid switch patterns.
- `default` and `_` are equivalent wildcard spellings for `switch`.
- At most one wildcard arm may appear in a `switch`.
- A `switch` must not mix `default` and `_` in the same arm set.
- The blocks of all `switch` arms must have the same static type, subject only to ordinary contextual typing already defined elsewhere in the language.
- The static result type of the `switch` expression is that shared static type.
- A `switch` used as an `ExprStmt` is valid when the selected arm blocks evaluate to unit.
- A `switch` expression used in a value-required position must be exhaustive, either by a wildcard arm or by another statically proven exhaustive case set.

### 3.15 `optional` construction and extraction

Rules:

- `some(expr)` forms an `optional<P>` value where `P` is the static type of `expr`, unless an expected `optional<Q>` context is present and constrains `expr` to be compatible with `Q`.
- `some(expr)` is invalid when the payload normalizes to `void`.
- `none` is valid only when an expected `optional<P>` type is available from context.
- `opt else fallback` requires the left operand to have static type `optional<P>`.
- In `opt else fallback`, the `fallback` expression must be compatible with payload shape `P`.
- The static result type of `opt else fallback` is the carrier value type for single-slot payloads and the named tuple payload shape for multi-slot payloads.
- `opt else fallback` does not introduce implicit mutation or unwrapping side effects beyond normal expression evaluation.

### 3.16 `result<E>` return flow and handling

Rules:

- `return ok(expr);` is valid only inside a function whose declared return surface is `result<E> P`.
- In `return ok(expr);`, `expr` must be compatible with the declared success payload shape `P`.
- `return err(E.label);` is valid only inside a function whose declared return surface is `result<E> P`.
- In `return err(E.label);`, the error path must resolve to a declared case of the same error type `E`.
- `ok(...)` and `err(...)` do not denote ordinary value expressions in v1 core.
- `expr!` requires `expr` to have static type `result<E> P`.
- `expr!` is valid only when the enclosing function returns `result<E> Q` for the same error type `E`.
- The static result type of `expr!` is the extracted success payload shape `P`, collapsed to its carrier value when single-slot.
- `handle expr { ... }` requires `expr` to have static type `result<E1> P`.
- `handle expr { ... }` is valid only when the enclosing function returns `result<E2> Q` for some payload `Q`.
- Each non-wildcard `handle` arm must match a distinct declared case of `E1`.
- Each mapped error path on the right side of a `handle` arm must resolve to a declared case of `E2`.
- `handle` arms must be exhaustive over `E1`, either by naming all cases exactly once or by providing `_`.
- The static result type of `handle expr { ... }` is the extracted success payload shape `P`, collapsed to its carrier value when single-slot.
- On error, `handle` performs an immediate enclosing-function return with the mapped `err(...)`.

### 3.17 Required static diagnostics

At minimum, deterministic static diagnostics are required for:

- duplicate parameter names in `fn` declarations,
- duplicate output labels in named tuple returns,
- duplicate error case labels in `declare error`,
- duplicate enum case labels in `declare enum`,
- duplicate enum case identifiers in `declare enum`,
- invalid mixed implicit/explicit enum case identifiers,
- invalid `this` usage outside struct method body,
- invalid `Self` type usage outside struct method or `ctor` declarations,
- invalid struct method declaration shape,
- invalid `ctor` declaration shape,
- duplicate `implements Contract for Struct` pair,
- `implements` declared outside the owner module of the struct,
- incompatible or missing contract method implementation,
- invalid contract coercion from concrete struct value,
- unresolved barrel function signature after label-insensitive matching,
- unresolved callback barrel entry,
- invalid enum case path,
- invalid enum intrinsic member call,
- invalid named constructor target,
- incompatible top-level `fn` assignment to callback type,
- ambiguous overloaded top-level `fn` assignment to callback type,
- attempted assignment of service method to callback type,
- attempted assignment of `host fn` to callback type,
- use of `bind(...)` without an expected callback type,
- incompatible `bind(...)` context type for callback target,
- ambiguous overloaded top-level `fn` target in `bind(...)`,
- `apply` on a non-callable target,
- arity mismatch in `apply`,
- argument type mismatch in `apply`,
- `apply` chain with incompatible intermediate carrier/tuple shape,
- ambiguous overload resolution,
- unresolved callable application,
- possible fallthrough of plain non-unit function,
- non-boolean `while` condition,
- invalid `for` iteration type,
- incompatible `for` bound or step type,
- non-boolean `if` expression condition,
- incompatible `if` expression branch types,
- duplicate `switch` arm pattern,
- mixed `default` and `_` wildcard arms in `switch`,
- invalid `switch` selector type,
- selector-pattern type mismatch in `switch`,
- invalid enum case switch pattern,
- incompatible `switch` arm block types,
- non-exhaustive `switch` expression in value position,
- invalid mixed `optional`/`result` return surface,
- invalid payload-less `optional` type surface,
- invalid `optional void` type surface,
- invalid `none` usage without expected optional type,
- invalid `else` extraction over non-optional operand,
- fallback type mismatch in `else` extraction,
- invalid `some(...)` construction form,
- use of `ok(...)` or `err(...)` outside `return`,
- invalid `ok(...)` construction form,
- invalid `err(...)` construction form,
- invalid error label in `err(...)`,
- invalid `!` propagation on non-result expression,
- mismatched error type in `!` propagation,
- invalid `handle` on non-result expression,
- non-exhaustive `handle` mapping,
- duplicate `handle` mapping arm,
- invalid mapped error label in `handle`,
- attempted use of a single-slot tuple literal where no such surface form exists,
- member access on a missing struct field,
- member access on a missing struct method,
- member access on a missing contract method,
- member projection on a single-slot carrier value,
- invalid optional intrinsic member call,
- member projection on a missing named output label.