Prose: render param-in restrictions and (kernel) marker (prep.3 holes) #35

New Issue

2026-05-29T09:19:05+02:00

Brummel commented

2026-05-29 09:19:05 +02:00

The prose printer (crates/ailang-prose/src/lib.rs) silently drops
two fields introduced by the kernel-extension-mechanics milestone
(prep.3, #33):

TypeDef.param_in — write_type_def does not inspect the map;
the closed-set restriction (param-in (a Int Float)) disappears
on render.
Module.kernel — write_module does not inspect the flag; a
(kernel) module is indistinguishable from a normal one in prose.

Both are semantically load-bearing (the difference between
NumBox<Int> accepted and NumBox<Str> rejected is exactly the
param_in map; auto-import behaviour depends on kernel), so this
goes beyond the "prose-is-lossy by design" carve-out for (con T)
wrappings and parenthesis elision.

Proposed projection — param-in:

Inline on the type-var list, analogous to forall<a> where Num a:

data NumBox<a in {Int, Float}> = MkNumBox(a)

Multiple restrictions:

data MultiBox<a in {Int, Float}, b in {Str}> = MkMulti(a, b)

The restriction sits at the point where the variable is introduced,
which keeps the data line readable as a single declaration.

Proposed projection — (kernel):

Marker comment on the line below // module …, analogous to
// @suppress:

// module kernel_stub
// @kernel

data StubT<a in {Int, Float}> = Stub(a)

// @kernel reuses the existing // @<attr> convention (currently
only @suppress) instead of introducing a new top-level keyword.

Open question for the brainstorm:

(term-ctor T Ctor args) currently renders as Ctor(args) (the
type name is dropped — recoverable from typecheck context). With
param-in in scope, the type identity at the constructor site is
load-bearing for the LLM reader (to local-check the restriction).
Worth empirically testing whether the LLM-mediated roundtrip
recovers (term-ctor NumBox MkNumBox 17) correctly from
MkNumBox(17), or whether prose should render NumBox::MkNumBox(17)
when the ctor's type carries a param-in map.

Form-A is unchanged. Canonical and hashable artefacts move
nothing. Only the prose projection changes.

Scope:

crates/ailang-prose/src/lib.rs — extend write_type_def
(param-in rendering) and write_module (@kernel marker)
New snapshot fixtures under examples/ exercising both fields
(likely a minimal numbox_demo.ail for param-in and a
re-projection of kernel_stub for @kernel)
docs/PROSE_ROUNDTRIP.md — document the two new projections

Refs #33.

The prose printer (`crates/ailang-prose/src/lib.rs`) silently drops two fields introduced by the kernel-extension-mechanics milestone (prep.3, #33): - `TypeDef.param_in` — `write_type_def` does not inspect the map; the closed-set restriction `(param-in (a Int Float))` disappears on render. - `Module.kernel` — `write_module` does not inspect the flag; a `(kernel)` module is indistinguishable from a normal one in prose. Both are semantically load-bearing (the difference between `NumBox<Int>` accepted and `NumBox<Str>` rejected is exactly the `param_in` map; auto-import behaviour depends on `kernel`), so this goes beyond the "prose-is-lossy by design" carve-out for `(con T)` wrappings and parenthesis elision. **Proposed projection — `param-in`:** Inline on the type-var list, analogous to `forall<a> where Num a`: ``` data NumBox<a in {Int, Float}> = MkNumBox(a) ``` Multiple restrictions: ``` data MultiBox<a in {Int, Float}, b in {Str}> = MkMulti(a, b) ``` The restriction sits at the point where the variable is introduced, which keeps the `data` line readable as a single declaration. **Proposed projection — `(kernel)`:** Marker comment on the line below `// module …`, analogous to `// @suppress`: ``` // module kernel_stub // @kernel data StubT<a in {Int, Float}> = Stub(a) ``` `// @kernel` reuses the existing `// @<attr>` convention (currently only `@suppress`) instead of introducing a new top-level keyword. **Open question for the brainstorm:** `(term-ctor T Ctor args)` currently renders as `Ctor(args)` (the type name is dropped — recoverable from typecheck context). With `param-in` in scope, the type identity at the constructor site is load-bearing for the LLM reader (to local-check the restriction). Worth empirically testing whether the LLM-mediated roundtrip recovers `(term-ctor NumBox MkNumBox 17)` correctly from `MkNumBox(17)`, or whether prose should render `NumBox::MkNumBox(17)` when the ctor's type carries a `param-in` map. **Form-A is unchanged.** Canonical and hashable artefacts move nothing. Only the prose projection changes. **Scope:** - `crates/ailang-prose/src/lib.rs` — extend `write_type_def` (`param-in` rendering) and `write_module` (`@kernel` marker) - New snapshot fixtures under `examples/` exercising both fields (likely a minimal `numbox_demo.ail` for `param-in` and a re-projection of `kernel_stub` for `@kernel`) - `docs/PROSE_ROUNDTRIP.md` — document the two new projections Refs #33.

Brummel added the feature label 2026-05-29 09:19:05 +02:00

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: Brummel/AILang#35