Intrepid/prometeu-studio

Fork 0

bQUARKz bc5a1e1dcc

add spec docs

2026-03-24 13:42:16 +00:00

28 KiB

Raw Blame History

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:

Runtime authority (docs/specs/hardware/topics/chapter-2.md, chapter-3.md, chapter-9.md, chapter-12.md, chapter-16.md)
Bytecode authority (docs/specs/bytecode/ISA_CORE.md)
3. Core Syntax Specification.md
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:

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 and ctor bodies.
Self is valid only in struct method and ctor declarations and denotes the enclosing struct type.
The enclosing struct name is in scope inside its own field declarations, enabling self-referential field types.
A named ctor declared in a struct body is not a method, but it does introduce an implicit under-construction this.
A ctor has no declared return annotation and is not a fn.
A ctor completes by falling off the end of its body after initializing the enclosing struct instance.
Every field of the enclosing struct must be definitely assigned on every completing ctor path.
return; and return expr; are both invalid inside ctor bodies.
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.
as in expression position is reserved for explicit contract coercion only; no other cast semantics exist in v1 core.
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:

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

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

  ctor createWithSomethingSpecial(x: int) {
    this.a = 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:

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

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

let cb: TickCb = on_tick;

Bound example:

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:

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:

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:

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:

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:

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.
Bare extraction of a struct or contract method as a value is invalid in v1 core because methods are not first-class.
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 or ctor body,
invalid Self type usage outside struct method or ctor declarations,
invalid struct method declaration shape,
invalid ctor declaration shape,
invalid return inside ctor,
incomplete field initialization on a completing ctor path,
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,
bare method extraction from a struct or contract value,
member projection on a single-slot carrier value,
invalid optional intrinsic member call,
member projection on a missing named output label.

28 KiB Raw Blame History

PBS Static Semantics Specification

1. Purpose

2. Core Semantic Model

2.1 Authority and precedence

2.2 Semantic namespaces

2.3 Tuple shapes

3. Functions and apply

3.1 Canonical function model

3.2 Callable categories

3.3 Declaration validity

3.4 Enum declarations and values

3.5 Structs, methods, and contracts

3.6 Nominal callbacks

3.7 Canonical application

3.8 Call sugar

3.9 Result type of application

3.10 Overload resolution

3.11 Member access and projection

3.12 Block expressions and function fallthrough

3.13 Loop forms

3.14 if and switch conditional expressions

3.15 optional construction and extraction

3.16 result<E> return flow and handling

3.17 Required static diagnostics

28 KiB

Raw Blame History

3. Functions and `apply`

3.14 `if` and `switch` conditional expressions

3.15 `optional` construction and extraction

3.16 `result<E>` return flow and handling