diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 95465c1..7d28a87 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1446,6 +1446,318 @@ materialises with a real workload. - **Does not introduce regions.** Regions were considered and rejected; see "Why not other memory models" above. +## Decision 11: typeclasses — Haskell-lite, monomorphised, coherent + +**Committed 2026-05-09 (Iter 22a), as the design pass that gates +22b implementer work. Codified after the Feature-acceptance +criterion (this document, above) 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 +(`int_eq`, `string_eq`, `bool_eq`, `int_show`, `string_show`, …). With +typeclasses behind a monomorphising compiler, the LLM author writes +one signature with a class constraint and one method per concrete +type, and the compiler emits the same machine code as the per-type +version. No runtime cost, no dictionary passing, no vtables. + +**Choice.** A deliberately narrow typeclass design — narrower than +Haskell, narrower than Rust traits — calibrated to what an LLM +author naturally produces. Five semantic axes are committed: + +1. **Scope.** Multi-method, single-parameter, optional defaults, + single-superclass relation. No multi-param classes, no + functional dependencies, no associated types. +2. **Constraints in signatures.** Explicit and mandatory. A + function that calls a class method must declare the constraint + in its `forall` block. No constraint inference. +3. **Resolution.** Orphan-free coherence. An `instance C T` may be + declared only in the module of `C` or in the module of `T`. + Resolution is global type-directed against a workspace-built + registry; coherence makes the lookup unambiguous. +4. **Defaults.** Opt-in via an explicit `default` keyword in the + class body. Methods without `default` are abstract-required; + methods with `default` may be overridden or inherited per + instance. +5. **Class-parameter kind.** Concrete types only (kind `*`). No + higher-kinded class params; `Functor`/`Monad`-style abstractions + over type constructors are not expressible. The LLM-natural + pattern is `List.map` / `Tree.map` as separate functions per + type, which monomorphisation handles directly. + +The five axes follow from the Feature-acceptance criterion: each +rejected mechanism (multi-param, higher-kinded, FunDeps, assoc +types) is one an LLM author does not unprompted produce. + +### Form-A schema (the JSON authoring surface) + +Three additive schema extensions; no existing module becomes invalid. + +**`ClassDef`** — top-level definition kind, declares a class: + +``` +{ "kind": "ClassDef", + "name": "Show", + "param": "a", + "superclass": null, + "methods": [ + { "name": "show", + "type": { /* full FnSig over `a`, with mode annotations */ }, + "default": null + } + ] +} +``` + +`superclass` is either `null` or `{ "class": , "type": "a" }` +where `"a"` MUST be the same identifier as the class's own `param`. +`default` is either `null` (method is abstract-required at instance +sites) or an AST body (method is optional with the body as fallback). + +**`InstanceDef`** — top-level definition kind, declares an instance: + +``` +{ "kind": "InstanceDef", + "class": "Show", + "type": "Int", + "methods": [ + { "name": "show", "body": } + ] +} +``` + +`type` is a concrete type expression, never the class param. `methods` +contains the bodies for every required method plus optional overrides +of default-bearing methods. + +**`FnDef.type` extension** — the existing FnSig schema gains a +`constraints` sibling field next to `forall`: + +``` +"type": { + "forall": ["a"], + "constraints": [{ "class": "Show", "type": "a" }], + "type": ["Fn", [...], "String"] +} +``` + +When `forall` is empty, `constraints` is also empty (and may be +omitted for hash stability of pre-22a definitions). Each constraint's +`type` field MUST reference a type variable bound by the surrounding +`forall`. + +**Method invocation sites do NOT get a new node.** A call to a class +method is a normal `Call` node; resolution against a class is the +typechecker's job, not the parser's. The LLM author writes `show x` +exactly as for any free function. + +### Resolution and monomorphisation + +**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. +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: + +- **Coherence.** Each instance's module must be either the class's + defining module or the instance type's defining module. Otherwise + → `OrphanInstance`. +- **Uniqueness.** No two entries share a key. Otherwise → + `DuplicateInstance`. +- **Method completeness.** Each instance specifies every required + (non-default) method of its class. Otherwise → `MissingMethod`. + +Registry build is a one-time-per-build pass that fires before any +typechecking. Its errors are workspace-load errors, not per-call-site +errors. + +**Resolution at call sites with concrete types.** When the typechecker +sees a method call where every type variable in the constraint is +substituted to a concrete type, it queries the registry. Hit → +resolved. Miss → `NoInstance`. + +**Resolution at polymorphic call sites.** When type variables are +still free, the constraint propagates into the surrounding function's +constraint context — which the user MUST have declared explicitly +(per axis 2). No constraint is implicitly hoisted. + +**Monomorphisation (post-typecheck, pre-codegen).** A pass between +typechecking and codegen replaces every resolved class-method call +with a call to a synthesised monomorphic `FnDef`. For each unique +`(method, concrete-type)` pair encountered, the pass: + +1. Synthesises a top-level `FnDef` named deterministically from the + method name and the canonical hash of the instance type. Body is + the resolved instance method (or default body), with the class + parameter substituted to the concrete type. +2. Caches the synthesised def by `(method, type-hash)` so the same + pair is not emitted twice. +3. Rewrites the original `Call` to target the synthesised name. + +After this pass, the IR contains no class machinery — only ordinary +monomorphic functions and direct calls. Codegen sees no difference +between a hand-written `show_int` and a synthesised `show@Int`. + +**No runtime dispatch, no dictionary passing.** The monomorphisation +pass is the ONLY mechanism for class-method calls. A call that +cannot be monomorphised — for instance, because a constraint remains +unresolved at the entry point — is a static error, not a runtime one. +This is the LLVM-friendly form and is consistent with Decision 10's +performance commitment. + +### Defaults and superclasses + +**Defaults.** A `ClassDef.methods[i].default` is either `null` (the +method is required at instance level) or an AST body. When an +`InstanceDef` does not specify a method that has a default, the +typechecker uses the default body for that instance, with the class +param substituted to the instance type. Default bodies may call +other methods of the same class (the canonical example is +`default ne x y = not (eq x y)`); the called methods resolve at +monomorphisation time against the same instance. + +**Superclasses.** A `ClassDef.superclass` of `{ "class": "Eq", +"type": "a" }` declares that any `instance C T` requires a +corresponding `instance Eq T` to exist. The check fires at +workspace-load time: for each `InstanceDef` whose class declares a +superclass, the registry is queried for the matching superclass +instance. Missing → `MissingSuperclassInstance`. + +**Superclass auto-expansion in constraint contexts.** When a function +declares `Ord a` as a constraint, the typechecker treats the constraint +context as `{ Ord a, Eq a }` for the purposes of `MissingConstraint` +checking. This is the one deviation from "alles sichtbar": the +extension is anchored in the class's own `superclass` field, so the +relation is schema-visible at the class declaration even when the +constraint at the function site reads `Ord a` alone. + +Superclass chains are linear (single-superclass relation per class) +and auto-expansion closes transitively across the chain. + +**No `deriving`.** 22a does not auto-derive instances. `instance Eq +MyType` must be written by hand. Auto-derivation may land in a future +iteration if the Feature-acceptance criterion holds for it; that +discussion is out of scope here. + +### Diagnostic categories + +The typeclass layer introduces three families of diagnostics. Exact +wording is fixed in 22b; the categories and their triggers are: + +**Workspace-load (registry-build) diagnostics:** + +- `OrphanInstance` — instance is not in class's or type's module. +- `DuplicateInstance` — two instances match the same key. +- `MissingSuperclassInstance` — superclass instance absent. +- `MissingMethod` — instance omits a required method. +- `OverridingNonExistentMethod` — instance specifies a method not in + the class. +- `MethodNameCollision` — same method name across two in-scope + classes, or between a class method and a top-level function. + +**Class-schema diagnostics** (validation of class declarations): + +- `KindMismatch` — class param appears in applied position in any + method signature (e.g., `f a` where `f` is the class param). +- `InvalidSuperclassParam` — superclass `type` differs from the + class's own `param`. +- `ConstraintReferencesUnboundTypeVar` — a constraint mentions a + type variable not bound by the surrounding `forall`. + +**Typecheck diagnostics** (per function body): + +- `MissingConstraint` — body's residual constraint is not covered + by declared (and superclass-expanded) constraints. +- `NoInstance` — fully concrete constraint has no registry entry. + +There is no `AmbiguousInstance` diagnostic. Coherence (W2) makes +every `(class, type)` key globally unique; resolution is therefore +deterministic by construction. + +### What 22a explicitly does NOT support + +Each of the following is rejected by either schema (parser cannot +express the construct) or by an enumerated diagnostic. The +combination of axis-1 (single-param, no FunDeps, no assoc) and +axis-5 (kind `*` only) covers the space. + +- **Multi-parameter classes** (`class Foo a b where ...`). Schema + rejects: `ClassDef.param` is a string, not a list. +- **Higher-kinded class params** (`class Functor f`). Diagnostic + S1 (`KindMismatch`) at class declaration if any method applies + the param. +- **Higher-rank polymorphism** (`forall a. (forall b. b -> b) -> a`). + Already rejected at parse time per the typeclass-conversation + rationale recorded in JOURNAL 2026-05-09; constraint-bearing + signatures inherit that prohibition. +- **Existential / dyn dispatch** (`exists a. Show a => a`, + heterogeneous lists like `[Show]`). Schema does not express + existentials. The LLM-natural alternative is sum types. +- **Associated types** (`class Container c where type Element c`). + Schema does not express type-level methods. +- **Functional dependencies** (`class Convert a b | a -> b`). Required + only for multi-param classes; entails by axis 1. +- **`deriving` / auto-derivation** (`data Foo = ... deriving (Eq)`). + Future iteration, gated separately on Feature-acceptance. +- **Numeric literal defaulting.** `1` does not auto-resolve to `Int` + under an ambiguous `Num a` constraint. Bare polymorphic literals + with multiple satisfying instances fire `NoInstance` with a hint + to annotate. The LLM-author writes `1 : Int` or `1 : Float`. +- **Orphan-with-warning mode.** Coherence is hard. `OrphanInstance` + is always an error, never a warning. The corollary `--allow-orphans` + flag is not provided. + +### Prelude (built-in) classes + +22a/22b ship a fixed Prelude consisting of three classes: **`Show`, +`Eq`, `Ord`**, with instances for the four primitive types `Int`, +`Float`, `Bool`, `String`. `Ord` declares `Eq` as its superclass. + +`print x` is rewired through `Show.show`: at codegen, the existing +print primitive routes its argument through the resolved `show@T`. +This is the one operator-routing change in 22b. + +`==`, `<`, `<=`, `>`, `>=` REMAIN primitive operators. Class methods +are accessed by name (`eq x y`, `lt x y`, …), not via these operators. +Routing operators through classes is deliberately deferred — it would +require migrating every existing fixture and would risk firing the +bench gate. A future iteration may add operator routing once the +typeclass layer has settled and the bench corpus is stable. + +`Num` is NOT in the 22a/22b Prelude. Arithmetic operators (`+`, `-`, +`*`, `/`) stay primitive and per-type. The LLM-natural pattern of +distinct `Int` and `Float` arithmetic is preserved; class-based +numeric overloading would invoke literal-defaulting which axis-7 +already excluded. + +### What this decision does NOT commit to + +- **Operator routing.** `==`, `<`, etc. stay primitive in 22a/22b. + Class-routing operators is a future-iteration option, not a + Decision-11 commitment. +- **Form-B (prose) projection of class/instance.** The prose + renderer for the new schema nodes is 22b implementer scope; the + form is not pinned in 22a. +- **Specific monomorphised-symbol naming format.** The naming is + deterministic from `(method, type-hash)`; the exact textual form + is fixed in 22b alongside the existing mangling scheme. +- **Mode annotations on class methods.** Class method signatures + ARE full FnSigs and DO carry mode annotations per Decision 10; + the convention for default modes (typically `borrow` for + read-only methods like `show`, `eq`) is settled in 22b. +- **Number of Prelude classes.** Three classes (Show, Eq, Ord) is + the 22b commitment. Adding `Num`, `Functor`-substitutes + (per-type), or domain-specific classes is gated on the Feature- + acceptance criterion at the time of proposal. + ## Mangling scheme (Iter 5c) All AILang functions are mangled to `@ail__` — even in the diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 9de1172..bc9ef39 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -10865,3 +10865,133 @@ directly: DESIGN.md typeclass section, instantiation strategy, schema nodes for `class` and `instance`, naming convention for monomorphised functions. Implementer iter (22b) follows after 22a's design lands and is reviewed. + +## 2026-05-09 — 22a: typeclass design + +Trigger: 22a is the typeclass design iter queued in the previous +JOURNAL entry. Per CLAUDE.md, design iters are orchestrator work +done directly. This entry records the decisions and the reasoning; +the canonical specification lives in `docs/DESIGN.md` as Decision 11. + +The Feature-acceptance criterion (codified earlier the same day) +was applied as the primary gate. Each of the five committed +semantic axes traces to a single question: "would an LLM author +unprompted produce code that uses this mechanism, AND does the +mechanism measurably remove redundancy or improve correctness?" +Where the answer was no, the mechanism was rejected. + +### Five committed axes + +1. **Haskell-lite scope** (multi-method, single-param, optional + defaults, single-superclass). Multi-param classes were rejected + because LLM authors do not produce them unprompted, and because + they would require functional dependencies for tractable + resolution. Full Haskell scope (assoc types, GADTs-style + constraints) was rejected on the same grounds. + +2. **Constraints in signatures: explicit and mandatory.** Constraint + inference was rejected for the same reason mandatory mode + annotations are mandatory (Decision 10): explicit annotation + makes every commitment visible at the function boundary, so + reading a signature requires no body-level reasoning. The "alles + sichtbar" line of the project is preserved at this layer. + +3. **Resolution: orphan-free coherence.** Modeled on Rust's coherence + rule rather than Haskell's orphan-with-warning. The hard rule + makes registry resolution unambiguous by construction; no + `AmbiguousInstance` diagnostic exists. The trade — reduced + flexibility for third-party instance authors — is acceptable + because AILang's authoring surface is a single workspace, not + an open package ecosystem. + +4. **Defaults via explicit `default` keyword.** Haskell's + convention of mixing default and required methods in the class + body without syntactic distinction was rejected on visibility + grounds. The `default` keyword makes "what must this instance + implement" answerable from the class header alone. Same line + as axis 2. + +5. **Class-parameter kind: `*` only.** Higher-kinded class params + were rejected because the abstraction they enable (`Functor`, + `Monad`, `Applicative`) is not what an LLM author produces + unprompted. The natural LLM pattern is `List.map`, `Tree.map`, + `Option.map` as separate functions per type, which + monomorphisation handles directly without class machinery. The + kind-`*` restriction also removes the implementation cost of + higher-kinded constraint resolution. + +### Prelude scope + +Three classes ship in the 22b Prelude: `Show`, `Eq`, `Ord`, with +instances for the four primitive types (`Int`, `Float`, `Bool`, +`String`). `Ord` declares `Eq` as superclass. + +`print x` is rewired through `Show.show` at codegen — the one +operator-routing change in 22b. + +`==`, `<`, `<=`, `>`, `>=` stay primitive operators. Routing them +through `Eq`/`Ord` would require migrating every existing fixture +and would risk firing the bench gate during a feature iter. +Operator routing is deliberately deferred to a later iter, gated +on bench-stability. + +`Num` is NOT in the Prelude. Arithmetic operators stay primitive +and per-type. The LLM-natural pattern of distinct `Int` and +`Float` arithmetic is preserved. + +### What 22a does not commit to + +- The exact textual form of monomorphised-symbol names (e.g. + `show@Int` vs. `show#Int` vs. a hash-suffixed scheme). Naming + is deterministic from `(method, type-hash)`; the textual form + is fixed in 22b alongside the existing mangling scheme + (DESIGN.md §"Mangling scheme"). +- The Form-B (prose) projection of `ClassDef` and `InstanceDef`. + Prose-projector arms for the new nodes are 22b scope. +- Mode-annotation defaults for class methods. Class method + signatures are full FnSigs and carry mode annotations per + Decision 10; conventions (likely `borrow` for read-only methods + like `show`, `eq`, `lt`) settle in 22b. +- Auto-derivation of instances. `deriving` is a future-iter option, + gated on Feature-acceptance at proposal time. + +### Why this iter is design-only + +Per CLAUDE.md and the previous JOURNAL queue entry, 22a is design. +No Rust crates change in this iter; no schema-floor commit; no +bench corpus change. The iter ships a single edit to +`docs/DESIGN.md` (Decision 11 added between Decision 10 and the +Mangling-scheme section) and this JOURNAL entry. The schema and +implementation land in 22b. + +### Test state + +288 / 0 / 3, unchanged. Documentation-only. + +### Bench gates + +Not re-run. No runtime, codegen, or check-time path is touched. + +### JOURNAL queue (updated) + +- **22b — typeclass implementer.** Schema floor for `ClassDef`, + `InstanceDef`, `FnDef.type.constraints`. Workspace-load + registry build with the three coherence/uniqueness/completeness + checks. Class-schema validation (`KindMismatch`, + `InvalidSuperclassParam`, `ConstraintReferencesUnboundTypeVar`). + Typecheck arms for `MissingConstraint` and `NoInstance`. + Monomorphisation pass + naming convention. Prelude module with + `Show`/`Eq`/`Ord` and the four primitive instances. `print` + rewiring through `Show.show`. End-to-end fixture exercising + the full path. Bench gate at close. +- **22c — typeclass corpus expansion (deferred).** User-defined + classes/instances exercised by an example beyond the Prelude. + Optional `deriving` shorthand if Feature-acceptance gate passes. +- **Operator routing through Eq/Ord (deferred, no commitment).** + Migrating `==`, `<`, etc. to class methods. Big-bang fixture + refactor; gated on bench-stability and on a clear LLM-author + benefit ("less ceremony" alone is not a benefit; needs a + redundancy-removal claim). +- **21'h, latency methodology, FnDef::synthetic, Boehm full + retirement, closure-pair slab/pool, deferred richer integration + paths.** Unchanged from 21'g.