Feat/effects partial inference 59#308
Closed
hyperpolymath wants to merge 2 commits into
Closed
Conversation
… row (Refs #59) STAGE-B effect-tracking spine. Until now ctx.current_eff was declared but never read or mutated — effect inference did nothing, and #59's explicit motivating case ('{Partial} — short-circuit failure, ? on Result') produced no tracking. Root-cause, single concrete effect source for tracking-only v1: - ExprTry with no catch arm (incl. the 'e?' desugar, parser.mly expr_postfix QUESTION) unions Partial into ctx.current_eff; a handled try (catch arm present) discharges it and adds nothing. - check_fn_decl now snapshots/resets current_eff around the body, then — only when an effect row is *explicitly declared* — requires the inferred row ⊆ declared (Effect.eff_subset), erroring with a new EffectNotDeclared type_error. Undeclared rows stay permissive (tracking-only v1), so blast radius is zero: no stdlib/test uses '?' or an explicit row. Other effect sources (IO calls, Async) remain unconstrained for now — deliberately scoped; this stands up the accumulate→subsume path they will plug into, it does not fake full inference. Tests: test/test_effects.ml — declared /{Partial}+? ok; declared /{IO}+? rejected (#59 mismatch naming Partial); undeclared permissive; handled try adds no Partial. Full gate 257/257 (253 + 4, no regression). Refs #59 (left open for user joint-close per requirements-target rule). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…] comment (Refs #59) Completes the human+machine docs for the #207 effect-inference spine: - SPEC.adoc §3.4: Exn[Error] examples → Throws[E] (Exn retired in #203; the old text was stale/misleading), and a new 'Effect inference (tracking-only v1)' subsection stating the actual implemented rule (catch-less try/? ⇒ Partial; declared rows enforced inferred⊆declared; undeclared permissive). Disambiguated from 'Partial by Default' (termination), an unrelated reuse of the word. - lib/effect.ml: the 'type parameter not yet threaded' comment was doc-drift — #204 threads Throws[E] via name-mangling in Typecheck.lower_effect_expr; comment now states reality. Out-of-scope residual (surfaced, not half-swept): SPEC §5.2/§6.5 effect-handler examples still use the retired 'Exn' name — that is handler-design territory (deferred) and a separate Exn→Throws spec sweep, not part of this slice. Gate 257/257 (unchanged). Refs #59. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Owner
Author
|
Closing as superseded — fully duplicated by already-merged work on main. Tracing the three commits on this branch:
The 3-dot diff Refs #59 (lineage-only; do not reopen). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.