Return and finally clauses in first class handlers

Return and finally clauses now are attached to first class handlers,
making possible to define more intuitive first class handlers for e.g.
state or backtracking. The delimiter's type and effect are not visible
in the type of first-class-handlers, therefore, the dynamic labels of
handlers do not work.

src/DblParser/Desugar.ml

@@ -542,7 +542,10 @@ and tr_expr (e : Raw.expr) =
     tr_expr_app (tr_expr e1) es
   | EDefs(defs, e) -> make (EDefs(tr_defs defs, tr_expr e))
   | EMatch(e, cls) -> make (EMatch(tr_expr e, List.map tr_match_clause cls))
-  | EHandler h     -> make (EHandler (tr_expr h))
+  | EHandler(h, hcs) ->
+    let e = tr_expr h in
+    let (rcs, fcs) = map_h_clauses tr_h_clause hcs in
+    make (EHandler(e, rcs, fcs))
   | EEffect(es, rp_opt, e) ->
     let (pos, rp) =
       match rp_opt with
@@ -728,18 +731,20 @@ and tr_def ?(public=false) (def : Raw.def) =
     ]
   | DLabel(pub, pat) ->
     let public = public || pub in
-    let (eff_opt, pat) = tr_label_pattern ~public pat in
+    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
     [ make (DLabel (eff_opt, pat)) ]
-  | DHandle(pub, pat, h, hcs) ->
+  | DHandle(pub, pat, body, hcs) ->
     let public = public || pub in
-    let (lbl_opt, eff_opt, pat)  = tr_handle_pattern ~public pat in
-    let body = { h with data = EHandler(tr_expr h) } in
-    [ make_handle ~pos:def.pos lbl_opt eff_opt pat body hcs ]
-  | DHandleWith(pub, pat, e, hcs) ->
+    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
+    let body = tr_expr body in
+    let (rcs, fcs) = map_h_clauses tr_h_clause hcs in
+    let body = { body with data = EHandler(body, rcs, fcs) } in
+    [ make (DHandlePat(eff_opt, pat, body)) ]
+  | DHandleWith(pub, pat, body) ->
     let public = public || pub in
-    let (lbl_opt, eff_opt, pat)  = tr_handle_pattern ~public pat in
-    let body = tr_expr e in
-    [ make_handle ~pos:def.pos lbl_opt eff_opt pat body hcs ]
+    let (eff_opt, pat) = tr_pattern_with_eff_opt ~public pat in
+    let body = tr_expr body in
+    [ make (DHandlePat(eff_opt, pat, body)) ]
   | DModule(pub, x, defs) ->
     let public = public || pub in
     [ make (DModule(public, x, tr_defs defs)) ]
@@ -765,42 +770,17 @@ and tr_pattern_with_fields ~public (pat : Raw.expr) =
   | _ ->
     (None, tr_pattern ~public pat)
 
-and tr_label_pattern ~public (pat : Raw.expr) =
+and tr_pattern_with_eff_opt ~public (pat : Raw.expr) =
   let (flds_opt, pat) = tr_pattern_with_fields ~public pat in
-  (Option.map (tr_label_fields ~public) flds_opt, pat)
+  (Option.map (tr_eff_opt_fields ~public) flds_opt, pat)
 
-and tr_handle_pattern ~public (pat : Raw.expr) =
-  let (flds_opt, pat) = tr_pattern_with_fields ~public pat in
-  match flds_opt with
-  | Some flds ->
-    let (lbl_opt, eff_opt) = tr_handle_fields ~public flds in
-    (lbl_opt, eff_opt, pat)
-  | None -> (None, None, pat)
-
-and tr_label_fields ~public flds =
+and tr_eff_opt_fields ~public flds =
   match flds with
   | [] -> assert false
   | [{ data = FldEffectVal tp; _ }] -> tr_type_arg ~public tp
   | { data = FldEffectVal _; _} :: fld :: _ | fld :: _ ->
     Error.fatal (Error.desugar_error fld.pos)
 
