diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml index e1f7dbd1..ed2b6640 100644 --- a/src/DblParser/Desugar.ml +++ b/src/DblParser/Desugar.ml @@ -292,9 +292,10 @@ let rec tr_ctor_pattern (p : Raw.expr) = | ESelect(path, p) -> path_append path (tr_ctor_pattern p) | EWildcard | ENum _ | ENum64 _ | EStr _ | EChr _ | EParen _ | EVar _ - | EImplicit _ | EFn _ | EApp _ | EDefs _ | EMatch _ | EHandler _ | EEffect _ - | ERecord _ | EMethod _ | EExtern _ | EAnnot _ | EIf _ | EBOp _ | EUOp _ - | EList (_ :: _) | EPub _ | EMethodCall _ | EInterp (_, _) -> + | EImplicit _ | EFn _ | EApp _ | EDefs _ | EMatch _ | EHandler _ + | EHandlerFn _ | EEffect _ | ERecord _ | EMethod _ | EExtern _ | EAnnot _ + | EIf _ | EBOp _ | EUOp _ | EList (_ :: _) | EPub _ | EMethodCall _ + | EInterp (_, _) -> Error.fatal (Error.desugar_error p.pos) (** Translate a pattern *) @@ -341,8 +342,9 @@ let rec tr_pattern (p : Raw.expr) = make (List.fold_right cons ps pnil).data | EPub p -> make (Attributes.make_vis_pattern (tr_pattern p)).data - | EFn _ | EDefs _ | EMatch _ | EHandler _ | EEffect _ | ERecord _ - | EMethod _ | EExtern _ | EIf _ | EMethodCall _ | EAnnot(_, AnnotTotal _) -> + | EFn _ | EDefs _ | EMatch _ | EHandler _ | EHandlerFn _ | EEffect _ + | ERecord _ | EMethod _ | EExtern _ | EIf _ | EMethodCall _ + | EAnnot(_, AnnotTotal _) -> Error.fatal (Error.desugar_error p.pos) (** Translate a pattern, separating out its annotation [Some sch] if present, @@ -360,8 +362,9 @@ and tr_annot_pattern (p : Raw.expr) = Error.fatal (Error.desugar_error pos) | EWildcard | EUnit | EVar _ | EBOpID _ | EUOpID _ | EImplicit _ | ECtor _ | ENum _ | ENum64 _ | EStr _ | EChr _ | EFn _ | EApp _ | EDefs _ | EMatch _ - | EHandler _ | EEffect _ | ERecord _ | EMethod _ | EMethodCall _ | EExtern _ - | EIf _ | ESelect _ | EBOp _ | EUOp _ | EList _ | EPub _ | EInterp (_, _) -> + | EHandler _ | EHandlerFn _ | EEffect _ | ERecord _ | EMethod _ + | EMethodCall _ | EExtern _ | EIf _ | ESelect _ | EBOp _ | EUOp _ | EList _ + | EPub _ | EInterp (_, _) -> tr_pattern p, None and tr_named_pattern (fld : Raw.field) = @@ -432,8 +435,9 @@ let rec tr_let_pattern (p : Raw.expr) = LP_Pat(tr_pattern p) | EWildcard | EParen _ | EFn _ | EApp _ | EDefs _ - | EMatch _ | EHandler _| EEffect _ | ERecord _ | EMethod _ - | EExtern _ | EAnnot _ | EIf _ | EBOp _ | EUOp _ | EPub _ | EMethodCall _ -> + | EMatch _ | EHandler _ | EHandlerFn _ | EEffect _ | ERecord _ | EMethod _ + | EExtern _ | EAnnot _ | EIf _ | EBOp _ | EUOp _ | EPub _ + | EMethodCall _ -> Error.fatal (Error.desugar_error p1.pos) end @@ -442,8 +446,8 @@ let rec tr_let_pattern (p : Raw.expr) = | EInterp (_, _) -> LP_Pat (tr_pattern p) - | EFn _ | EDefs _ | EMatch _ | EHandler _ | EEffect _ | ERecord _ - | EMethod _ | EExtern _ | EIf _ | EMethodCall _ -> + | EFn _ | EDefs _ | EMatch _ | EHandler _ | EHandlerFn _ | EEffect _ + | ERecord _ | EMethod _ | EExtern _ | EIf _ | EMethodCall _ -> Error.fatal (Error.desugar_error p.pos) (** Translate a function, given a list of formal parameters *) @@ -492,14 +496,15 @@ let rec tr_poly_expr (e : Raw.expr) = | EWildcard | ENum _ | ENum64 _ | EStr _ | EChr _ | EParen _ | EFn _ | EApp _ | EEffect _ | EDefs _ | EMatch _ | ERecord _ | EHandler _ - | EExtern _ | EAnnot _ | EIf _ | EMethod _ | ESelect _ | EBOp _ | EUOp _ - | EList (_ :: _) | EPub _ | EMethodCall _ | EInterp (_, _) -> + | EHandlerFn _ | EExtern _ | EAnnot _ | EIf _ | EMethod _ | ESelect _ + | EBOp _ | EUOp _ | EList (_ :: _) | EPub _ | EMethodCall _ + | EInterp (_, _) -> Error.fatal (Error.desugar_error e.pos) end | EWildcard | ENum _ | ENum64 _ | EStr _ | EChr _ | EParen _ | EFn _ | EApp _ - | EEffect _ | EDefs _ | EMatch _ | ERecord _ | EHandler _ | EExtern _ - | EAnnot _ | EIf _ | EBOp _ | EUOp _ | EList (_ :: _) | EPub _ + | EEffect _ | EDefs _ | EMatch _ | ERecord _ | EHandler _ | EHandlerFn _ + | EExtern _ | EAnnot _ | EIf _ | EBOp _ | EUOp _ | EList (_ :: _) | EPub _ | EMethodCall _ | EInterp (_, _) -> Error.fatal (Error.desugar_error e.pos) @@ -514,9 +519,9 @@ and tr_poly_expr_def (e : Raw.expr) = make (PE_Poly (tr_poly_expr e)) | ENum _ | ENum64 _ | EStr _ | EChr _ | EApp _ | EMethodCall _ | EDefs _ - | EMatch _ | EHandler _ | EEffect _ | EExtern _ | EAnnot _ | EIf _ - | ESelect _ | EBOp _ | EUOp _ | EList _ | EWildcard | ERecord _ | EPub _ - | EInterp (_, _) -> + | EMatch _ | EHandler _ | EHandlerFn _ | EEffect _ | EExtern _ | EAnnot _ + | EIf _ | ESelect _ | EBOp _ | EUOp _ | EList _ | EWildcard | ERecord _ + | EPub _ | EInterp (_, _) -> make (PE_Expr (tr_expr e)) and tr_apply (e1 : Raw.expr) (es : Raw.expr list) = @@ -574,6 +579,11 @@ and tr_expr (e : Raw.expr) = let e = tr_expr h in let (rcs, fcs) = map_h_clauses tr_h_clause hcs in make (EHandler(e, rcs, fcs)) + | EHandlerFn(defs, cap_e, hcs) -> + let defs = tr_defs defs in + let cap_e = tr_expr cap_e in + let (rcs, fcs) = map_h_clauses tr_h_clause hcs in + make (EHandlerFn(defs, cap_e, rcs, fcs)) | EEffect { label; args; resumption; body } -> let (pos, res) = match resumption with diff --git a/src/DblParser/Lexer.mll b/src/DblParser/Lexer.mll index 8a1cbd66..d7aa4064 100644 --- a/src/DblParser/Lexer.mll +++ b/src/DblParser/Lexer.mll @@ -25,6 +25,7 @@ let kw_map = ; "fn", KW_FN ; "handle", KW_HANDLE ; "handler", KW_HANDLER + ; "handlerfn", KW_HANDLERFN ; "if", KW_IF ; "import", KW_IMPORT ; "in", KW_IN diff --git a/src/DblParser/Raw.ml b/src/DblParser/Raw.ml index 9b3f8c43..738266a6 100644 --- a/src/DblParser/Raw.ml +++ b/src/DblParser/Raw.ml @@ -199,6 +199,10 @@ and expr_data = | EHandler of expr * h_clause list (** First-class handler *) + | EHandlerFn of def list * expr * h_clause list + (** First-class handler defined on top of a block of definitions. In + contrast to [EHandler], this handler does not create a fresh label. *) + | EEffect of { label : expr option; args : expr list; diff --git a/src/DblParser/YaccParser.mly b/src/DblParser/YaccParser.mly index 6cdf778d..9a38242f 100644 --- a/src/DblParser/YaccParser.mly +++ b/src/DblParser/YaccParser.mly @@ -13,7 +13,7 @@ %token BR_OPN BR_CLS SBR_OPN SBR_CLS CBR_OPN CBR_CLS ATTR_OPEN %token ARROW EFF_ARROW ARROW2 BAR COLON COMMA DOT EQ SEMICOLON2 SLASH GT_DOT %token KW_ABSTR KW_AS KW_DATA KW_EFFECT KW_ELSE KW_END KW_EXTERN -%token KW_FINALLY KW_FN KW_HANDLE KW_HANDLER KW_IF KW_IMPORT +%token KW_FINALLY KW_FN KW_HANDLE KW_HANDLER KW_HANDLERFN KW_IF KW_IMPORT %token KW_IN KW_LABEL KW_LET KW_MATCH KW_METHOD KW_MODULE KW_OF KW_OPEN %token KW_PARAMETER KW_PUB %token KW_REC @@ -458,6 +458,8 @@ expr_simple | KW_MATCH expr KW_WITH bar_opt match_clause_list KW_END { make (EMatch($2, $5)) } | KW_HANDLER expr h_clauses KW_END { make (EHandler($2, $3)) } +| KW_HANDLERFN def_list KW_IN expr h_clauses KW_END + { make (EHandlerFn($2, $4, $5)) } | CBR_OPN field_list CBR_CLS { make (ERecord $2) } | BR_OPN op BR_CLS { make (EBOpID ($2).data)} | BR_OPN op DOT BR_CLS { make (EUOpID ($2).data)} diff --git a/src/EffectInference/Expr.ml b/src/EffectInference/Expr.ml index 5e193eb7..deb43fe2 100644 --- a/src/EffectInference/Expr.ml +++ b/src/EffectInference/Expr.ml @@ -495,6 +495,35 @@ and infer_type : type ed. () in (res, tp, return_pure eff_req) + | EHandlerFn { eff_var; cap_type; in_type; out_type; comp_var; body } -> + (* create effect variable *) + let inner_env = Env.enter_scope env in + let (inner_env, eff_var) = Env.add_tvar inner_env eff_var in + (* compute inner type and effect *) + let cap_type = Type.tr_type inner_env cap_type in + let in_type = Type.tr_type inner_env in_type in + let in_eff = T.Effct.join (T.Effct.var eff_var) (Env.fresh_gvar env) in + let comp_sch = + { T.sch_targs = [(TNAnon, eff_var)]; + T.sch_named = []; + T.sch_body = + T.Type.t_arrow (T.Scheme.of_type cap_type) in_type (Impure in_eff) + } in + 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 + (res, tp, return_pure eff_req) + | EEffect(lbl, x, body, res_tp) -> let (lbl, lbl_tp, eff_resp1) = infer_type env lbl eff_req in let (eff, delim_tp, delim_eff) = Subtyping.as_label lbl_tp in diff --git a/src/Lang/Surface.ml b/src/Lang/Surface.ml index 2b5abb3c..d6dfc0c9 100644 --- a/src/Lang/Surface.ml +++ b/src/Lang/Surface.ml @@ -266,6 +266,10 @@ and expr_data = (** First-class handler, with return and finally clauses. For each of these clause lists, empty list means the default identity clause *) + | EHandlerFn of def list * expr * match_clause list * match_clause list + (** First-class handler defined on top of a block of definitions. In + contrast to [EHandler], this handler does not create a fresh label. *) + | EEffect of expr option * pattern * expr (** Effectful operation. The only argument is a continuation. Other arguments should be bound using regular lambda abstractions ([EFn]). diff --git a/src/Lang/Unif.mli b/src/Lang/Unif.mli index 7cf001f5..f05ad46b 100644 --- a/src/Lang/Unif.mli +++ b/src/Lang/Unif.mli @@ -438,6 +438,30 @@ and expr_data = (** Body of the finally clause *) } + | EHandlerFn of (** First class handler, defined as a function *) + { eff_var : tvar; + (** Effect variable *) + + cap_type : typ; + (** Type of the capability *) + + in_type : typ; + (** Inner type of a handler: a type of expression that can be run + inside this handler *) + + out_type : typ; + (** Outer type of a handler: a type of the whole handler expression + *) + + comp_var : var; + (** An argument to the body of the handler function. It has type + [{eff_var} -> cap_type ->[eff_var, ...] in_type] *) + + body : expr + (** Body of the handler function. It can use [comp_var] and it should + have type [out_type]. *) + } + | EEffect of expr * var * expr * typ (** Capability of effectful functional operation. It stores dynamic label, continuation variable binder, body, and the type of the whole diff --git a/src/Lang/UnifPriv/Syntax.ml b/src/Lang/UnifPriv/Syntax.ml index 8e4ddcd6..6ead452c 100644 --- a/src/Lang/UnifPriv/Syntax.ml +++ b/src/Lang/UnifPriv/Syntax.ml @@ -133,6 +133,14 @@ and expr_data = fin_var : var; fin_body : expr; } + | EHandlerFn of + { eff_var : tvar; + cap_type : typ; + in_type : typ; + out_type : typ; + comp_var : var; + body : expr + } | EEffect of expr * var * expr * typ | EExtern of string * typ | EAnnot of expr * type_expr diff --git a/src/TypeInference/Expr.ml b/src/TypeInference/Expr.ml index d0ea543b..1575f5d6 100644 --- a/src/TypeInference/Expr.ml +++ b/src/TypeInference/Expr.ml @@ -152,6 +152,57 @@ let infer_expr_type ~tcfix ?app_type env (e : S.expr) = er_constr = er_cap.er_constr @ er_ret.er_constr @ er_fin.er_constr } + | 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)), + er_ret.er_expr)); + er_type = er_ret.er_type; + er_effect = Impure; + er_constr = er_cap.er_constr @ er_ret.er_constr + }} + in + let (fin_x, er_fin) = + MatchClause.tr_finally_clauses ~tcfix ~pos env + (expr_result_type er_handler_body) + fcs + Infer in + let out_tp = expr_result_type er_fin in + { er_expr = make (T.EHandlerFn + { eff_var = eff_var; + cap_type = cap_tp; + in_type = in_tp; + out_type = out_tp; + comp_var = comp_f; + body = + make (T.ELetMono(fin_x, er_handler_body.er_expr, er_fin.er_expr)) + }); + er_type = Infered (T.Type.t_handler eff_var cap_tp in_tp out_tp); + er_effect = Pure; + er_constr = er_handler_body.er_constr @ er_fin.er_constr + } + | EAnnot(e, tp) -> let tp_expr = Type.tr_ttype env tp in let tp = T.TypeExpr.to_type tp_expr in @@ -393,6 +444,58 @@ let check_expr_type ~tcfix env (e : S.expr) tp = Error.fatal (Error.expr_not_handler_ctx ~pos ~pp tp) end + | EHandlerFn(defs, cap, rcs, fcs) -> + begin match Unification.from_handler ~pos env tp with + | H_Handler(b, cap_tp, tp_in, tp_out) -> + (* variable that represents computation in the handler body. *) + let comp_f = Var.fresh ~name:"comp" () 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 + (* 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)), + er_ret.er_expr)); + er_type = er_ret.er_type; + er_effect = Impure; + er_constr = er_cap.er_constr @ er_ret.er_constr + }} + in + let (fin_x, er_fin) = + MatchClause.tr_finally_clauses ~tcfix ~pos env + (expr_result_type er_handler_body) fcs (Check tp_out) in + { er_expr = make (T.EHandlerFn + { eff_var = b; + cap_type = cap_tp; + in_type = tp_in; + out_type = tp_out; + comp_var = comp_f; + body = + make (T.ELetMono(fin_x, er_handler_body.er_expr, er_fin.er_expr)) + }); + er_type = Checked; + er_effect = Pure; + er_constr = er_handler_body.er_constr @ er_fin.er_constr + } + | H_No -> + Error.fatal (Error.expr_not_handler_ctx ~pos ~pp tp) + end + | EEffect(lbl_opt, cont_pat, body) -> let (lbl, delim_tp, lbl_cs) = check_label ~tcfix ~pos env lbl_opt in let cont_tp = T.Type.t_arrow (T.Scheme.of_type tp) delim_tp Impure in diff --git a/src/TypeInference/RecDefs.ml b/src/TypeInference/RecDefs.ml index 5d75e972..ae53222d 100644 --- a/src/TypeInference/RecDefs.ml +++ b/src/TypeInference/RecDefs.ml @@ -305,7 +305,7 @@ let rec guess_rec_fun_type env (e : S.expr) tp = }, T.Impure | EUnit | ENum _ | ENum64 _ | EStr _ | EChr _ | EPoly _ | EApp _ | EDefs _ - | EMatch _ | EHandler _ | EEffect _ | EExtern _ | ERepl _ -> + | EMatch _ | EHandler _ | EHandlerFn _ | EEffect _ | EExtern _ | ERepl _ -> let pp = Env.pp_tree env in { rfb_type = { T.pos = pos; T.pp = pp; T.data = T.TE_Type tp }; rfb_args = []; @@ -597,6 +597,16 @@ let update_rec_body ~pos fds (body : T.poly_fun) = fin_body = update_expr h.fin_body }) + | EHandlerFn h -> + make (T.EHandlerFn { + eff_var = h.eff_var; + cap_type = h.cap_type; + in_type = h.in_type; + out_type = h.out_type; + comp_var = h.comp_var; + body = update_expr h.body + }) + | EAnnot(e, tp) -> make (T.EAnnot(update_expr e, tp)) diff --git a/test/ok/ok0154_handlerfn.fram b/test/ok/ok0154_handlerfn.fram new file mode 100644 index 00000000..c2d84bf4 --- /dev/null +++ b/test/ok/ok0154_handlerfn.fram @@ -0,0 +1,34 @@ +data rec List X = + | [] + | (::) of X, List X + +data ST E X = + { get : Unit ->[E] X + , put : X ->[E] Unit + } + +let hST st0 = + handler ST + { effect get () = fn st => resume st st + , effect put st = fn _ => resume () st + } + return x => fn _ => x + finally c => c st0 + end + +data Writer E X = + { tell : X ->[E] Unit + } + +let hWriter = + handlerfn + handle st with hST [] + in + Writer { tell x = st.put (x :: st.get ()) } + return () => st.get () + end + +let _ : List Int = + handle wr with hWriter in + wr.tell 1; + wr.tell 2 diff --git a/test/ok/ok0155_handlerfnFinally.fram b/test/ok/ok0155_handlerfnFinally.fram new file mode 100644 index 00000000..521c5349 --- /dev/null +++ b/test/ok/ok0155_handlerfnFinally.fram @@ -0,0 +1,27 @@ +data rec List X = + | [] + | (::) of X, List X + +data BT E = + { flip : Unit ->[E] Bool + , fail : {X} -> Unit ->[E] X + } + +let hBT = + handler BT + { effect flip () = resume True || resume False + , effect fail () = False + } + return () => True + end + +let hBT' = + handlerfn + handle bt with hBT + in + bt + return _ :: _ => () + return [] => bt.fail () + finally True => "ok" + finally False => "fail" + end diff --git a/test/ok/ok0156_handlerfnComplex.fram b/test/ok/ok0156_handlerfnComplex.fram new file mode 100644 index 00000000..694146be --- /dev/null +++ b/test/ok/ok0156_handlerfnComplex.fram @@ -0,0 +1,14 @@ +data Exn E = { raise : {X} -> Unit ->[E] X } + +data BT E = + { flip : Unit ->[E] Bool + , fail : {X} -> Unit ->[E] X + } + +let hBT = + handlerfn + handle flip = effect () => resume True; resume False + handle exn = Exn { effect raise () = () } + in + BT { flip, fail = exn.raise } + end diff --git a/test/ok/ok0157_emptyHandlerFn.fram b/test/ok/ok0157_emptyHandlerFn.fram new file mode 100644 index 00000000..6074fdb5 --- /dev/null +++ b/test/ok/ok0157_emptyHandlerFn.fram @@ -0,0 +1 @@ +let hPure = handlerfn in () end diff --git a/test/ok/ok0158_handlerfn.fram b/test/ok/ok0158_handlerfn.fram new file mode 100644 index 00000000..79bc4c0c --- /dev/null +++ b/test/ok/ok0158_handlerfn.fram @@ -0,0 +1,5 @@ +let runH {A} h (f : {E} -> (A ->[E] A) ->[E] _) = + handle x with h in + f x + +let _ = runH (handlerfn in (fn x => x) end) (fn op => op ())