Conversation
This commit introduces affine effects to the effect system and adapts the effect inference algorithm to support this feature. However, the algorithm doesn't check if the `aff effect` construct uses the continuation in the affine way -- it just trust the programmer.
There was a problem hiding this comment.
Pull request overview
This PR extends DBL’s effect system with effect modes (currently Unrestricted and Affine) and updates parsing, typing, and effect inference so effects/handlers can be projected to a mode (e.g. aff E) and effect variables can carry an implicit mode (notably enabling affine IO).
Changes:
- Add
EffectModeplus mode-aware effect projections (TEffProj/TE_EffProj) and propagate mode through parser → surface → unif → effect inference. - Replace the effect-guard propositional logic in ConE with a mode-enriched formula representation and update constraint solving/pretty-printing accordingly.
- Add new OK/ERR tests covering affine effects, mixed affinity in handlers, and rejecting non-affine effects passed to affine parameters.
Reviewed changes
Copilot reviewed 38 out of 38 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| test/ok/ok0154_affineEffect.fram | Basic acceptance test for aff effects in type annotations. |
| test/ok/ok0155_affineIO.fram | Demonstrates affine IO interop via implicit mode projection. |
| test/ok/ok0156_affineExn.fram | Adds an affine exception-like effect and handler test. |
| test/ok/ok0157_mixedAffinity.fram | Tests mixed unrestricted/affine operations in a single handler. |
| test/ok/ok0158_affineIdEffect.fram | Tests affine effect operation expression (aff effect ... => ...). |
| test/err/tc_0021_nonAffineParameter.fram | Error test for passing non-affine effectful function to affine parameter. |
| src/Utils/EffectMode.ml | Introduces the EffectMode.t definition (Unrestricted/Affine). |
| src/TypeInference/Type.ml | Adds kind-checking/translation support for surface TEffProj. |
| src/TypeInference/Expr.ml | Threads effect mode through EEffect during type checking. |
| src/ToCore/Type.ml | Switches effect “fixing” to the new mode-aware formula API. |
| src/Lang/UnifPriv/TypeExpr.ml | Treats TE_EffProj as an effect-kind type in unif type expressions. |
| src/Lang/UnifPriv/Syntax.ml | Extends unif AST with TE_EffProj and mode-carrying EEffect. |
| src/Lang/UnifCommon/TVar.mli | Adds mode to type variables and documents implicit projection semantics. |
| src/Lang/UnifCommon/TVar.ml | Implements mode on TVars and extends fresh with optional ~mode. |
| src/Lang/UnifCommon/Pretty.mli | Adds PP_EffProj to effect pretty-print tree representation. |
| src/Lang/UnifCommon/Pretty.ml | Prints mode projections in effects (aff ...) and handles precedence. |
| src/Lang/UnifCommon/BuiltinType.ml | Marks built-in IO effect TVar as ~mode:Affine. |
| src/Lang/Unif.mli | Exposes TE_EffProj and mode-carrying EEffect in the public Unif API. |
| src/Lang/Surface.ml | Extends surface AST with TEffProj and mode-carrying EEffect. |
| src/Lang/ConEPriv/TVar.mli | Documents/exposes TVar.mode for ConE pretty-printing/projection. |
| src/Lang/ConEPriv/Pretty.ml | Pretty-prints effects by expanding mode-aware formulas into projections. |
| src/Lang/ConEPriv/Formula.mli | New mode-aware formula interface (top/bot/conj/disj/implies/fix/CNF). |
| src/Lang/ConEPriv/Formula.ml | Implements mode-aware formulas as paired IncrSAT formulas + printing helpers. |
| src/Lang/ConEPriv/Effct.mli | Switches effect guards to mode-aware Formula.t and adds Effct.proj. |
| src/Lang/ConEPriv/Effct.ml | Updates effect operations to use mode-aware formula guards and projection. |
| src/Lang/ConE.mli | Makes formula abstract and re-exports mode-aware formula operations. |
| src/Lang/ConE.ml | Wires ConE’s formula to ConEPriv.Formula.t and re-exports Formula. |
| src/IncrSAT/Solver.mli | Adds add_cnf API to add CNF constraints directly. |
| src/IncrSAT/Solver.ml | Implements add_cnf and rewrites add_imply in terms of it. |
| src/IncrSAT/Formula.mli | Minor doc wording tweaks (no functional change). |
| src/EffectInference/Type.ml | Adds implicit projection when translating effect TVars with a mode; supports TE_EffProj. |
| src/EffectInference/Expr.ml | Projects delimiter effect by mode for EEffect during effect inference. |
| src/EffectInference/Env.ml | Adds constraints via CNF using new mode-aware formula CNF conversion. |
| src/EffectInference/ConstrSimplify.ml | Replaces IncrSAT.Formula operations with the new T.Formula API. |
| src/DblParser/YaccParser.mly | Adds aff keyword, parses aff effect and aff <effect> (projection) forms. |
| src/DblParser/Raw.ml | Adds mode to raw EEffect and restructures FldNameEffectFn to include mode. |
| src/DblParser/Lexer.mll | Adds aff keyword tokenization. |
| src/DblParser/Desugar.ml | Desugars TEffProj and threads mode through effect-operation expressions and fields. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 38 out of 38 changed files in this pull request and generated 2 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| let get_gvar eff = | ||
| match T.Effct.view eff with | ||
| | ([], [(gv, p)]) when IncrSAT.Formula.is_true p -> gv | ||
| | ([], [(gv, p)]) when T.Formula.is_true p -> gv |
There was a problem hiding this comment.
get_gvar currently only accepts effects of the form gvar with predicate p where T.Formula.is_true p. With affine modes, projecting an effect via T.Effct.proj Affine will turn an unconditional gvar into one guarded by Formula.of_mode Affine (i.e. p is not is_true anymore), so get_gvar will start throwing the internal-error despite the effect still being a single generalizable variable. Consider relaxing this check (e.g. accept any p that is not T.Formula.is_false, or accept formulas that correspond to a single certain mode such as Formula.of_mode Affine) so affine projections don’t break constraint simplification invariants.
| | ([], [(gv, p)]) when T.Formula.is_true p -> gv | |
| | ([], [(gv, p)]) when not (T.Formula.is_false p) -> gv |
There was a problem hiding this comment.
WHAT!? This function shall be used only on effects constructed by T.Effct.gvar gv, so it is guaranteed that the formula is true (unless, the variable was set in a meantime). This is unrelated to effect modes.
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 38 out of 38 changed files in this pull request and generated no new comments.
Comments suppressed due to low confidence (1)
src/IncrSAT/Formula.mli:22
- Typo in the updated doc comment: “Conjunction of two formuals” → “Conjunction of two formulas”.
(** Formula built from a single fresh propositional variable *)
val fresh_var : unit -> t
(** Conjunction of two formuals *)
val conj : t -> t -> t
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Foxinio
left a comment
Foxinio
left a comment
There was a problem hiding this comment.
For the first look at this PR, the changes look good.
I did leave some minor suggestions, which relate to code presentation.
However I did not look thoroughly enough at implementation of constraint simplification (which i intend to do shortly).
|
|
||
| let hBT = | ||
| handler BT | ||
| { effect flip () = resume True; resume False |
There was a problem hiding this comment.
I don't know it it's a good practice, but I maybe we should add a TODO comment, to copy this file with flip incorrectly labeled as aff to error tests once this detection is implemented.
There was a problem hiding this comment.
I think it is a bad practice. Nobody would look into test files as long as they work correctly, so such TODO comment would stay there forever. On the other hand, the person who will implement this detection (probably me) would be responsible to provide tests, and probably would write such a test, or very similar one from the scratch, as it is very obvious thing to check.
|
|
||
| | EEffect(lbl, x, body, res_tp) -> | ||
| | EEffect(lbl, mode, x, body, res_tp) -> | ||
| (* TODO: check if the usage of resumption respects the mode *) |
There was a problem hiding this comment.
In spite of what are current guidelines, I suggest including nr of issue in comments such as this one.
There was a problem hiding this comment.
Are there any such guidelines? I see a cyclic dependency: to get the issue number we need to create the issue, for which we need to merge this PR, for which we should update this comment, but this require the issue number.
|
|
||
| (** Project the effect to the given mode. The call to [proj mode eff] is | ||
| equivalent to [guard eff (Formula.of_mode mode)]. *) | ||
| val proj : EffectMode.t -> t -> t |
There was a problem hiding this comment.
From the first part of the comment i got the impression that this function performs some kind of pass through the effect and sets all leaves (or formulas inside) to have mode given to this function (as one would do in imperative language). Instead this is achieved lazily by adding node that when read is to be interpreted, as if pass through was performed (as is suggested by the second part of this comment)..
I have no suggestion in this comment, just wanted to confirm i have correct understanding of the code.
There was a problem hiding this comment.
Since the function takes the effect and returns the effect, it at least pretends to be purely functional: it doesn't alter the meaning of the input effect. However, propositional variables, or gvars might be set during the effect inference process, thus the exact representation of the effect may change each time it is viewed, by removing some redundant parts. It is just an optimization, in the same spirit as path compression in union-find, or in the type representation in the Unif language.
This PR introduces affine effects to the effect system and adapts the effect inference algorithm to support this feature. However, the algorithm doesn't check if the
aff effectconstruct uses the continuation in the affine way–it just trust the programmer.The implementation is surprisingly simple: it is enough to change the propositional logic used by the effect inference. It is so simple, that I am not totally convinced if it is correct: the simplification rules that manipulates formulas looks reasonable for me, but it would be nice if someone else would look at them with some dose of criticism.
To have affine
IOeffect, effect variables (in Unif and ConE) have attached effect mode, and each use of this variable is implicitly projected to that mode (and this projection is not printed by the pretty-printer). This approach enables simple implementation, and paves the path towards a nice feature: the programmer could annotate type variables with a mode in binders, so the variable is used only with that (or more restrictive) mode. We can discuss this direction later.As the next steps, the following things should be done (as separate issues):
Mutablemodule) should be adapted to use this feature to improve the interface;