Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

Iter 14a: polymorphic List a end-to-end + monomorphisation fix

Browse Source 
Dogfood payoff for parameterised ADTs (13a/b/c). Adds the first
program to nest a nullary ctor of a parameterised ADT inside a
parent ctor (Cons(Int, Nil)) and to call a polymorphic recursive
higher-order fn over a recursive parameterised ADT.

Fixture (examples/list_map_poly.ail.json):
- data List a = Nil | Cons a (List a)
- inc : (Int) -> Int = \x. x + 1
- map : forall a b. ((a) -> b, List<a>) -> List<b>
        recursive, instantiated at (Int, Int)
- print_list : (List<Int>) -> Unit !{IO}, recursive
- main builds [1,2,3], maps inc, prints each: "2", "3", "4"

E2E test list_map_poly_inc_then_prints in crates/ail/tests/e2e.rs.

Bug fixed (crates/ailang-codegen/src/lib.rs, +30/-9):
synth_arg_type used Type::unit() as placeholder for ADT type
vars that the ctor's args couldn't pin (Nil for List<a>).
Inside Cons(Int, Nil), unify_for_subst then bound a=Int from
the head and collided with a=Unit from the tail. Replaced the
placeholder with a synth-only wildcard Type::Var{name:"$u"}
mirroring the checker's $m metavar convention; unify_for_subst
short-circuits on $u-prefixed arg-side vars (accept without
binding, let a sibling pin the var).

No schema or API change. No new variant. Tester's recursion
hypothesis was refuted by debugger via a non-recursive
Cons(7, Nil) repro before the fix landed.

Tests: 25/25 e2e (was 24). All Iter 12/13 regressions green.
cargo doc --no-deps zero warnings (workspace invariant from
13d/e/f preserved).