-and tr_handle_fields ~public flds =
-  match flds with
-  | [] -> assert false
-  | [{ data = FldNameVal(NLabel, e); _ }] ->
-    (Some (tr_expr e), None)
-  | [{ data = FldEffectVal eff; _ }] ->
-    (None, Some (tr_type_arg ~public eff))
-  | [{ data = FldNameVal(NLabel, e); _ }; { data = FldEffectVal eff; _ }]
-  | [{ data = FldEffectVal eff; _ }; { data = FldNameVal(NLabel, e); _ }] ->
-    (Some (tr_expr e), Some (tr_type_arg ~public eff))
-  | { data=FldNameVal(NLabel, _); _} :: { data=FldEffectVal _; _ } :: fld :: _
-  | { data=FldEffectVal _; _ } :: { data=FldNameVal(NLabel, _); _} :: fld :: _
-  | { data=FldNameVal(NLabel, _); _} :: fld :: _
-  | { data=FldEffectVal _; _ } :: fld :: _
-  | fld :: _ ->
-    Error.fatal (Error.desugar_error fld.pos)
-
 and tr_h_clause (hc : Raw.h_clause) =
   let make data = { hc with data = data } in
   match hc.data with
@@ -809,19 +789,7 @@ and tr_h_clause (hc : Raw.h_clause) =
   | HCFinally(pat, body) ->
     Either.Right (make (Clause(tr_pattern ~public:false pat, tr_expr body)))
 
-and make_handle ~pos lbl_opt eff_opt pat body hcs =
-  let make data = { pos; data } in
-  let (rcs, fcs) = map_h_clauses tr_h_clause hcs in
-  make (DHandlePat
-    { label       = lbl_opt;
-      effect      = eff_opt;
-      cap_pat     = pat;
-      capability  = body;
-      ret_clauses = rcs;
-      fin_clauses = fcs
-    })
-
-(** Returns: list of explicit type adnotations with fresh type variable names
+(** Returns: list of explicit type annotations with fresh type variable names
     and a function that given a field name returns piece of code that
     represents pattern which pulls out this variable, making it easy to use in
     generated code *)

src/DblParser/Raw.ml

@@ -195,7 +195,7 @@ and expr_data =
   | EMatch of expr * match_clause list
     (** Pattern-matching *)
 
-  | EHandler of expr
+  | EHandler of expr * h_clause list
     (** First-class handler *)
 
   | EEffect of expr list * expr option * expr
@@ -264,7 +264,7 @@ and def_data =
   | DHandle of is_public * expr * expr * h_clause list
     (** Effect handler *)
 
-  | DHandleWith of is_public * expr * expr * h_clause list
+  | DHandleWith of is_public * expr * expr
     (** Effect handler, with first-class handler *)
 
   | DMethod of is_public * expr * expr

src/DblParser/YaccParser.mly

@@ -263,7 +263,6 @@ expr
 | KW_FN expr_250_list1 ARROW2 expr { make (EFn($2, $4))   }
 | KW_EFFECT expr_250_list effect_resumption_opt ARROW2 expr
     { make (EEffect($2, $3, $5)) }
-| KW_HANDLER expr { make (EHandler $2) }
 | expr_0 { $1 }
 ;
 
@@ -272,7 +271,6 @@ expr_no_comma
 | KW_FN expr_250_list1 ARROW2 expr_no_comma { make (EFn($2, $4))   }
 | KW_EFFECT expr_250_list effect_resumption_opt ARROW2 expr_no_comma
     { make (EEffect($2, $3, $5)) }
-| KW_HANDLER expr_no_comma { make (EHandler $2) }
 | expr_0_no_comma { $1 }
 ;
 
@@ -454,6 +452,7 @@ expr_simple
 | KW_MATCH expr KW_WITH KW_END   { make (EMatch($2, [])) }
 | 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)) }
 | 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)}
@@ -523,8 +522,8 @@ def
 | pub KW_LABEL rec_opt expr_70 { make_def $3 (DLabel($1, $4)) }
 | pub KW_HANDLE rec_opt expr_70 EQ expr h_clauses
     { make_def $3 (DHandle($1, $4, $6, $7)) }
-| pub KW_HANDLE rec_opt expr_70 KW_WITH expr h_clauses
-    { make_def $3 (DHandleWith($1, $4, $6, $7)) }
+| pub KW_HANDLE rec_opt expr_70 KW_WITH expr
+    { make_def $3 (DHandleWith($1, $4, $6)) }
 | pub KW_METHOD rec_opt expr_70 EQ expr { make_def $3 (DMethod($1, $4, $6)) }
 | pub KW_METHOD KW_FN var_id { make (DMethodFn($1, $4, $4)) }
 | pub KW_METHOD KW_FN var_id EQ var_id { make (DMethodFn($1, $4, $6)) }

