iter effect-doc-honesty: make the effect-system documentation true
Standalone documentation-honesty tidy (no language/checker/codegen change; `ail check`/`run` byte-unchanged by construction). Corrects three false effect-system claims the effect-subsystem recon surfaced, plus two satellite mentions, guarded by a new doc-presence pin: - DESIGN.md Decision 3: removed the "row-polymorphic (`![IO | r]`)" claim (no EffectRow / row variable exists in any crate — effect sets are a flat, unordered, closed set unified by set-equality); reconciled "`IO` and `Diverge` are wired up" to IO-only + `Diverge` reserved/unimplemented (zero code in any crate), modelled on Decision 4's reserved-refinements precedent. - DESIGN.md "What is not (yet) supported": "IO and Diverge ops" bullet -> IO-only + Diverge-reserved. - ast.rs Term::Do doc-comment: "resolved against the effect-handler table at link time" -> the real mechanism (typecheck lookup in Env::effect_ops + literal lower_effect_op codegen match; no handler table, no link-time resolution). - form_a.md:226 + rule 3, and main.rs merge-prose CONTRACT example: Diverge mentions reconciled in lockstep. - new crates/ailang-core/tests/effect_doc_honesty_pin.rs: 4 tests, fiction-absent + corrected-anchor-present, single-line wrap-robust substrings. cargo test --workspace 600 -> 604 (4 new pin tests, 0 regressions); design_schema_drift / spec_drift / schema_coverage stay green, empirically confirming none scans the effect-prose region.
This commit is contained in:
+10
-4
@@ -168,9 +168,14 @@ Advantages:
|
||||
## Decision 3: pure core language + algebraic effects
|
||||
|
||||
The default is total, pure functions. Effects are declared as a set in the
|
||||
function type: `(Int) -> Int ![IO]`. The effect set is row-polymorphic
|
||||
(`![IO | r]`). In the MVP only the effects `IO` and `Diverge` (for infinite
|
||||
loops) are wired up.
|
||||
function type: `(Int) -> Int ![IO]`. The effect set is a
|
||||
flat, unordered, closed set of effect names, unified by set-equality —
|
||||
there is no effect row variable; a signature lists exactly the effects
|
||||
its body may perform.
|
||||
In the MVP only the effect `IO` is wired up (its sole op is `io/print_str`).
|
||||
`Diverge` (for non-termination) is reserved as an effect name but is
|
||||
unimplemented — no op, no codegen, no checker injection — in the same
|
||||
sense Decision 4 reserves refinements.
|
||||
|
||||
This is the most important LLM property: when I read a function, I can trust
|
||||
its signature without reading the body.
|
||||
@@ -2719,7 +2724,8 @@ proof is the protection.
|
||||
Snapshot of the current boundary. Items move out of this list
|
||||
as iterations land; the JOURNAL records when.
|
||||
|
||||
- No effect handlers — only the built-in IO and Diverge ops.
|
||||
- No effect handlers — only the built-in `IO` op (`io/print_str`).
|
||||
`Diverge` is a reserved effect name with no op and no codegen.
|
||||
- No refinements / SMT escalation.
|
||||
- No HM inference inside bodies. Top-level def types are explicit;
|
||||
polymorphism is opt-in via `Type::Forall { vars, body }`. Inside
|
||||
|
||||
Reference in New Issue
Block a user