Three-agent flow (tester -> debugger, no implementer needed
since the fix was inside debugger's <50 LOC scope). Process
note in JOURNAL.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Brummel
2026-05-07 15:32:48 +02:00
parent 1918fbee7f
commit 747b7cd05c
4 changed files with 380 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ail/tests/e2e.rs
+14
View File
@@ -93,6 +93,20 @@ fn list_map_doubles_then_prints() {
assert_eq!(lines, vec!["2", "4", "6"]);
}
/// Iter 14a: end-to-end exercise of parameterised ADTs through a
/// polymorphic higher-order fn. `data List a` plus
/// `map : forall a b. ((a) -> b, List<a>) -> List<b>` recursive,
/// instantiated at `(Int, Int)`. Guards: forall with two type vars +
/// recursive call inside its own body + ctor construction with
/// substituted field types + match-arm bindings flowing into an
/// effectful tail call.
#[test]
fn list_map_poly_inc_then_prints() {
let stdout = build_and_run("list_map_poly.ail.json");
let lines: Vec<&str> = stdout.lines().collect();
assert_eq!(lines, vec!["2", "3", "4"]);
}
/// Iter 11 dogfood: insertion sort over an 11-element IntList.
/// Exercises `<=`, `if`, mutual-leaf recursion (`insert` and `sort`),
/// nested ctor construction, and the Iter 10 seq operator inside
crates/ailang-codegen/src/lib.rs
+30 -9
View File
@@ -2076,18 +2076,27 @@ impl<'a> Emitter<'a> {
for (exp, actual) in cref.ail_fields.iter().zip(arg_tys.iter()) {
unify_for_subst(exp, actual, &var_set, &mut subst)?;
}
// Vars not pinned by ctor args (e.g. `None` for
// `Maybe a`) are filled with `Type::unit()` as a
// placeholder. That's harmless for monomorphic call
// sites — codegen never instantiates a polymorphic fn
// off this un-pinned shape because the typechecker
// would have rejected an under-determined call —
// and keeps the function total for the well-formed
// ones (e.g. `Some(7)` pins `a` from the arg).
// Vars not pinned by ctor args (e.g. `Nil` for `List a`,
// `None` for `Maybe a`) are filled with a synth-only
// wildcard `Type::Var { name: "$u" }`. The `$u`-prefix
// is reserved here (mirrors the checker's `$m` for
// metavars) and is treated as a match-anything wildcard
// by `unify_for_subst` on the arg side. This matters
// when a nullary ctor like `Nil` is nested inside a
// parent ctor whose other args pin the same type var
// concretely — e.g. `Cons(Int, Nil) : List<a>` must
// pin `a = Int` from the head and let the tail's
// unconstrained `a` defer rather than collide on
// `Type::unit()` as it would have pre-fix.
let resolved: Vec<Type> = cref
.type_vars
.iter()
.map(|v| subst.get(v).cloned().unwrap_or_else(Type::unit))
.map(|v| {
subst
.get(v)
.cloned()
.unwrap_or_else(|| Type::Var { name: "$u".into() })
})
.collect();
Ok(Type::Con {
name: type_name.clone(),
@@ -2237,6 +2246,18 @@ fn unify_for_subst(
vars: &BTreeSet<&str>,
subst: &mut BTreeMap<String, Type>,
) -> Result<()> {
// Iter 14a fix: an arg-side `$u`-prefixed var is a synth-only
// wildcard produced by `synth_arg_type` for nullary ctors of a
// parameterised ADT (e.g. `Nil : List<$u>`). It carries no real
// constraint — accept without binding so a sibling arg can pin
// the type var instead. Without this, `Cons(Int, Nil)` synth
// would unify `a = Int` (from head) and then `a = $u` (from
// tail's recursive `List<a>` slot) and falsely error.
if let Type::Var { name } = arg {
if name.starts_with("$u") {
return Ok(());
}
}
match (param, arg) {
(Type::Var { name }, _) if vars.contains(name.as_str()) => {
if let Some(prev) = subst.get(name) {
docs/JOURNAL.md
+106
View File
@@ -1407,3 +1407,109 @@ budget at the start of 14a is tight, alternative is 14b
(GC/arena scaffolding) or 14c (poly fn as value); both have
real design questions that need an orchestrator design pass
first, so 14a stays the default.
## Iter 14a — polymorphic `List a` end-to-end + monomorphisation bug fixed
The dogfood payoff for parameterised ADTs (13a/b/c). Prior
to this iter, the only programs exercising the feature were
`box.ail.json` (single `MkBox(42)` round-trip) and
`maybe_int.ail.json` (single `or_else` call). That is a thin
slice — neither program builds a recursive parameterised ADT
nor calls a polymorphic higher-order fn. 14a closes that gap
with `data List a` + `map : forall a b. ((a) -> b, List<a>) ->
List<b>` recursive, then prints the result.
Three-agent run (tester → debugger → no implementer needed):
1. **Tester** wrote `examples/list_map_poly.ail.json` (5 defs:
`List`, `inc`, `map`, `print_list`, `main`) and a new e2e
test `list_map_poly_inc_then_prints` that asserts stdout
`["2", "3", "4"]`. Typecheck passed, build crashed:
`internal: monomorphisation: var \`a\` bound to two
distinct types`. Tester correctly stopped — fixture
encodes the contract; bug is in the compiler — and
reported with a hypothesis (recursion / shared
substitution slot in `map`).
2. **Debugger** refuted the hypothesis with a non-recursive
repro (`Cons(7, Nil)` triggers the same crash without
`map` in the picture at all). Real cause was much smaller:
in `synth_arg_type` (codegen, ~line 2087) for `Term::Ctor`,
any type var of the parent ADT that the ctor's args
couldn't pin was filled with `Type::unit()` as a
placeholder. For nullary ctors of a parameterised ADT
(`Nil : List<a>`, `None : Maybe<a>`) that placeholder
leaked upward. Inside a parent like `Cons(Int, Nil) :
List<a>`, `unify_for_subst` would walk
`cref.ail_fields = [Var{a}, Con{List,[Var{a}]}]` against
`[Int, Con{List,[Unit]}]`, bind `a = Int` from the head,
then collide with `a = Unit` from the tail. The recursive
`map` fixture surfaced it because it is the first program
to nest a nullary ctor of a parameterised ADT inside a
parent ctor — the existing 13b regressions never did. The
tester's hypothesis was reasonable from the symptom but
wrong on mechanism; refuting it via a smaller repro is
exactly the discipline the debugger role is for.
3. **Fix** (`crates/ailang-codegen/src/lib.rs`, +30/-9 LOC,
no new variant, no API change):
- Replace `Type::unit()` placeholder with a synth-only
wildcard `Type::Var { name: "$u" }`. The `$u` prefix is
a reserved-namespace convention that mirrors the
checker's `$m<id>` for instantiation metavars — same
trick (source-level identifiers can't start with `$`),
same goal (extra semantics without schema change).
- `unify_for_subst` short-circuits on a `$u`-prefixed
**arg-side** var: accept without binding, let a sibling
arg pin the type var instead. Param-side semantics
untouched. `derive_substitution`'s "var not pinned"
check still fires for genuinely under-determined calls
(those would have failed typechecking, so codegen never
sees them, but the safety net stands).
**Tests:** 25/25 e2e (was 24, +1 new poly test). All five
named regressions stayed green: `list_map_doubles_then_prints`,
`parameterised_box_round_trip`, `parameterised_maybe_match`,
`polymorphic_id_at_int_and_bool`, `polymorphic_apply_with_fn_param`.
Insertion sort still green. `cargo doc --no-deps`: 0 warnings
(workspace invariant from 13d/e/f preserved). `cargo build
--workspace` green.
**Process note: tester→debugger→done in one iter.** No
implementer dispatch needed — the debugger's mandate covers
"propose **and apply** a minimally invasive fix" once the
diagnosis is solid. 30 LOC across two sites in one file is
inside the role's scope (the role doc says "stop and report"
only on >50 LOC across multiple files). The orchestrator-side
work was the design (the source program), the scoped briefs,
and verification. This is the cleanest agent-flow shape so
far: each agent did exactly its job, the tester's wrong
hypothesis didn't propagate because the debugger tested it,
and the orchestrator never wrote compiler code.
**Findings flagged** (judgement deferred, not fixed):
- `CodegenError::Internal` (the catch-all string variant the
docwriter flagged in 13f) is now used by one more invariant
— the `$u` short-circuit could in principle be reached by a
malformed input; it's currently silent because typecheck
rejects under-determined calls upstream. Worth splitting
into typed variants the next time codegen tests get a real
rewrite. (Same finding as 13f, now reinforced by another
use site.)
- The `$u` / `$m` reserved-prefix convention (`$u` for
codegen synth wildcards, `$m<id>` for checker metavars)
is undocumented as a project-wide naming rule. Two
prefixes is fine; if a third appears, this should be
promoted to a DESIGN.md note.
**Next.** Parameterised ADTs are now genuinely usable for
real programs. The standard library starter set (an
`examples/std_*` series with `List`, `Maybe`, `Either`,
basic combinators `length`, `filter`, `fold`, `concat`)
becomes worthwhile in a way it wasn't pre-14a — that's a
plausible 14b alternative, smaller than GC/arena, and would
itself surface more dogfood bugs. The original 14b
(GC/arena) and 14c (poly fn as value) remain on the queue
but have not had a design pass.
examples/list_map_poly.ail.json
+230
View File
@@ -0,0 +1,230 @@
{
"schema": "ailang/v0",
"name": "list_map_poly",
"imports": [],
"defs": [
{
"kind": "type",
"name": "List",
"vars": ["a"],
"doc": "Polymorphic singly-linked list.",
"ctors": [
{ "name": "Nil", "fields": [] },
{
"name": "Cons",
"fields": [
{ "k": "var", "name": "a" },
{
"k": "con",
"name": "List",
"args": [{ "k": "var", "name": "a" }]
}
]
}
]
},
{
"kind": "fn",
"name": "inc",
"type": {
"k": "fn",
"params": [{ "k": "con", "name": "Int" }],
"ret": { "k": "con", "name": "Int" },
"effects": []
},
"params": ["x"],
"doc": "Add 1 to an Int.",
"body": {
"t": "app",
"fn": { "t": "var", "name": "+" },
"args": [
{ "t": "var", "name": "x" },
{ "t": "lit", "lit": { "kind": "int", "value": 1 } }
]
}
},
{
"kind": "fn",
"name": "map",
"type": {
"k": "forall",
"vars": ["a", "b"],
"body": {
"k": "fn",
"params": [
{
"k": "fn",
"params": [{ "k": "var", "name": "a" }],
"ret": { "k": "var", "name": "b" },
"effects": []
},
{
"k": "con",
"name": "List",
"args": [{ "k": "var", "name": "a" }]
}
],
"ret": {
"k": "con",
"name": "List",
"args": [{ "k": "var", "name": "b" }]
},
"effects": []
}
},
"params": ["f", "xs"],
"doc": "Polymorphic map: apply f to every element, recursing on the tail.",
"body": {
"t": "match",
"scrutinee": { "t": "var", "name": "xs" },
"arms": [
{
"pat": { "p": "ctor", "ctor": "Nil", "fields": [] },
"body": {
"t": "ctor",
"type": "List",
"ctor": "Nil",
"args": []
}
},
{
"pat": {
"p": "ctor",
"ctor": "Cons",
"fields": [
{ "p": "var", "name": "h" },
{ "p": "var", "name": "t" }
]
},
"body": {
"t": "ctor",
"type": "List",
"ctor": "Cons",
"args": [
{
"t": "app",
"fn": { "t": "var", "name": "f" },
"args": [{ "t": "var", "name": "h" }]
},
{
"t": "app",
"fn": { "t": "var", "name": "map" },
"args": [
{ "t": "var", "name": "f" },
{ "t": "var", "name": "t" }
]
}
]
}
}
]
}
},
{
"kind": "fn",
"name": "print_list",
"type": {
"k": "fn",
"params": [
{
"k": "con",
"name": "List",
"args": [{ "k": "con", "name": "Int" }]
}
],
"ret": { "k": "con", "name": "Unit" },
"effects": ["IO"]
},
"params": ["xs"],
"doc": "Print each Int on its own line.",
"body": {
"t": "match",
"scrutinee": { "t": "var", "name": "xs" },
"arms": [
{
"pat": { "p": "ctor", "ctor": "Nil", "fields": [] },
"body": { "t": "lit", "lit": { "kind": "unit" } }
},
{
"pat": {
"p": "ctor",
"ctor": "Cons",
"fields": [
{ "p": "var", "name": "h" },
{ "p": "var", "name": "t" }
]
},
"body": {
"t": "seq",
"lhs": {
"t": "do",
"op": "io/print_int",
"args": [{ "t": "var", "name": "h" }]
},
"rhs": {
"t": "app",
"fn": { "t": "var", "name": "print_list" },
"args": [{ "t": "var", "name": "t" }]
}
}
}
]
}
},
{
"kind": "fn",
"name": "main",
"type": {
"k": "fn",
"params": [],
"ret": { "k": "con", "name": "Unit" },
"effects": ["IO"]
},
"params": [],
"doc": "Map inc over [1,2,3] via polymorphic List, then print: 2,3,4.",
"body": {
"t": "app",
"fn": { "t": "var", "name": "print_list" },
"args": [
{
"t": "app",
"fn": { "t": "var", "name": "map" },
"args": [
{ "t": "var", "name": "inc" },
{
"t": "ctor",
"type": "List",
"ctor": "Cons",
"args": [
{ "t": "lit", "lit": { "kind": "int", "value": 1 } },
{
"t": "ctor",
"type": "List",
"ctor": "Cons",
"args": [
{ "t": "lit", "lit": { "kind": "int", "value": 2 } },
{
"t": "ctor",
"type": "List",
"ctor": "Cons",
"args": [
{ "t": "lit", "lit": { "kind": "int", "value": 3 } },
{
"t": "ctor",
"type": "List",
"ctor": "Nil",
"args": []
}
]
}
]
}
]
}
]
}
]
}
}
]
}