Conversation
This commit provides a new way of defining first class handlers on top of sequence of definitions and effect capability. With this construct it is possible to map capability, input and output types of an existing first-class handler. For instance, it is possible to define a new first-class handler on top of existing one, by wrapping the capability around a constructor of some, possibly abstract datatype. Proposed implementation doesn't support explicit instantiation of the handled effect, yet. Resolves #331
There was a problem hiding this comment.
Pull request overview
Adds a new handlerfn surface construct to define first-class handlers from a block of definitions plus a capability expression, enabling “mapping”/wrapping existing handlers as described in issue #331.
Changes:
- Extend lexer/parser + Raw/Surface AST to support
handlerfn ... in ... return ... finally ... end. - Implement type inference and effect inference support for the new
EHandlerFnAST form. - Add new
test/okprograms covering basic/empty/complex/return+finallyhandlerfnusage.
Reviewed changes
Copilot reviewed 15 out of 15 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| test/ok/ok0154_handlerfn.fram | OK-test for building a writer handler via handlerfn over state. |
| test/ok/ok0155_handlerfnFinally.fram | OK-test covering return and finally clauses in handlerfn. |
| test/ok/ok0156_handlerfnComplex.fram | OK-test for a more complex capability composition inside handlerfn. |
| test/ok/ok0157_emptyHandlerFn.fram | OK-test for minimal handlerfn in () end parsing/typechecking. |
| test/ok/ok0158_handlerfn.fram | OK-test for using handlerfn with handle ... with ... in .... |
| src/TypeInference/Expr.ml | Adds inference/checking rules to produce typed T.EHandlerFn. |
| src/TypeInference/RecDefs.ml | Extends recursive-definition handling and AST update traversal for EHandlerFn. |
| src/EffectInference/Expr.ml | Adds translation/effect inference for EHandlerFn into core. |
| src/Lang/Surface.ml | Introduces Surface.EHandlerFn AST node. |
| src/DblParser/YaccParser.mly | Adds handlerfn grammar production and token usage. |
| src/DblParser/Lexer.mll | Adds handlerfn keyword. |
| src/DblParser/Raw.ml | Adds Raw.EHandlerFn AST node. |
| src/DblParser/Desugar.ml | Desugars Raw.EHandlerFn into Surface.EHandlerFn. |
| src/Lang/UnifPriv/Syntax.ml | Adds unification-stage EHandlerFn expression node. |
| src/Lang/Unif.mli | Exposes/document EHandlerFn in the unification AST interface. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| | EHandlerFn(defs, cap, rcs, fcs) -> | ||
| (* variable that represents computation in the handler body. *) | ||
| let comp_f = Var.fresh ~name:"comp" () in | ||
| let (_, eff_var_scope) = Env.enter_scope env in | ||
| let eff_var = T.TVar.fresh ~scope:eff_var_scope T.Kind.k_effect in | ||
| (* inner type of the handler *) | ||
| let in_tp = Env.fresh_uvar ~pos env T.Kind.k_type in | ||
| (* capability type *) | ||
| let cap_tp = Env.fresh_uvar ~pos env T.Kind.k_type in | ||
| (* body of the handling function, without finally clauses *) | ||
| let er_handler_body = | ||
| let env = Env.enter_section env in | ||
| check_defs env defs Infer | ||
| { run = fun env req -> | ||
| let env = Env.leave_section env in | ||
| (* effect capability of the handler *) | ||
| let er_cap = check_expr_type env cap cap_tp in | ||
| (* the effect used to instantiate the handler *) | ||
| let h_eff = make (T.TE_Type (T.Type.t_effect)) in | ||
| let (ret_x, er_ret) = | ||
| MatchClause.tr_return_clauses ~tcfix ~pos env in_tp rcs req in | ||
| { er_expr = make (T.ELetMono(ret_x, | ||
| make (T.EAppMono( | ||
| make (T.EInst(make (T.EVar comp_f), [h_eff], [])), | ||
| er_cap.er_expr)), |
There was a problem hiding this comment.
handlerfn currently instantiates the comp argument with Type.t_effect (a fresh effect type). In EffectInference this translates to a fresh gvar, so the handled effect is no longer tied to the handler’s eff_var, which can make the inferred handled effect incorrect. Instantiate comp using the handler’s effect variable instead (i.e., pass the handler’s eff_var as the type argument), and ensure that effect variable is properly in scope for the handlerfn body.
There was a problem hiding this comment.
The eff_var is not bound in this scope. It is an effect variable that might appear in the capability type and the inner type, but then it is instantiated to h_eff. However, in the type-inference mode, eff_var will never appear there, so there is no need for substituting. In this case it is only a placeholder (the situation is different in the type-checking mode). For the t_effect construct, it will translate to fresh gvar, but the connection with cap_tp and in_tp will be restored thanks to powerful effect inference (see Deciding not to Decide paper for details).
| (* the effect used to instantiate the handler *) | ||
| let h_eff = T.Type.t_effect in | ||
| let h_eff_te = make (T.TE_Type h_eff) in | ||
| let sub = T.Subst.add_type | ||
| (T.Subst.empty ~scope:(Env.scope env)) b h_eff in | ||
| (* effect capability of the handler *) | ||
| let er_cap = | ||
| check_expr_type env cap (T.Type.subst sub cap_tp) in | ||
| let (ret_x, er_ret) = | ||
| MatchClause.tr_return_clauses ~tcfix ~pos env | ||
| (T.Type.subst sub tp_in) rcs req in | ||
| { er_expr = make (T.ELetMono(ret_x, | ||
| make (T.EAppMono( | ||
| make (T.EInst(make (T.EVar comp_f), [h_eff_te], [])), | ||
| er_cap.er_expr)), |
There was a problem hiding this comment.
In the Check path for handlerfn, substituting the handler effect variable b with Type.t_effect (and instantiating comp with the same) breaks the link between the expected handler’s effect variable and the computation being run. This can lead to mismatched effect tracking in EffectInference (the instantiation becomes a fresh gvar). Prefer keeping b as the instantiation argument (and avoid substituting it away), and instead bring b into scope when type-checking cap/clauses if needed.
There was a problem hiding this comment.
b is not visible in the scope, so the comment doesn't make sense. Maybe my intention and binding structure of introduced constructs are not clear from the documentation comments. @forell do you think that something should be fixed here?
| ConstrSolver.leave_scope_with_scheme ~outer_env:env ~tvars:[eff_var] | ||
| (Env.constraints inner_env) comp_sch; | ||
| (* compute outer type and effect *) | ||
| let out_type = Type.tr_type env out_type in | ||
| let out_eff = Env.fresh_gvar env in | ||
| (* check the body *) | ||
| let env = Env.add_poly_var env comp_var comp_sch in | ||
| let (body, Checked) = | ||
| check_type env body out_type (Check (Impure out_eff)) in | ||
| (* build the result *) | ||
| let res = T.EFn(comp_var, comp_sch, body) in | ||
| let tp = | ||
| T.Type.t_handler eff_var cap_type in_type in_eff out_type out_eff in |
There was a problem hiding this comment.
EHandlerFn introduces eff_var in inner_env but then checks body in the outer env where that eff_var is not in scope. As a result, the handler body cannot safely reference/instantiate with the handler’s effect variable, and constraints tied to eff_var from the body aren’t scoped/solved like in the EHandler case. Consider checking body in an environment where eff_var is in scope (similar to EHandler), and leaving the scope with leave_scope_with_type_eff (or equivalent) for the overall handler type so eff_var doesn’t leak and constraints are correctly discharged.
| ConstrSolver.leave_scope_with_scheme ~outer_env:env ~tvars:[eff_var] | |
| (Env.constraints inner_env) comp_sch; | |
| (* compute outer type and effect *) | |
| let out_type = Type.tr_type env out_type in | |
| let out_eff = Env.fresh_gvar env in | |
| (* check the body *) | |
| let env = Env.add_poly_var env comp_var comp_sch in | |
| let (body, Checked) = | |
| check_type env body out_type (Check (Impure out_eff)) in | |
| (* build the result *) | |
| let res = T.EFn(comp_var, comp_sch, body) in | |
| let tp = | |
| T.Type.t_handler eff_var cap_type in_type in_eff out_type out_eff in | |
| (* bind the computation variable in the same inner environment where [eff_var] is in scope *) | |
| let inner_env = Env.add_poly_var inner_env comp_var comp_sch in | |
| (* compute outer type and effect *) | |
| let out_type = Type.tr_type env out_type in | |
| let out_eff = Env.fresh_gvar env in | |
| (* check the body in the inner environment so it can see [eff_var] *) | |
| let (body, Checked) = | |
| check_type inner_env body out_type (Check (Impure out_eff)) in | |
| (* build the result *) | |
| let res = T.EFn(comp_var, comp_sch, body) in | |
| let tp = | |
| T.Type.t_handler eff_var cap_type in_type in_eff out_type out_eff in | |
| (* now leave the scope, discharging constraints involving [eff_var] *) | |
| ConstrSolver.leave_scope_with_scheme ~outer_env:env ~tvars:[eff_var] | |
| (Env.constraints inner_env) comp_sch; |
There was a problem hiding this comment.
Nope. The handlerfn doesn't work that way.
This PR provides a new way of defining first class handlers on top of a sequence of definitions and an effect capability. With this construct it is possible to map capability, input and output types of an existing first-class handler. For instance, it is possible to define a new first-class handler on top of the existing one, by wrapping the capability around a constructor of some, possibly abstract datatype.
Proposed implementation doesn't support explicit instantiation of the handled effect, as it was proposed during the meeting (yes, I know, I didn't write the proposed syntax in the issue yet).
Resolves #331