design: 22a — Decision 11 typeclasses (Haskell-lite, monomorphised, coherent)

2026-05-09 12:16:48 +02:00
parent 30e9b117cb
commit f6cb900082
2 changed files with 442 additions and 0 deletions
@@ -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": <name>, "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": <AST> }
+  ]
+}
+```
+
+`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
+`<Class> <Type>` where `<Type>` 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_<module>_<def>` — even in the
@@ -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.