diff --git a/crates/ailang-core/tests/docs_honesty_pin.rs b/crates/ailang-core/tests/docs_honesty_pin.rs index 092fc42..454a731 100644 --- a/crates/ailang-core/tests/docs_honesty_pin.rs +++ b/crates/ailang-core/tests/docs_honesty_pin.rs @@ -41,8 +41,12 @@ fn design_corpus() -> String { read("design/models/rc-uniqueness.md"), read("design/contracts/float-semantics.md"), read("design/contracts/typeclasses.md"), + read("design/contracts/method-dispatch.md"), + read("design/contracts/prelude-classes.md"), + read("design/contracts/language-constraints.md"), read("design/models/effects.md"), read("design/models/authoring-surface.md"), + read("design/models/prose-projection.md"), ] .join("\n") } @@ -100,7 +104,7 @@ fn design_md_present_tense_anchors_present() { let memory = norm(&read("design/contracts/memory-model.md")); let pipeline = norm(&read("design/models/pipeline.md")); let str_abi = norm(&read("design/contracts/str-abi.md")); - let typeclasses = norm(&read("design/contracts/typeclasses.md")); + let prelude_classes = norm(&read("design/contracts/prelude-classes.md")); let records = norm(&read("docs/journals/2026-05-19-design-decision-records.md")); // the discriminator meta-subsection -> contracts/honesty-rule.md @@ -122,8 +126,8 @@ fn design_md_present_tense_anchors_present() { "float_to_str must be present-tense honest-reserved in str-abi.md"); assert!(records.contains("AILang demands annotations *because* the LLM author can produce them effortlessly"), "the 'does not infer everything' bullet must be present-tense in the decision-records (no doc-archaeology)"); - assert!(typeclasses.contains("`io/print_str` is the only built-in direct-output effect-op"), - "the print-op set must be stated present-tense in typeclasses.md, not as a retirement narrative"); + assert!(prelude_classes.contains("`io/print_str` is the only built-in direct-output effect-op"), + "the print-op set must be stated present-tense in prelude-classes.md (post-split home), not as a retirement narrative"); assert!(records.contains("the render in `crates/ailang-prose/src/lib.rs` is a placeholder and informational only"), "the Form-B class/instance prose-projection state must be present-tense in the decision-records"); } diff --git a/design/INDEX.md b/design/INDEX.md index ab5773c..bee3686 100644 --- a/design/INDEX.md +++ b/design/INDEX.md @@ -82,6 +82,7 @@ is the default. | feature-acceptance | brainstorm-gate / stable | skills/brainstorm/SKILL.md | design/contracts/feature-acceptance.md | | authoring-surface | LLM author / stable | crates/ailang-surface/tests/round_trip.rs | design/contracts/authoring-surface.md | | roundtrip-invariant | every release / stable | crates/ailang-surface/tests/round_trip.rs | design/contracts/roundtrip-invariant.md | +| language-constraints | LLM author / stable | crates/ailang-check/src/uniqueness.rs (in-source mod tests) | design/contracts/language-constraints.md | | memory-model | LLM author / stable | crates/ailang-check/src/uniqueness.rs (in-source mod tests) | design/contracts/memory-model.md | | data-model | LLM author / stable | crates/ailang-core/tests/design_schema_drift.rs | design/contracts/data-model.md | | mangling | codegen / stable | crates/ail/tests/eq_ord_e2e.rs | crates/ailang-codegen/src/lib.rs //! | @@ -90,6 +91,8 @@ is the default. | frozen-value-layout | embedding ABI / one-way-frozen| crates/ailang-codegen/tests/embed_record_layout_pin.rs | design/contracts/frozen-value-layout.md + runtime/rc.c §layout | | float-semantics | LLM author / stable | crates/ail/tests/eq_float_noinstance.rs | design/contracts/float-semantics.md | | typeclasses | LLM author / stable | crates/ail/tests/show_no_instance_e2e.rs | design/contracts/typeclasses.md | +| method-dispatch | LLM author / stable | crates/ail/tests/show_no_instance_e2e.rs | design/contracts/method-dispatch.md | +| prelude-classes | LLM author / stable | crates/ail/tests/show_no_instance_e2e.rs | design/contracts/prelude-classes.md | | str-abi | runtime ABI / stable | crates/ail/tests/e2e.rs (Str path) | design/contracts/str-abi.md + runtime/str.c §heap-Str | | tail-calls | codegen / stable | crates/ailang-check/src/lib.rs (in-source tail_call_in_non_tail_position_is_rejected) | design/contracts/tail-calls.md | | honesty-rule | architect+grounding / stable | crates/ailang-core/tests/docs_honesty_pin.rs | design/contracts/honesty-rule.md | @@ -104,4 +107,5 @@ is the default. | typeclasses | onboarding / evolves | design/models/typeclasses.md | | effects | onboarding / evolves | design/models/effects.md | | authoring-surface | onboarding / evolves | design/models/authoring-surface.md | +| prose-projection | onboarding / evolves | design/models/prose-projection.md | | pipeline | onboarding / evolves | design/models/pipeline.md | diff --git a/design/contracts/authoring-surface.md b/design/contracts/authoring-surface.md index 4c6dff1..0cc8ea9 100644 --- a/design/contracts/authoring-surface.md +++ b/design/contracts/authoring-surface.md @@ -18,7 +18,7 @@ the same time, leaving only diagnostic helpers (`type_to_string`, The textual surface is **not** a replacement for the JSON-AST. It is one projection among potentially many. Concretely: -- The JSON-AST keeps its role as the canonical, hashable, content- +- The [JSON-AST](data-model.md) keeps its role as the canonical, hashable, content- addressed representation of a module. All hashing, content- addressing, cross-module references, and typecheck/codegen input flow through the JSON-AST. **No new hashable form is introduced.** @@ -55,7 +55,7 @@ the AST and remain projection-agnostic. shape. The full bijection between `.ail.json` and `.ail` (both directions, BLAKE3-stable hashing, Float-bits-hex encoding, workspace-CI enforcement points) is anchored as the top-level - §"Roundtrip Invariant" — this constraint records that Decision + [Roundtrip Invariant](roundtrip-invariant.md) — this constraint records that Decision 6's surface-design choice must satisfy that invariant; the invariant itself lives at top level because the property is load-bearing on the language identity, not on this Decision's diff --git a/design/contracts/data-model.md b/design/contracts/data-model.md index 82169b2..8617aaf 100644 --- a/design/contracts/data-model.md +++ b/design/contracts/data-model.md @@ -167,7 +167,8 @@ are real surface forms. ``` In the MVP, `do` is only a direct call to a built-in effect op (no -handler). A `lam` term constructs an anonymous function value; free +handler); the effect system is described in [effects](../models/effects.md). +A `lam` term constructs an anonymous function value; free variables of its body are captured from the enclosing scope. Loop binders are alloca-resident: typecheck binds them in the @@ -237,6 +238,10 @@ Patterns are linear: each pattern variable may appear at most once. `implicit ≡ own` semantically; the distinction exists so existing unannotated fixtures continue to serialize without the mode wrapper and keep their -canonical-JSON hash. +canonical-JSON hash. The full mode contract (codegen consequences, +the over-strict-mode lint, the `Suppress` mechanism) lives in +[memory model](memory-model.md); the four language-design +preconditions that make RC sound live in +[language constraints](language-constraints.md). Ratified by: `crates/ailang-core/tests/design_schema_drift.rs`. diff --git a/design/contracts/embedding-abi.md b/design/contracts/embedding-abi.md index 332e5b9..4a93460 100644 --- a/design/contracts/embedding-abi.md +++ b/design/contracts/embedding-abi.md @@ -47,8 +47,9 @@ ctx-threaded C signature is the M2 shape. Export parameters are written **bare**: a scalar type carries no `own`/`borrow` mode (a single-constructor record export parameter, -by contrast, carries `own`/`borrow` — the ownership contract the -frozen value layout below specifies). The +by contrast, carries `own`/`borrow` — see [memory model](memory-model.md) +for the full ownership contract; the +frozen value layout below specifies how that contract lands at the C ABI). The canonical M1 export shape: ``` diff --git a/design/contracts/feature-acceptance.md b/design/contracts/feature-acceptance.md index 89cab06..ebe5fdf 100644 --- a/design/contracts/feature-acceptance.md +++ b/design/contracts/feature-acceptance.md @@ -29,7 +29,8 @@ A proposed feature ships only if all three hold: RC-acyclicity guarantees were built to remove. The decisive question is whether the construct re-opens a class of mistakes (iterated-mutable-state reasoning, silently-unbounded recursion, - reference cycles) that a foundational invariant closes. If it does, + reference cycles) that a foundational invariant — see + [language constraints](language-constraints.md) — closes. If it does, it is cut even when 1 and 2 hold — *or* it must be reshaped until the bug class is structurally impossible rather than merely discouraged. A documentation note is not a reshape; the diff --git a/design/contracts/float-semantics.md b/design/contracts/float-semantics.md index e1dd54f..afc6603 100644 --- a/design/contracts/float-semantics.md +++ b/design/contracts/float-semantics.md @@ -66,7 +66,7 @@ no `f32` variant. The runtime / codegen contract: The same libc-`%g` rendering applies to `show 1.5` / `show nan` / `show inf` via `instance Show Float` (which calls `float_to_str` -internally — see [Prelude (built-in) classes](typeclasses.md) for the Show ship). +internally — see [Prelude (built-in) classes](prelude-classes.md) for the Show ship). The NaN-spelling caveat above is observable via `do print x` for Float-typed `x`; the rendering is libc-version-dependent and target-libc-specific. AILang does NOT canonicalise Float textual @@ -83,12 +83,16 @@ use case appears. **Form-A serialisation:** Float literals carry the IEEE-754 bit pattern as a 16-character lowercase hex string in the canonical -JSON: `{"kind":"float","bits":"<16-hex>"}`. Routing through the +JSON: `{"kind":"float","bits":"<16-hex>"}` (see +[Data model](data-model.md) for the literal schema). Routing through the JSON *string* path (not `serde_json::Number`) preserves bit stability across `serde_json` versions and lets NaN / ±Inf round-trip through Form-A — JSON numbers cannot represent them. +This bits-hex encoding is what keeps Floats inside the +[Roundtrip Invariant](roundtrip-invariant.md). -**Pattern matching:** `Pattern::Lit` on `Literal::Float` is hard- +**Pattern matching:** `Pattern::Lit` on `Literal::Float` (see +[Data model](data-model.md) for the pattern schema) is hard- rejected at typecheck (`CheckError::FloatPatternNotAllowed`). IEEE semantics make Float patterns semantically dubious — NaN never matches via IEEE-`==`, and bit-exact equality is rarely what an diff --git a/design/contracts/frozen-value-layout.md b/design/contracts/frozen-value-layout.md index c4fdc8a..93347ba 100644 --- a/design/contracts/frozen-value-layout.md +++ b/design/contracts/frozen-value-layout.md @@ -3,7 +3,8 @@ ## Frozen value layout (M3 — one-way commitment) For a single-constructor `data T` whose `n` fields are each `Int` -or `Float`, a value of `T` crossing the embedding C boundary is a +or `Float`, a value of `T` crossing the +[embedding C boundary](embedding-abi.md) is a bare payload pointer `p`: | bytes | content | @@ -27,8 +28,9 @@ offsets above. A raw `malloc` is a contract violation: `own`-consume and `ailang_rc_dec` both require the runtime's 8-byte header at `p - 8` initialised to `1`. -**Ownership follows the declared mode** (the §"Mode metadata is -load-bearing for codegen" contract, as the C ABI): a `(own (con +**Ownership follows the declared mode** (the +[Mode metadata is load-bearing for codegen](memory-model.md) +contract, as the C ABI): a `(own (con T))` parameter transfers ownership in — the kernel consumes it (Iter-B drop-at-return); the host MUST NOT touch or `dec` it after the call. A `(borrow (con T))` parameter is retained by the host — diff --git a/design/contracts/honesty-rule.md b/design/contracts/honesty-rule.md index 92f5467..6699f63 100644 --- a/design/contracts/honesty-rule.md +++ b/design/contracts/honesty-rule.md @@ -15,9 +15,10 @@ Two things never belong in a contract or model file: A cross-reference that does belong stays: it is a formal, file-relative Markdown link into the durable tier (`design/` or -source), enforced by `design_index_pin.rs` clause-5. A reference -that cannot be expressed as such a link is, by that fact, the -history-or-rationale prose the rule above removes. +source), enforced by +[`design_index_pin.rs`](../../crates/ailang-core/tests/design_index_pin.rs) +clause-5. A reference that cannot be expressed as such a link is, +by that fact, the history-or-rationale prose the rule above removes. The single legitimate exception is a present-tense reserved or deliberately-excluded claim that is explicitly and correctly diff --git a/design/contracts/language-constraints.md b/design/contracts/language-constraints.md new file mode 100644 index 0000000..1bd99a9 --- /dev/null +++ b/design/contracts/language-constraints.md @@ -0,0 +1,40 @@ +# Language-design constraints (binding) + +## Language-design constraints (binding) + +The four constraints below are necessary preconditions for RC to +be sound and complete *without* a cycle-collector backstop. They +are not new — AILang already satisfies all four — but Decision 10 +makes them load-bearing rather than incidental: + +1. **Strict evaluation.** Every `Term::App` (see + [Data model](data-model.md)) argument is fully + evaluated before the call. No laziness, no thunks. (Already + true.) +2. **No recursive value bindings.** `(let x EXPR ...)` evaluates + `EXPR` in a scope where `x` is *not* bound. Recursion is + exclusively via `Term::LetRec` (which binds a fn, not a value) + and module-level fn defs. (Already true.) +3. **No shared mutable refs.** Values are immutable once + constructed. There is no `ref`, `IORef`, `Mutex`, or any + primitive that allows a value to be mutated from a position + outside its allocation. (Already true.) +4. **ADTs are acyclic by construction.** Strict evaluation + + no-recursive-value-bindings + no-shared-mutable-refs together + guarantee that any value graph reachable from a binding is a + DAG. The reference graph has no cycles. (Follows from 1–3.) + +Laziness, recursive value bindings, shared mutable state, or any +feature that creates cycles is rejected at design time unless the +proposal proves the cycle is collectible by an extension (e.g. +linear ownership). + +These constraints are the precondition for the +[memory model](memory-model.md): a sound RC implementation without +a cycle-collector backstop requires the reference graph to be a +DAG, which constraint 4 establishes from 1–3. They are also the +load-bearing structural reason behind several +[feature-acceptance](feature-acceptance.md) clause-3 rejections +(notably iterated-mutable-state reasoning). + +Ratified by: `crates/ailang-check/src/uniqueness.rs` (in-source mod tests). diff --git a/design/contracts/memory-model.md b/design/contracts/memory-model.md index c1e7fa8..917eb3a 100644 --- a/design/contracts/memory-model.md +++ b/design/contracts/memory-model.md @@ -1,38 +1,19 @@ -# Memory model — language-design constraints and codegen contract +# Memory model — schema, diagnostics, codegen contract -## Language-design constraints (binding) - -The four constraints below are necessary preconditions for RC to -be sound and complete *without* a cycle-collector backstop. They -are not new — AILang already satisfies all four — but Decision 10 -makes them load-bearing rather than incidental: - -1. **Strict evaluation.** Every `Term::App` argument is fully - evaluated before the call. No laziness, no thunks. (Already - true.) -2. **No recursive value bindings.** `(let x EXPR ...)` evaluates - `EXPR` in a scope where `x` is *not* bound. Recursion is - exclusively via `Term::LetRec` (which binds a fn, not a value) - and module-level fn defs. (Already true.) -3. **No shared mutable refs.** Values are immutable once - constructed. There is no `ref`, `IORef`, `Mutex`, or any - primitive that allows a value to be mutated from a position - outside its allocation. (Already true.) -4. **ADTs are acyclic by construction.** Strict evaluation + - no-recursive-value-bindings + no-shared-mutable-refs together - guarantee that any value graph reachable from a binding is a - DAG. The reference graph has no cycles. (Follows from 1–3.) - -Laziness, recursive value bindings, shared mutable state, or any -feature that creates cycles is rejected at design time unless the -proposal proves the cycle is collectible by an extension (e.g. -linear ownership). +The four language-design constraints that make RC sound without a +cycle-collector backstop (strict evaluation, no recursive value +bindings, no shared mutable refs, acyclic ADTs) live in +[language constraints](language-constraints.md); this file covers +the schema additions, advisory diagnostics, and codegen contract +that build on them. ## Schema additions -**Parameter modes on `Type::Fn`.** +**Parameter modes on `Type::Fn`** (see [Data model](data-model.md) +for the schema-level definition of `Type::Fn`). -The form-A surface for fn signatures gains mode wrappers: +The form-A surface (see [authoring surface](authoring-surface.md)) +for fn signatures gains mode wrappers: ``` (fn-type (params (borrow (List Int))) (ret (con Int))) @@ -102,7 +83,7 @@ Three schema fields carry class references in this form: `ClassDef.name` itself stays bare (defining-site context, like `TypeDef.name`). -Method dispatch is type-driven post-mq.3 (see [Method dispatch](typeclasses.md)): +Method dispatch is type-driven post-mq.3 (see [Method dispatch](method-dispatch.md)): synth resolves a `Term::Var { name: "show" }` by consulting the workspace's method-to-candidate-class index, filtering by argument type (concrete) or by declared constraint (rigid-var), and @@ -167,8 +148,8 @@ until the fixture intentionally adopts the feature. **`FnDef.suppress`.** The `suppress` field on `FnDef` carries a list of advisory-diagnostic suppress entries; each entry has a `code` (the diagnostic being suppressed) and a `because` (a -mandatory non-empty reason). See §"Data model" for the canonical -schema. +mandatory non-empty reason). See [Data model](data-model.md) for +the canonical schema. Form-A surface: `(suppress (code "...") (because "..."))` clause between fn name and `(type ...)`. Multiple clauses allowed; one diff --git a/design/contracts/method-dispatch.md b/design/contracts/method-dispatch.md new file mode 100644 index 0000000..7f309c4 --- /dev/null +++ b/design/contracts/method-dispatch.md @@ -0,0 +1,54 @@ +# Method dispatch + +## Method dispatch + +The class-method resolution rule that pairs with the +[typeclasses](typeclasses.md) contract; the `Show`/`Eq`/`Ord` instances +the rule dispatches against live in [prelude classes](prelude-classes.md). + +Post-mq.3, dispatch is two-mode: + +**Polymorphic call sites** (inside a fn body with `forall` + +constraint set): the constraint names the class via the qualified +`Constraint.class` field (canonical-form per mq.1). Synth's +residual carries the class name directly; constraint-discharge at +fn-body-end matches against the workspace registry by +`(class, type_hash)` key. + +**Monomorphic call sites**: synth consults the workspace-flat +`Env.method_to_candidate_classes: BTreeMap>` index, then runs the 5-step +dispatch rule: + +1. Parse the `Term::Var.name` for an optional class qualifier + (last-dot-segment is the method name; everything before is the + qualified class). +2. If `method_to_candidate_classes` has no entry for the method + name, fall through to the existing Var-arm branches (free fn + lookup, dot-qualified cross-module). +3. Qualifier present: filter candidates to the named class. Empty + result fires `UnknownClass`. Singleton survivor proceeds. +4. Qualifier empty (bare-method form): singleton candidate proceeds + directly; multiple candidates yield a multi-candidate residual + for discharge-time refinement. +5. At discharge, refinement runs: concrete `type_` filters + candidates via the workspace registry; rigid-var `type_` filters + via the active fn's declared constraints + (`env.active_declared_constraints`). Single survivor discharges; + multiple survivors fire `AmbiguousMethodResolution` (concrete) or + `MissingConstraint` (rigid-var); zero survivors fire `NoInstance` + (concrete) or `MissingConstraint` (rigid-var). + +The `method_to_candidate_classes` index is the load-bearing data +structure for this routing — its construction in `build_check_env` +inverts the per-module `class_methods` maps (themselves tuple-keyed +by `(qualified-class, method)` post-mq.3) to a workspace-flat +method-name-to-class-set map. + +Class-fn collisions resolve at the call site, not at workspace load +time: the fn lookup precedence (locals → caller-module-fn → +imported-fn) runs ahead of the class-method branch. When both +sides have a match, the fn wins and a `class-method-shadowed-by-fn` +warning surfaces the shadow. + +Ratified by: `crates/ail/tests/show_no_instance_e2e.rs`. diff --git a/design/contracts/prelude-classes.md b/design/contracts/prelude-classes.md new file mode 100644 index 0000000..d94dc94 --- /dev/null +++ b/design/contracts/prelude-classes.md @@ -0,0 +1,32 @@ +# Prelude (built-in) classes + +## Prelude (built-in) classes + +The prelude ships the `Ordering` ADT, the `Eq` and `Ord` +[classes](typeclasses.md), primitive `Eq Int/Bool/Str` and +`Ord Int/Bool/Str` instances, and the five polymorphic free-fn +helpers `ne`/`lt`/`le`/`gt`/`ge`. Float has neither `Eq` nor `Ord` +instance per [Float semantics](float-semantics.md); a polymorphic +helper invoked at Float fires `NoInstance` at typecheck with a +Float-aware diagnostic cross-referencing this section. The lookup +machinery that turns a `show x` call site into the right monomorphic +instance is documented in [method dispatch](method-dispatch.md). + +The prelude ships `class Show a where show : (a borrow) -> Str` and +primitive `Show Int`, `Show Bool`, `Show Str`, `Show Float` +instances. Float **is** included in Show (unlike Eq/Ord) — IEEE-754 +makes structural equality and total ordering semantically dubious, +but textual representation of a Float is well-defined modulo the +NaN-spelling caveat in [Float semantics](float-semantics.md). Each +`Show ` instance body is a single-application lambda invoking the +corresponding runtime primitive (`int_to_str`, `bool_to_str`, +`str_clone`, `float_to_str`; see [Str ABI](str-abi.md) for the +heap-Str primitives); no codegen intercept is required. The +polymorphic helper `print : forall a. Show a => a -> () !IO` has body +`\x -> let s = show x in do io/print_str s` (explicit let-binder for +heap-Str RC discipline per eob.1 Str carve-out). The let-binder is +structurally pinned by `crates/ail/tests/print_mono_body_shape.rs`. +Routing through `print` is the path for non-`Str` primitives; +`io/print_str` is the only built-in direct-output effect-op. + +Ratified by: `crates/ail/tests/show_no_instance_e2e.rs`. diff --git a/design/contracts/roundtrip-invariant.md b/design/contracts/roundtrip-invariant.md index f78dabd..8f1291e 100644 --- a/design/contracts/roundtrip-invariant.md +++ b/design/contracts/roundtrip-invariant.md @@ -3,11 +3,12 @@ ## Roundtrip Invariant Every well-formed AILang module has a canonical `.ail.json` -representation (the hashable, content-addressed JSON-AST) and a -hand-authored `.ail` representation (Form A, the authoring -projection). The JSON-AST is derived from `.ail` in-process by -consumers that need it; the round-trip is now the *property* of -that derivation, not the byte-level agreement of two on-disk forms. +representation (the hashable, content-addressed +[JSON-AST](data-model.md)) and a hand-authored `.ail` representation +(Form A, the [authoring projection](authoring-surface.md)). The +JSON-AST is derived from `.ail` in-process by consumers that need +it; the round-trip is now the *property* of that derivation, not +the byte-level agreement of two on-disk forms. Concretely: @@ -46,9 +47,9 @@ approximation. The canonical encoding is `{"kind":"float","bits":"<16-lowercase-hex>"}` and the surface emits the same bits-hex string. NaN, ±Inf, signed zero, and subnormals all round-trip exactly because the JSON-number path is bypassed (see -§"Float semantics", "Form-A serialisation"). Floats are not an -exception to the invariant — the bits-hex encoding is the -mechanism that keeps them *inside* it. +[Float semantics](float-semantics.md), "Form-A serialisation"). +Floats are not an exception to the invariant — the bits-hex +encoding is the mechanism that keeps them *inside* it. ### Enforcement diff --git a/design/contracts/scope-boundaries.md b/design/contracts/scope-boundaries.md index 5acce24..32ce608 100644 --- a/design/contracts/scope-boundaries.md +++ b/design/contracts/scope-boundaries.md @@ -4,12 +4,14 @@ Snapshot of the current boundary. -- No effect handlers — only the built-in `IO` op (`io/print_str`). +- No effect handlers — only the built-in `IO` op (`io/print_str`); + the effect system is described in [effects](../models/effects.md). `Diverge` is a reserved effect name with no op and no codegen. - No refinements / SMT escalation. - No HM inference inside bodies. Top-level def types are explicit; - polymorphism is opt-in via `Type::Forall { vars, body }`. Inside - a body, lambdas check monomorphically against their declared type. + polymorphism is opt-in via `Type::Forall { vars, body }` (see + [Data model](data-model.md)). Inside a body, lambdas check + monomorphically against their declared type. - Polymorphic fns must be **directly called** at the use site. Passing a polymorphic fn as a value (`let f = id in f(42)`) is not yet supported. @@ -17,11 +19,12 @@ Snapshot of the current boundary. polymorphic fn (`apply(id, 42)`) is not supported. - No recursive `let` for non-fn values. Plain `let x = … in …` only sees `x` inside the body, not inside its own RHS — recursive value - bindings would break Decision 10's acyclicity invariant. Recursive + bindings would break the + [acyclicity invariant](language-constraints.md). Recursive *fn* bindings are supported via `Term::LetRec` (`{ "t": "letrec", ... }`); the desugar pass lifts most occurrences to a synthetic top-level fn, with `lift_letrecs` finishing the residue after - typecheck. + typecheck (see [pipeline](../models/pipeline.md)). - No visibility rules in imports. Every top-level def of an imported module is reachable; there is no `pub` / `priv`. @@ -30,8 +33,9 @@ What **is** supported (and used as the smoke test for the pipeline): - Int, Bool, Unit, **Str**, **Float** as primitive types. - `if`, `let`, function calls, recursion. - Effects on function signatures, with `do op(args)` for direct effect - ops (`io/print_str`). The polymorphic `print` (§"Polymorphic print") - is the canonical output path for non-Str values. + ops (`io/print_str`). The polymorphic `print` (see + [prelude classes](prelude-classes.md)) is the canonical output + path for non-Str values. - **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`) of type `forall a. (a, a) -> a` (codegen-restricted to `{Int, Float}`); `%` of type `(Int, Int) -> Int` (Int-only — `fmod` semantics for @@ -99,14 +103,17 @@ What **is** supported (and used as the smoke test for the pipeline): `(term-ctor std_pair.Pair MkPair x y)` and `(pat-ctor MkPair x y)` inside that scrutinee. Std-library demos (`examples/std_*_demo.ail.json`) exercise this end-to-end. -- **AI-authoring text surface, form (A)** (Decision 6). The `ailang-surface` crate parses `.ail` form-A - text into a canonical `ailang-core::ast::Module` and prints any module - back as form-A text. `ail render` and `ail describe` use it as the +- **AI-authoring text surface, form (A)** (see + [authoring surface](authoring-surface.md)). The `ailang-surface` + crate parses `.ail` form-A text into a canonical + `ailang-core::ast::Module` and prints any module back as form-A + text. `ail render` and `ail describe` use it as the sole text projection; `ail parse` is the inverse direction. Round-trip identity (text → AST → JSON → AST → text) is gated by `ailang-surface/tests/round_trip.rs` over every shipped fixture. -- **Memory management via Boehm conservative GC** (Decision 9), - with **per-fn arena via stack `alloca` for non-escaping allocations** +- **Memory management via Boehm conservative GC** (see + [RC + uniqueness](../models/rc-uniqueness.md)), with + **per-fn arena via stack `alloca` for non-escaping allocations** layered on top. Every ADT box, lambda env, and closure pair allocates either via `@GC_malloc` (escaping; Boehm-managed) or via LLVM `alloca` (non-escaping; freed at fn return). The decision diff --git a/design/contracts/str-abi.md b/design/contracts/str-abi.md index 2623f01..bedd5a7 100644 --- a/design/contracts/str-abi.md +++ b/design/contracts/str-abi.md @@ -12,13 +12,15 @@ and return an owned `Str`. Each is registered as a builtin in and backed by a `runtime/str.c` C helper. - `int_to_str : (borrow Int) -> Str` — decimal rendering - of an `Int`. Backs `Show Int` in the prelude. + of an `Int`. Backs `Show Int` in the + [prelude](prelude-classes.md). - `bool_to_str : (borrow Bool) -> Str` — `"true"`/`"false"`. - Backs `Show Bool` in the prelude. + Backs `Show Bool` in the [prelude](prelude-classes.md). - `float_to_str : (borrow Float) -> Str` — type-installed; codegen is reserved and not yet shipped. - `str_clone : (borrow Str) -> Str` — allocates a fresh - heap-Str copy of the input's bytes. Backs `Show Str` in the prelude. + heap-Str copy of the input's bytes. Backs `Show Str` in the + [prelude](prelude-classes.md). - `str_concat : (borrow Str, borrow Str) -> Str` — combines two `Str` values into a single owned `Str`. General-purpose; commonly used in Show bodies for labelled output @@ -32,8 +34,8 @@ instance body that wants to combine fragments. Primitive output for `Str` values goes through `io/print_str` directly; values of other primitive types route through the -polymorphic `print` helper (§"Polymorphic print"), which feeds -the heap-Str result of `show x` into `io/print_str`. +polymorphic `print` helper (see [prelude classes](prelude-classes.md)), +which feeds the heap-Str result of `show x` into `io/print_str`. `==`, `<`, `<=`, `>`, `>=` REMAIN primitive operators. Class methods are accessed by name (`eq x y`, `lt x y`, …), not via these @@ -57,7 +59,8 @@ bytes, regardless of realisation. The byte-comparison semantics are inherited from libc `strcmp` — locale-independent, NUL- terminated. -The heap-Str realisation participates in standard RC: the +The heap-Str realisation participates in standard RC (see +[memory model](memory-model.md)): the `rc_header` slot eight bytes before the `len` field is managed by `ailang_rc_alloc` / `ailang_rc_inc` / `ailang_rc_dec` exactly like any other RC-allocated cell. The static-Str realisation has diff --git a/design/contracts/tail-calls.md b/design/contracts/tail-calls.md index 78109b3..ae8f424 100644 --- a/design/contracts/tail-calls.md +++ b/design/contracts/tail-calls.md @@ -12,7 +12,8 @@ hazard the language exists to eliminate. Solution: explicit, verified tail calls. - **AST.** `Term::App { fn, args, tail: bool }` and - `Term::Do { op, args, tail: bool }` gain a `tail` flag, + `Term::Do { op, args, tail: bool }` (see + [Data model](data-model.md)) gain a `tail` flag, serde-defaulting to `false` so existing fixtures load with `tail: false` and their hashes stay bit-identical. - **Typecheck.** A new pass `verify_tail_positions(fn_body)` @@ -37,7 +38,8 @@ Solution: explicit, verified tail calls. Productions are positional analogues of `app`/`do` with `tail: true` set on the resulting term. EBNF gains 2 lines; total production count goes from ~28 to ~30, still inside - the constraint-1 budget. + the constraint-1 budget (see + [authoring surface](authoring-surface.md)). **What this does NOT promise.** Per the tail-call survey of existing fixtures, many existing recursive calls are *not* in tail position diff --git a/design/contracts/typeclasses.md b/design/contracts/typeclasses.md index e6f8607..0d187c0 100644 --- a/design/contracts/typeclasses.md +++ b/design/contracts/typeclasses.md @@ -1,8 +1,18 @@ # Typeclasses +The schema, registry, and diagnostic contract for the typeclass +layer. The resolution/monomorphisation whitepaper lives at +[models/typeclasses](../models/typeclasses.md); the call-site +lookup rule at [method dispatch](method-dispatch.md); the built-in +classes the prelude ships at [prelude classes](prelude-classes.md). + ## Form-A schema (the JSON authoring surface) Three additive schema extensions; no existing module becomes invalid. +The canonical schema for `ClassDef`, `InstanceDef`, and the +`FnDef.type` constraints field lives in +[Data model](data-model.md); this section is the typeclass-layer +narrative. **`ClassDef`** — top-level definition kind, declares a class: @@ -181,7 +191,7 @@ wording is fixed; the categories and their triggers are: Cross-class method sharing is structurally legal; ambiguity surfaces at the call site via `AmbiguousMethodResolution` or, for class-fn name overlap, via the `class-method-shadowed-by-fn` warning. See -§"Method dispatch" below. +[Method dispatch](method-dispatch.md). **Class-schema diagnostics** (validation of class declarations): @@ -222,78 +232,6 @@ There is no `AmbiguousInstance` diagnostic at the registry level — coherence (`DuplicateInstance` at registry build, W2) makes per-`(class, type)` ambiguity structurally impossible. Cross-class method ambiguity is a separate concern resolved at the call site -via `AmbiguousMethodResolution` (see §"Method dispatch" below). - -## Method dispatch - -Post-mq.3, dispatch is two-mode: - -**Polymorphic call sites** (inside a fn body with `forall` + -constraint set): the constraint names the class via the qualified -`Constraint.class` field (canonical-form per mq.1). Synth's -residual carries the class name directly; constraint-discharge at -fn-body-end matches against the workspace registry by -`(class, type_hash)` key. - -**Monomorphic call sites**: synth consults the workspace-flat -`Env.method_to_candidate_classes: BTreeMap>` index, then runs the 5-step -dispatch rule: - -1. Parse the `Term::Var.name` for an optional class qualifier - (last-dot-segment is the method name; everything before is the - qualified class). -2. If `method_to_candidate_classes` has no entry for the method - name, fall through to the existing Var-arm branches (free fn - lookup, dot-qualified cross-module). -3. Qualifier present: filter candidates to the named class. Empty - result fires `UnknownClass`. Singleton survivor proceeds. -4. Qualifier empty (bare-method form): singleton candidate proceeds - directly; multiple candidates yield a multi-candidate residual - for discharge-time refinement. -5. At discharge, refinement runs: concrete `type_` filters - candidates via the workspace registry; rigid-var `type_` filters - via the active fn's declared constraints - (`env.active_declared_constraints`). Single survivor discharges; - multiple survivors fire `AmbiguousMethodResolution` (concrete) or - `MissingConstraint` (rigid-var); zero survivors fire `NoInstance` - (concrete) or `MissingConstraint` (rigid-var). - -The `method_to_candidate_classes` index is the load-bearing data -structure for this routing — its construction in `build_check_env` -inverts the per-module `class_methods` maps (themselves tuple-keyed -by `(qualified-class, method)` post-mq.3) to a workspace-flat -method-name-to-class-set map. - -Class-fn collisions resolve at the call site, not at workspace load -time: the fn lookup precedence (locals → caller-module-fn → -imported-fn) runs ahead of the class-method branch. When both -sides have a match, the fn wins and a `class-method-shadowed-by-fn` -warning surfaces the shadow. - -## Prelude (built-in) classes - -The prelude ships the `Ordering` ADT, the `Eq` and `Ord` classes, -primitive `Eq Int/Bool/Str` and `Ord Int/Bool/Str` instances, and -the five polymorphic free-fn helpers `ne`/`lt`/`le`/`gt`/`ge`. Float -has neither `Eq` nor `Ord` instance per §"Float semantics"; a -polymorphic helper invoked at Float fires `NoInstance` at typecheck -with a Float-aware diagnostic cross-referencing this section. - -The prelude ships `class Show a where show : (a borrow) -> Str` and -primitive `Show Int`, `Show Bool`, `Show Str`, `Show Float` -instances. Float **is** included in Show (unlike Eq/Ord) — IEEE-754 -makes structural equality and total ordering semantically dubious, -but textual representation of a Float is well-defined modulo the -NaN-spelling caveat in §"Float semantics". Each `Show ` instance -body is a single-application lambda invoking the corresponding -runtime primitive (`int_to_str`, `bool_to_str`, `str_clone`, -`float_to_str`); no codegen intercept is required. The polymorphic -helper `print : forall a. Show a => a -> () !IO` has body -`\x -> let s = show x in do io/print_str s` (explicit let-binder for -heap-Str RC discipline per eob.1 Str carve-out). The let-binder is -structurally pinned by `crates/ail/tests/print_mono_body_shape.rs`. -Routing through `print` is the path for non-`Str` primitives; -`io/print_str` is the only built-in direct-output effect-op. +via `AmbiguousMethodResolution` (see [Method dispatch](method-dispatch.md)). Ratified by: `crates/ail/tests/show_no_instance_e2e.rs`. diff --git a/design/contracts/verification.md b/design/contracts/verification.md index 95373f9..04be46d 100644 --- a/design/contracts/verification.md +++ b/design/contracts/verification.md @@ -4,7 +4,8 @@ 1. **Snapshot tests** for the pretty-printer and IR emit. The diff makes regressions visible immediately. -2. **Property tests** for the JSON ↔ pretty-print roundtrip. +2. **Property tests** for the JSON ↔ pretty-print + [roundtrip](roundtrip-invariant.md). 3. **End-to-end tests** for `examples/` with expected program output. 4. **Hash stability**: a test ensures the same def always produces the same hash. diff --git a/design/models/authoring-surface.md b/design/models/authoring-surface.md index f8a9bba..963e5a4 100644 --- a/design/models/authoring-surface.md +++ b/design/models/authoring-surface.md @@ -140,87 +140,11 @@ construction. **Cons:** the existing format mixes four mini-dialects params, `<>` for type args). Formalising it crisply is harder than designing a uniform form from scratch. -## Form (B) — human prose projection +The chosen form is (A), shipped as the `ailang-surface` crate (see +[authoring surface](../contracts/authoring-surface.md)); the +canonical JSON-AST it round-trips against is documented in +[Data model](../contracts/data-model.md), and the round-trip +property itself in [Roundtrip Invariant](../contracts/roundtrip-invariant.md). -AILang ships a -second textual projection of the AST: `ailang-prose`, a one-way -projection from `Module → human-readable text`. It is **not** an -authoring surface; it is the "display" projection that Decision 6's -architectural pin (line 167–176) explicitly anticipated: - -> *"Future projections are explicitly anticipated: a visual / -> graphical front-end is a plausible second projection for human -> review and inspection (display being the one case where non-AI -> eyes matter). The architecture leaves room: any producer of -> well-formed `ailang-core::ast::Module` values is a valid -> front-end."* - -Form (B) targets the specific failure mode where a human reviewer -needs to read an AILang module quickly. Form (A) was designed to -fit a 30-production EBNF spec and to be parsed zero-shot by foreign -LLMs; that prioritisation makes it dense and visually noisy for -human readers. Form (B) inverts the trade-offs: - -- **Rust-flavoured surface.** Braces and `=>` for match arms, - Rust-aligned 4-level operator precedence, infix arithmetic - (`a + b`, not `+(a, b)`), unary `!` for `not`. -- **Lossy by design.** Projection elides machinery the LLM can - re-derive: `(con T)` wrappers (`(con Int)` → `Int`), the - `(fn-type (params ...) (ret ...))` wrap, `(term-ctor T C ...)` - collapses to `C(...)`, redundant parens. Only the AST machinery - whose information is recoverable from typecheck context. -- **Lossless on load-bearing detail.** Mode annotations - (`own T`, `borrow T`), effects (`with IO`), explicit `clone`, - `reuse-as`, doc strings, type annotations on signatures and - lambdas, the `tail` flag — all preserved verbatim. - -Critically, **form (B) has no parser**. Form (A) is round-trippable -by construction (Decision 6 constraint 2); form (B) deliberately is -not. Re-integrating prose edits requires an external LLM mediator, -not a compiler pass — the prompt template `ail merge-prose` -composes the six-step cycle. - -Form (B) does not weaken any Decision 6 invariant: - -- The JSON-AST remains the only hashable artefact. Prose is not - hashed, not content-addressed, not load-bearing for any - cross-module reference. -- Form (A) remains the canonical authoring surface. Foreign LLMs - still author against form (A); humans review and edit through - form (B). -- The 30-production grammar of form (A) is unchanged. -- `ailang-check` and `ailang-codegen` remain projection-agnostic; - `ailang-prose` is a downstream consumer of `ailang-core::ast`, - parallel to `ailang-surface` but in the rendering direction only. - -The CLI gains `ail prose ` (the deterministic -projection) and `ail merge-prose ` -(the mediator-prompt composer); both are listed in the CLI section -below. - -**Form-A spec embedding.** An earlier `merge-prose` -prompt instructed the LLM to emit JSON-AST and offered a 12-line -schema-essentials reminder; that combination did not give a -foreign LLM enough to produce valid output. The current prompt revises this: - -- The LLM emits **Form-A** (the canonical authoring surface), not - JSON. JSON-AST stays the only hashable artefact, but it is not - a writing surface. The user runs `ail parse foo.new.ail` - before `ail check` to produce the canonical JSON. -- `crates/ailang-core/specs/form_a.md` is the complete LLM-targeted - Form-A specification — grammar, every term / pattern / type / - def keyword, schema invariants, pitfall catalogue, four - few-shot modules drawn from `examples/*.ail`. It is exported - as `ailang_core::FORM_A_SPEC` and embedded verbatim in every - `merge-prose` prompt. -- `crates/ailang-core/tests/spec_drift.rs` walks every variant of - `Term`, `Pattern`, `Type`, `Def`, `Literal` via exhaustive - `match` and asserts an anchor for each appears in the spec. - The exhaustive match is the load-bearing piece: adding a new - variant without updating the match fails compilation in this - test, before its assertions even run. Hand-written content, - mechanical drift detection. - -The cycle's lowest-common-denominator path is the static prompt -(`ail merge-prose | client | ail parse | ail check`), which works -with any client. +For the prose projection used for human review (Form B), see +[prose projection](prose-projection.md). diff --git a/design/models/effects.md b/design/models/effects.md index 631758e..35613ff 100644 --- a/design/models/effects.md +++ b/design/models/effects.md @@ -6,7 +6,10 @@ The default is total, pure functions. Effects are declared as a set in the function type: `(Int) -> Int ![IO]`. The effect set is a flat, unordered, closed set of effect names, unified by set-equality — there is no effect row variable; a signature lists exactly the effects -its body may perform. +its body may perform. The schema-level effect-set field on `Type::Fn` +is documented in [Data model](../contracts/data-model.md); what is +currently in scope vs. excluded lives in +[scope boundaries](../contracts/scope-boundaries.md). In the MVP only the effect `IO` is wired up (its sole op is `io/print_str`). `Diverge` (for non-termination) is reserved as an effect name but is unimplemented — no op, no codegen, no checker injection — in the same diff --git a/design/models/pipeline.md b/design/models/pipeline.md index e5f4dfc..6aa4946 100644 --- a/design/models/pipeline.md +++ b/design/models/pipeline.md @@ -17,18 +17,20 @@ ``` Two allocator backends share the same MIR. `--alloc=rc` is the -canonical backend committed to in Decision 10 and the CLI default. +canonical backend committed to in the +[memory model](../contracts/memory-model.md) and the CLI default. The typechecker enforces `(own)` / `(borrow)` modes, codegen emits `ailang_rc_inc` / `_dec` calls at the points dictated by linearity, and `Term::Clone` / `Term::ReuseAs` materialise into actual rc-bumps and in-place rewrites respectively. `--alloc=gc` selects the transitional Boehm -backend; `--alloc=rc` is the canonical backend (Decision 10) and the -CLI default. +backend (see [RC + uniqueness](rc-uniqueness.md)); +`--alloc=rc` is the canonical backend and the CLI default. -The **desugar** pass (`ailang-core::desugar::desugar_module`) runs -before typecheck and codegen in every entry point of `ailang-check` -and `ailang-codegen`. It is a pure AST → AST rewriter — currently +The **desugar** pass +([`ailang-core::desugar::desugar_module`](../../crates/ailang-core/src/desugar.rs)) +runs before typecheck and codegen in every entry point of +`ailang-check` and `ailang-codegen`. It is a pure AST → AST rewriter — currently only flattens nested constructor patterns, but is the chosen home for any future surface-smoothing rewrites that should not bloat the core AST or the backends. **Critical invariant:** `CheckedModule.symbols` @@ -69,3 +71,10 @@ ail emit-ir [--emit=staticlib] — writes .ll (staticlib: a main-fre ail build [--emit=staticlib] — full pipeline → binary (staticlib: lib.a + libailang_rt.a) ail run — build + execute (tempdir), passthrough exit code ``` + +The text projections the CLI moves between are documented in +[authoring surface](../contracts/authoring-surface.md) (Form-A, +round-trippable) and [prose projection](prose-projection.md) +(Form-B, lossy, no parser); `ail build --emit=staticlib` produces +the layout fixed in [embedding ABI](../contracts/embedding-abi.md) +plus [frozen value layout](../contracts/frozen-value-layout.md). diff --git a/design/models/prose-projection.md b/design/models/prose-projection.md new file mode 100644 index 0000000..cbf3413 --- /dev/null +++ b/design/models/prose-projection.md @@ -0,0 +1,89 @@ +# Form (B) — prose projection whitepaper + +## Form (B) — human prose projection + +AILang ships a +second textual projection of the AST: `ailang-prose`, a one-way +projection from `Module → human-readable text`. It is **not** an +authoring surface; it is the "display" projection that Decision 6's +architectural pin (see [authoring surface](../contracts/authoring-surface.md)) +explicitly anticipated: + +> *"Future projections are explicitly anticipated: a visual / +> graphical front-end is a plausible second projection for human +> review and inspection (display being the one case where non-AI +> eyes matter). The architecture leaves room: any producer of +> well-formed `ailang-core::ast::Module` values is a valid +> front-end."* + +Form (B) targets the specific failure mode where a human reviewer +needs to read an AILang module quickly. Form (A) was designed to +fit a 30-production EBNF spec and to be parsed zero-shot by foreign +LLMs; that prioritisation makes it dense and visually noisy for +human readers. Form (B) inverts the trade-offs: + +- **Rust-flavoured surface.** Braces and `=>` for match arms, + Rust-aligned 4-level operator precedence, infix arithmetic + (`a + b`, not `+(a, b)`), unary `!` for `not`. +- **Lossy by design.** Projection elides machinery the LLM can + re-derive: `(con T)` wrappers (`(con Int)` → `Int`), the + `(fn-type (params ...) (ret ...))` wrap, `(term-ctor T C ...)` + collapses to `C(...)`, redundant parens. Only the AST machinery + whose information is recoverable from typecheck context. +- **Lossless on load-bearing detail.** Mode annotations + (`own T`, `borrow T`), effects (`with IO`), explicit `clone`, + `reuse-as`, doc strings, type annotations on signatures and + lambdas, the `tail` flag — all preserved verbatim. + +Critically, **form (B) has no parser**. Form (A) is round-trippable +by construction (see [roundtrip invariant](../contracts/roundtrip-invariant.md)); +form (B) deliberately is not. Re-integrating prose edits requires an +external LLM mediator, not a compiler pass — the prompt template +`ail merge-prose` composes the six-step cycle. + +Form (B) does not weaken any Decision 6 invariant: + +- The [JSON-AST](../contracts/data-model.md) remains the only + hashable artefact. Prose is not hashed, not content-addressed, + not load-bearing for any cross-module reference. +- Form (A) remains the canonical authoring surface. Foreign LLMs + still author against form (A); humans review and edit through + form (B). +- The 30-production grammar of form (A) is unchanged. +- `ailang-check` and `ailang-codegen` remain projection-agnostic; + `ailang-prose` is a downstream consumer of `ailang-core::ast`, + parallel to `ailang-surface` but in the rendering direction only. + +The CLI gains `ail prose ` (the deterministic +projection) and `ail merge-prose ` +(the mediator-prompt composer); both are listed under +[pipeline](pipeline.md). + +## Form-A spec embedding + +An earlier `merge-prose` +prompt instructed the LLM to emit JSON-AST and offered a 12-line +schema-essentials reminder; that combination did not give a +foreign LLM enough to produce valid output. The current prompt revises this: + +- The LLM emits **Form-A** (the canonical authoring surface), not + JSON. JSON-AST stays the only hashable artefact, but it is not + a writing surface. The user runs `ail parse foo.new.ail` + before `ail check` to produce the canonical JSON. +- `crates/ailang-core/specs/form_a.md` is the complete LLM-targeted + Form-A specification — grammar, every term / pattern / type / + def keyword, schema invariants, pitfall catalogue, four + few-shot modules drawn from `examples/*.ail`. It is exported + as `ailang_core::FORM_A_SPEC` and embedded verbatim in every + `merge-prose` prompt. +- `crates/ailang-core/tests/spec_drift.rs` walks every variant of + `Term`, `Pattern`, `Type`, `Def`, `Literal` via exhaustive + `match` and asserts an anchor for each appears in the spec. + The exhaustive match is the load-bearing piece: adding a new + variant without updating the match fails compilation in this + test, before its assertions even run. Hand-written content, + mechanical drift detection. + +The cycle's lowest-common-denominator path is the static prompt +(`ail merge-prose | client | ail parse | ail check`), which works +with any client. diff --git a/design/models/rc-uniqueness.md b/design/models/rc-uniqueness.md index b82a3eb..20401d7 100644 --- a/design/models/rc-uniqueness.md +++ b/design/models/rc-uniqueness.md @@ -5,7 +5,8 @@ AILang ships two allocator backends with an asymmetric role: - **RC is canonical.** `--alloc=rc` is the CLI default for - `ail build` and `ail run`. The runtime AILang's memory model + `ail build` and `ail run` (see [pipeline](pipeline.md)). The + runtime AILang's [memory model](../contracts/memory-model.md) (RC + uniqueness inference) is designed for. New examples, benches, and corpus tests run under RC unless they explicitly pin GC. @@ -25,8 +26,11 @@ few iter families ship without the gc arm catching anything that the rc arm did not already catch. Until then, the cost of keeping libgc as a build dependency is accepted in exchange for diagnostic leverage. Decision 10 (RC + uniqueness) holds as the -specification of the canonical runtime; the rest of this section -documents the Boehm half, retained as the oracle. +specification of the canonical runtime (the contract version is +[memory model](../contracts/memory-model.md), built on +[language constraints](../contracts/language-constraints.md)); +the rest of this section documents the Boehm half, retained as +the oracle. **Choice: Boehm-Demers-Weiser conservative GC.** The simplest working option: @@ -143,10 +147,10 @@ costs are bounded and analysable per program point. A corpus committed to one memory model is expensive to switch — pre- stdlib is the cheapest moment to commit. -**Choice.** AILang's canonical memory model is reference counting -with static uniqueness inference **and explicit LLM-author -annotations on fn signatures**, in the lineage of Lean 4 / Roc / -Koka. Boehm becomes a transitional allocator (Decision 9) and is +**Choice.** AILang's canonical [memory model](../contracts/memory-model.md) +is reference counting with static uniqueness inference **and +explicit LLM-author annotations on fn signatures**, in the lineage +of Lean 4 / Roc / Koka. Boehm becomes a transitional allocator (Decision 9) and is retired when the RC pipeline matches the bump-allocator floor within an acceptable margin (target 1.3× on `bench/run.sh`). @@ -225,7 +229,9 @@ can carry the cognitive cost trivially, and the compiler gains a precise contract at every call site instead of a probabilistic guess. -**(2) Linear-by-default consumption with explicit `(clone X)`.** +**(2) Linear-by-default consumption with explicit `(clone X)`** +(the `Term::Clone` schema entry lives in +[Data model](../contracts/data-model.md)). In bodies, every binder is consumed by exactly one `own`-mode use. If the LLM writes: @@ -300,8 +306,8 @@ compiles, but what the compiler tells the author when it doesn't. ## Inference algorithm -Post-typecheck, post-`lift_letrecs`, pre-codegen pass over the -elaborated module. For each `Term` node that produces or binds a +Post-typecheck, post-`lift_letrecs` (see [pipeline](pipeline.md)), +pre-codegen pass over the elaborated module. For each `Term` node that produces or binds a boxed value, the pass computes a uniqueness flag: - **Unique:** at this program point, the reference is the only diff --git a/design/models/typeclasses.md b/design/models/typeclasses.md index 939f7d4..f8ac9bc 100644 --- a/design/models/typeclasses.md +++ b/design/models/typeclasses.md @@ -1,10 +1,19 @@ # Typeclasses — resolution and monomorphisation whitepaper +The schema-and-diagnostics contract for typeclasses lives in +[typeclasses](../contracts/typeclasses.md); the call-site lookup +rule in [method dispatch](../contracts/method-dispatch.md); the +built-in classes shipped in the prelude in +[prelude classes](../contracts/prelude-classes.md). This file +covers the design choices and the resolution / monomorphisation +algorithm. + ## Decision 11: typeclasses — Haskell-lite, monomorphised, coherent -**The design pass for typeclasses. Codified after the Feature-acceptance -criterion (this document, above) was committed; the criterion is -the explicit basis for the choices below.** +**The design pass for typeclasses. Codified after the +[Feature-acceptance criterion](../contracts/feature-acceptance.md) +was committed; the criterion is the explicit basis for the choices +below.** AILang ships typeclasses to compress a real LLM-author redundancy: without them, every comparable function must be written per-type @@ -46,17 +55,19 @@ types) is one an LLM author does not unprompted produce. **Constraint collection (per function body).** During typechecking of a body, each method call generates a residual constraint of shape -` ` where `` may still contain type variables. +` ` (the schema for these lives in +[Data model](../contracts/data-model.md)) where `` may still +contain type variables. After local typechecking, residual constraints are checked against the function's declared constraints (modulo α-conversion and modulo auto-expansion through superclasses; see below). Any residual not covered by declared constraints fires `MissingConstraint`. **Instance registry (workspace-global).** At workspace load (see -`crates/ailang-core/src/workspace.rs`), all `InstanceDef` nodes -across all reachable modules are collected into a registry keyed by -`(class-name, canonical-hash-of-instance-type)`. Registry build -performs three checks: +[`crates/ailang-core/src/workspace.rs`](../../crates/ailang-core/src/workspace.rs)), +all `InstanceDef` nodes across all reachable modules are collected +into a registry keyed by `(class-name, canonical-hash-of-instance-type)`. +Registry build performs three checks: - **Coherence.** Each instance's module must be either the class's defining module or the instance type's defining module. Otherwise