The first formal-links milestone shipped clause-5 + 8 links across the
existing file layout. Browsing surfaced that file-only granularity is
only as precise as the file boundaries — three files mixed two or
three navigation targets under one address, so the 8 links could not
multiply without ambiguity. This commit fixes the substrate, then
applies the sweep the original milestone deferred.
Splits (each extracts an already-self-contained section into its own
file so links land on the topic, not the parent doc's TOC):
contracts/typeclasses.md
→ +contracts/prelude-classes.md (Eq/Ord/Show ships, polymorphic `print`)
→ +contracts/method-dispatch.md (5-step dispatch rule, candidate index)
contracts/memory-model.md
→ +contracts/language-constraints.md (the 4 binding constraints
making RC sound without a
cycle collector)
models/authoring-surface.md
→ +models/prose-projection.md (Form-B / `ail prose` / merge-prose)
Each new file enters design/INDEX.md as its own row (three contracts
share show_no_instance_e2e.rs / uniqueness.rs as ratifying tests;
prose-projection is a model). Two pre-existing links rebind to the
new topic-files (memory-model.md → method-dispatch.md;
float-semantics.md → prelude-classes.md).
Link sweep: 8 → 88 formal Markdown links over 23 files. Every file
in design/contracts/ + design/models/ now has at least one outgoing
link; the tree is fully connected. Links are file-relative
`[label](path)` per the established convention, fenced code blocks
are skipped (a `](` inside ```jsonc``` is literal text), the durable
tier (design/ + crates/ + runtime/) is enforced by clause-5.
Tests:
- design_index_pin.rs (5/5 clauses): clean-cut, INDEX resolution,
ratifying-test resolution, no decision-record prose in contracts/,
body links durable + resolving.
- docs_honesty_pin.rs (5/5): one assertion rebinds from typeclasses.md
to prelude-classes.md (where the gated sentence now lives);
design_corpus widens to include the 4 new files so the Wunschdenken
/ doc-archaeology sweeps continue to cover everything that used to
live in the parents.
No spec/plan/journal for this batch — interactive collaboration after
the milestone closed; the user gated the splits explicitly before the
sweep.
8.3 KiB
Typeclasses — resolution and monomorphisation whitepaper
The schema-and-diagnostics contract for typeclasses lives in typeclasses; the call-site lookup rule in method dispatch; the built-in classes shipped in the prelude in prelude classes. 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 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:
- Scope. Multi-method, single-parameter, optional defaults, single-superclass relation. No multi-param classes, no functional dependencies, no associated types.
- Constraints in signatures. Explicit and mandatory. A
function that calls a class method must declare the constraint
in its
forallblock. No constraint inference. - Resolution. Orphan-free coherence. An
instance C Tmay be declared only in the module ofCor in the module ofT. Resolution is global type-directed against a workspace-built registry; coherence makes the lookup unambiguous. - Defaults. Opt-in via an explicit
defaultkeyword in the class body. Methods withoutdefaultare abstract-required; methods withdefaultmay be overridden or inherited per instance. - 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 isList.map/Tree.mapas 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.
Resolution and monomorphisation
Constraint collection (per function body). During typechecking
of a body, each method call generates a residual constraint of shape
<Class> <Type> (the schema for these lives in
Data model) 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 call to a
Type::Forall-quantified Def::Fn with a call to a synthesised
monomorphic FnDef. Two source-body entry points share the same
mechanics in one fixpoint:
- Class-method entry. For each unique
(method, concrete-type)pair produced by a class-constraint residual, the pass looks up the resolved instance body viaRegistry::entries[(class, type-hash)], substitutes the class parameter to the concrete type, and synthesises a top-levelFnDefnamed<method>__<type-surface-name>. - Free-fn entry. For each call site to a polymorphic free
Def::Fnwith a fully-concrete substitution, the pass takes the source body directly from the polymorphicDef::Fn, applies rigid-var substitution on both the type AND the body (the body may contain innerTerm::Lams whoseparam_tysreference the outer Forall vars), and synthesises a top-levelFnDefnamed<name>__<type-surface-name-1>__<type-surface-name-2>__…(concatenated inType::Forall.varsdeclaration order; the N-ary case extends the single-type-var class-method shape bit-stably).
Both arms share:
- A fixpoint loop that keeps collecting targets until a round adds nothing new (a synthesised free-fn body may invoke class methods at concrete types, scheduling new class-method targets; a class-method body may invoke polymorphic free fns at concrete types, scheduling new free-fn targets).
- A dedup cache keyed by
(kind, base-name, type-hash-or-joined-hashes)where the first component ("class"/"free") guarantees disjoint keying across the two kinds. - A call-site rewrite walker that rewrites bare polymorphic call sites — class-method-named OR poly-free-fn-named — to their mono symbols before codegen runs. The walker advances a single cursor over interleaved class-method and free-fn slots emitted in synth's traversal order.
After this pass, the IR contains no polymorphism, no class
machinery, no polymorphic call sites — only ordinary monomorphic
functions and direct calls. Codegen sees no difference between a
hand-written show_int and a synthesised show__Int.
Why mono, not virtual dispatch. Monomorphisation makes the call
target visible to the optimiser, unlocking inlining and downstream
loop transformations that virtual dispatch prevents in principle.
On a saturating branch predictor with a monomorphic indirect
target, the indirect call itself is comparable in cost to a
non-inlined direct call — the win is in what the optimiser can do
with the visible target, not in the call instruction. The
end-to-end gain shrinks toward zero on larger callee bodies and
cold call sites, but the architectural claim — "mono enables
optimisations vdisp forbids" — holds across the spectrum
(bench/mono_dispatch.py and the corresponding JOURNAL bench-notes
entry record the measured ratios).
The separator is __ rather than # or @ because # and @
are invalid in LLVM IR global identifiers (the IR verifier rejects
them inside @ail_<module>_<def> mangled names). __ is legal in
both LLVM IR and the C ABI used by the runtime glue, and parses
unambiguously into <method>__<type-surface-name> because neither
component contains __ by project convention.
No runtime dispatch, no dictionary passing. The monomorphisation
pass is the ONLY specialiser. Codegen sees only monomorphic
Def::Fns and direct calls; the pre-iter-23.4 codegen-time
specialiser (lower_polymorphic_call + module_polymorphic_fns +
mono_queue) was removed in iter 23.4. 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.