First class handlers from handling functions

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

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

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;

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)}

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

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]).

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

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

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

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))