src/Lang/Surface.ml

@@ -226,8 +226,9 @@ and expr_data =
   | EMatch of expr * match_clause list
     (** Pattern-matching *)
 
-  | EHandler of expr
-    (** First-class handler *)
+  | EHandler of expr * match_clause list * match_clause list
+    (** First-class handler, with return and finally clauses. For each of these
+      clause list, empty list means the default identity clause *)
 
   | EEffect of arg * expr
     (** Effectful operation. The only argument is a continuation. Other
@@ -266,26 +267,13 @@ and def_data =
     (** Creating a new label. Optional type argument binds newly created
       effect. *)
 
-  | DHandlePat of (* Effect handler combined with pattern matching *)
-    { label   : expr option;
-      (** Effect label of the handled effect. [None] means that handler is
-        lexical and generates its own label. *)
-
-      effect : type_arg option;
-      (** Optional name for the handled effect *)
-
-      cap_pat : pattern;
-      (** Pattern matched against the effect capability *)
-
-      capability : expr;
-      (** An expression providing capability to this handler *)
-
-      ret_clauses : match_clause list;
-      (** List of return clauses. Empty list means the default clause. *)
-
-      fin_clauses : match_clause list
-      (** List of finally clauses. Empty list means the default clause. *)
-    }
+  | DHandlePat of type_arg option * pattern * expr
+    (** Effect handler combined with pattern matching. In
+      [DHandlePat(eff, pat, body)] the meaning of parameters is the following.
+      - [eff]  -- Optional name for the handled effect.
+      - [pat]  -- Pattern matched against the effect capability.
+      - [body] -- An expression that should evaluate to fist class handler,
+          providing the capability of the handled effect. *)
 
   | DImplicit of iname * named_type_arg list * scheme_expr
     (** Declaration of implicit. The second parameter is a list of types

src/Lang/Unif.ml

@@ -96,17 +96,20 @@ and expr_data =
   | EData       of data_def list * expr
   | EMatchEmpty of expr * expr * typ * effrow
   | EMatch      of expr * match_clause list * typ * effrow
-  | EHandle     of
-    { label      : expr;
-      effect     : effect;
-      cap_var    : var;
-      body       : expr;
-      capability : expr;
-      ret_var    : var;
-      ret_body   : expr;
-      result_tp  : typ;
-      result_eff : effrow }
-  | EHandler    of tvar * var * typ * effrow * expr
+  | EHandle     of tvar * var * typ * expr * expr
+  | EHandler    of
+    { label     : var;
+      effect    : tvar;
+      delim_tp  : typ;
+      delim_eff : effect;
+      cap_type  : typ;
+      cap_body  : expr;
+      ret_var   : var;
+      body_tp   : typ;
+      ret_body  : expr;
+      fin_var   : var;
+      fin_body  : expr;
+    }
   | EEffect     of expr * var * expr * typ
   | EExtern     of string * typ
   | ERepl       of (unit -> expr) * typ * effrow

src/Lang/Unif.mli

@@ -208,44 +208,51 @@ and expr_data =
   | EMatch of expr * match_clause list * typ * effrow
     (** Pattern-matching. It stores type and effect of the whole expression. *)
 
-  | EHandle of (** Handler *)
-    { label : expr;
-      (** Label of the handler *)
+  | EHandle of tvar * var * typ * expr * expr
+    (** Handling construct. In [EHandle(a, x, tp, e1, e2)] the meaning of
+      parameters is the following.
+      - [a]  -- effect variable that represent introduced effect
+      - [x]  -- capability variable
+      - [tp] -- type of the capability
+      - [e1] -- expression that should evaluate to first-class handler
+      - [e2] -- body of the handler *)
+
+  | EHandler of (** First class handler *)
+    { label     : var;
+      (** Variable, that binds the runtime-label *)
+
+      effect    : tvar;
+      (** Effect variable *)
 
-      effect : effect;
-      (** Effect handled by the label *)
+      delim_tp  : typ;
+      (** Type of the delimiter *)
 
-      cap_var : var;
-      (** Variable that binds effect capability *)
+      delim_eff : effect;
+      (** Effect of the delimiter *)
 
-      body : expr;
-      (** Handled expression *)
+      cap_type  : typ;
+      (** Type of the capability *)
 
-      capability : expr;
-      (** An expression providing capability to this handler *)
+      cap_body  : expr;
+      (** An expression that should evaluate to effect capability. It can use
+        [label] and [effect]. It should be pure and have type [cap_type]. *)
 
-      ret_var : var;
+      ret_var   : var;
       (** An argument to the return clause *)
 
-      ret_body : expr;
-      (** A body of the return clause *)
+      body_tp   : typ;
+      (** Type of the handled expression. It is also a type of an argument
+        [ret_var] to the return clause *)
 
-      result_tp : typ;
-      (** The type of the whole handler *)
+      ret_body  : expr;
+      (** Body of the return clause *)
 
-      result_eff : effrow }
-      (** The effect of the whole handler *)
+      fin_var   : var;
+      (** An argument to the finally clause. It has type [delim_tp] *)
 
-  | EHandler of tvar * var * typ * effrow * expr
-    (** First-class handler. In [EHandler(a, lx, tp, eff, h)] the meaning of
-      parameter is the following:
-      - [a] -- binder of an effect variable (of kind [effect]). The variable
-        is bound in other arguments of [EHandler] expression.
-      - [lx] -- label variable bound by the handler. Its type should be
-        [TLabel(Effect.singleton a, tp, eff)].
-      - [tp] -- type of the delimiter ([EHandle]).
-      - [eff] -- effect of the delimiter.
-      - [h] -- body of the handler. *)
+      fin_body  : expr;
+      (** Body of the finally clause *)
+    }
 
   | EEffect of expr * var * expr * typ
     (** Capability of effectful functional operation. It stores dynamic label,
@@ -500,11 +507,13 @@ module Type : sig
     | TArrow of scheme * typ * effrow
       (** Impure arrow *)
 
-    | THandler of tvar * typ * typ * effrow
-      (** First class handler. In [THandler(a, tp, tp0, eff0)]:
-        - [a] is a variable bound in [tp], [tp0], and [eff0];
+    | THandler of tvar * typ * typ * effrow * typ * effect
+      (** First class handler. In [THandler(a, tp, itp, ieff, otp, oeff)]:
+        - [a] is a variable bound in [tp], [itp], and [ieff];
         - [tp] is a type of provided capability;
-        - [tp0] and [eff0] are type and effects of the whole delimiter. *)
+        - [itp] and [ieff] are type and effects of handled expression.
+          The variable [a] in [ieff] can be omitted.
+        - [otp] and [oeff] are type and effects of the whole handler. *)
 
     | TLabel of effect * typ * effrow
       (** Type of first-class label. It stores the effect of the label and
@@ -538,7 +547,7 @@ module Type : sig
     | Whnf_Arrow of scheme * typ * effrow
       (** Impure arrow *)
 
-    | Whnf_Handler of tvar * typ * typ * effrow
+    | Whnf_Handler   of tvar * typ * typ * effrow * typ * effrow
       (** Handler type *)
 
     | Whnf_Label of effect * typ * effrow
@@ -563,7 +572,7 @@ module Type : sig
   val t_arrow : scheme -> typ -> effrow -> typ
 
   (** Type of first-class handlers *)
-  val t_handler : tvar -> typ -> typ -> effrow -> typ
+  val t_handler : tvar -> typ -> typ -> effrow -> typ -> effrow -> typ
 
   (** Type of first-class label *)
   val t_label : effect -> typ -> effrow -> typ

src/Lang/UnifPriv/Subst.ml

@@ -98,10 +98,15 @@ and in_type_rec sub tp =
     t_pure_arrow (in_scheme_rec sub sch) (in_type_rec sub tp2)
   | TArrow(sch, tp2, eff) ->
     t_arrow (in_scheme_rec sub sch) (in_type_rec sub tp2) (in_type_rec sub eff)
-  | THandler(a, tp, tp0, eff0) ->
+  | THandler(a, tp, itp, ieff, otp, oeff) ->
+    let otp  = in_type_rec sub otp in
+    let oeff = in_type_rec sub oeff in
     let (sub, a) = add_tvar sub a in
     t_handler a (in_type_rec sub tp)
-      (in_type_rec sub tp0) (in_type_rec sub eff0)
+      (in_type_rec sub itp)
+      (in_type_rec sub ieff)
+      otp
+      oeff
   | TLabel(eff, tp0, eff0) ->
     t_label (in_type_rec sub eff) (in_type_rec sub tp0) (in_type_rec sub eff0)
   | TApp(tp1, tp2) ->