Skip to content

SETTLED-DECISIONS.adoc

Latest commit

 

History

History
156 lines (118 loc) · 5.96 KB

SETTLED-DECISIONS.adoc

File metadata and controls

156 lines (118 loc) · 5.96 KB
Raw

AffineScript: Settled Design Decisions

Table of Contents

This document records design decisions that are fully settled. Each entry gives the decision, the reasoning, and a pointer to the full ADR in .machine_readable/6a2/META.a2ml.

These are not open questions. Do not reopen them without amending the ADR.

Effect Invocation Syntax: Direct Call (ADR-008)

Effect operations are called with plain call syntax. No perform keyword.

fn fetch_user(id: Int) -> User / Http, Async {
  let resp = Http.get("/users/" ++ show(id))
  Async.await(resp.json())
}

The effects are declared once — in the return type (/ Http, Async). The call sites look like ordinary function calls. The type signature is the contract.

perform at every call site is noise that contradicts the ergonomics goal. Face parsers (Python-face, JS-face) can map async/await naturally to the Async effect via desugaring — no perform concept needed.

Conformance Suite Is Authoritative (ADR-009)

The spec is the source of truth. The parser must conform to the spec.

Standing rule: "Language scope lives in a written thesis. Thesis authoritative, code must conform. If disagreement, code is wrong."

As of 2026-04-11, 8/12 valid conformance tests fail to parse. Required fixes:

  1. PascalCase type names — Int, String, Bool, Option, user-defined types are PascalCase. The parser’s ident rule (lowercase only) must be split: ident for values, type_ident (uppercase-leading) for types.

  2. Enum declaration syntax — parser must match the spec’s enum syntax.

  3. Effect op type parameters — parser must support type parameters on effect operations.

Target: 12/12 conformance tests passing. Once passing, any future parser change that breaks a conformance test is a bug, not a spec disagreement.

QTT Surface Syntax: @-Annotations Primary (ADR-007)

The surface forms for quantity annotations are:

@linear        — used exactly once            (:1 sugar also accepted)
@erased        — compile-time only, not at runtime  (:0 sugar also accepted)
@unrestricted  — any number of uses           (:ω sugar also accepted)
                 (default — omitting the annotation means @unrestricted)

@linear/@erased/@unrestricted are the primary forms used in tutorials, error messages, IDE tooling, and generated code. The :1/:0/:ω numeric forms are accepted as sugar (preserved for QTT paper compatibility and for users porting from Idris2/Granule) but are never the canonical form.

Type parameters on generic functions are implicitly erased — no annotation needed:

fn get_name[..r](obj: { name: String, ..r }) -> String = obj.name
//          ^^^  — implicitly @erased (compile-time only)

The own/ref/mut ownership keywords on function parameters are surface syntax for common combinations:

own T   →  @linear T       (caller transfers ownership)
ref T   →  @unrestricted T (read-only borrowed view)
mut T   →  @linear T + mutation rights (exclusive mutable access)

Face-Aware Error Formatting Is a First-Class Toolchain Concern (ADR-010)

When a developer writes Python-face AffineScript and hits a type error, the error must be expressed in Python-face terms — not raw AffineScript canonical syntax.

Architecture:

compiler (canonical error representation, face-agnostic)
      ↓
face-aware error formatter   ← separate layer, swappable
      ↓
terminal / IDE / LSP

The compiler itself has no face knowledge. The formatter receives (error, active-face) and produces the display string. Each face ships an error vocabulary mapping (e.g. Python-face: "affine binding" → "single-use variable").

This is a design commitment, not an immediate implementation task. The compiler’s error representation must be designed with formatability in mind from the start — errors must carry enough structured information for the formatter to reconstruct face-appropriate messages.

typed-wasm: Dual Role (typed-wasm ADR-004)

The typed-wasm repository has two distinct, compatible roles:

  1. Primary: TypeLL 10-level type safety for WebAssembly linear memory. WASM linear memory as a schemaless database with schemas (regions) and type-safe access operations, verified through 10 progressive levels.

  2. Secondary: Aggregate library — the convergence infrastructure for AffineScript and Ephapax. Both languages compile to typed WasmGC and need agreed binary conventions (type layout, ABI, stdlib types, linking). The Idris2 ABI infrastructure that proves the 10-level claims also proves the cross-language layout contracts.

Neither role is subordinate. They are kept distinct in documentation and in src/abi/ (separate Idris2 modules, clear naming).

See typed-wasm/docs/architecture/AGGREGATE-LIBRARY-VISION.adoc for the aggregate library design.

Stdlib Namespace Model: Real Modules (ADR-011)

The standard library uses real modules with qualified paths, not a flat de-duplicated prelude.

Every stdlib/.affine declares module <Name>;; cross-file use is explicit (use option::{Option, Some, None}; / Result::unwrap); there is exactly one canonical definition per name, owned by its module. A minimal prelude module may *re-export the universally needed names (Option, Result, Some/None/Ok/Err) — re-exports, never independent redefinitions.

This resolves the prelude vs option vs result signature-divergent duplicates (prelude.map(arr, f) vs option.map(f, opt)) by single ownership, and makes the AOT pipeline exercise real cross-module resolution — the actual objective of issue #128. It is consistent with the machinery the compiler (module_loader.ml, module/use/:: grammar) and the newer stdlib files (Core, Deno, Vscode, …) already use.

Settles issue #132; gates #133/#135/#137/#138. Full ADR in .machine_readable/6a2/META.a2ml (ADR-011).