diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml
index e1f7dbd1..ea542159 100644
--- a/src/DblParser/Desugar.ml
+++ b/src/DblParser/Desugar.ml
@@ -136,6 +136,24 @@ let rec tr_type_expr (tp : Raw.type_expr) =
     make (TEffect (List.map tr_type_expr tps))
   | TApp(tp1, tp2) ->
     make (TApp(tr_type_expr tp1, tr_type_expr tp2))
+  | THandler (effct_opt, cap_tp, in_comp, out_comp) ->
+      let cap_type = tr_type_expr cap_tp in
+      let in_eff_opt, in_type = tr_eff_type in_comp in
+      let in_eff =
+        Option.value in_eff_opt ~default:(make (TEffect [ make TWildcard ]))
+      in
+      let out_eff_opt, out_type = tr_eff_type out_comp in
+      let out_eff =
+        Option.value out_eff_opt ~default:(make (TEffect [ make TWildcard ]))
+      in
+      make (THandler {
+        effct = effct_opt;
+        cap_type;
+        in_type;
+        in_eff;
+        out_type;
+        out_eff;
+      })
   | TRecord _ | TTypeLbl _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
@@ -178,7 +196,7 @@ and tr_scheme_expr (tp : Raw.type_expr) =
       Error.fatal (Error.impure_scheme pos)
     end
 
-  | TWildcard | TVar _ | TArrow _ | TEffect _ | TApp _ ->
+  | TWildcard | TVar _ | TArrow _ | TEffect _ | TApp _ | THandler _ ->
     { sch_pos  = pos;
       sch_args = [];
       sch_body = tr_type_expr tp
@@ -214,7 +232,7 @@ and tr_type_var (tp : Raw.type_expr) =
     let k = Option.value ka ~default:(make KWildcard) in
     (x, k)
   | TVar ({data = NPSel _; _}, _) | TWildcard | TArrow _ | TEffect _ | TApp _
-  | TRecord _ | TTypeLbl _ ->
+  | THandler _ | TRecord _ | TTypeLbl _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
 (** Translate a type expression as a type parameter *)
@@ -240,7 +258,7 @@ let rec tr_named_type_arg (tp : Raw.type_expr) =
   | TTypeLbl tp -> make (TNAnon, tr_type_arg tp)
   | TWildcard -> make (TNAnon, make (TA_Wildcard))
   | TVar ({data = NPSel _; _}, _) | TArrow _ | TEffect _ | TApp _
-  | TRecord _ ->
+  | THandler _ | TRecord _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
 (** Translate a left-hand-side of the type definition. The additional
@@ -250,7 +268,7 @@ let rec tr_type_def (tp : Raw.type_expr) args =
   | TVar ({data = NPName x; _}, _) -> TD_Id(x, args)
   | TApp(tp1, tp2) -> tr_type_def tp1 (tp2 :: args)
   | TVar ({data = NPSel _; _}, _) | TWildcard | TParen _ | TArrow _
-  | TEffect _ | TRecord _ | TTypeLbl _ ->
+  | TEffect _ | THandler _ | TRecord _ | TTypeLbl _ ->
     Error.fatal (Error.desugar_error tp.pos)
 
 let tr_ctor_decl (d : Raw.ctor_decl) =
diff --git a/src/DblParser/Raw.ml b/src/DblParser/Raw.ml
index 9b3f8c43..60704801 100644
--- a/src/DblParser/Raw.ml
+++ b/src/DblParser/Raw.ml
@@ -120,6 +120,9 @@ and type_expr_data =
   | TTypeLbl of type_expr
     (** Label of anonymous type parameter of ADT *)
 
+  | THandler of tvar option * type_expr * type_expr * type_expr
+    (** Handler type: effect binding, capability, input comp, output comp *)
+
 (** Field of record-like type *)
 and ty_field = (type_expr, type_expr) field_data node
 
diff --git a/src/DblParser/YaccParser.mly b/src/DblParser/YaccParser.mly
index 6cdf778d..1f3b24a7 100644
--- a/src/DblParser/YaccParser.mly
+++ b/src/DblParser/YaccParser.mly
@@ -168,8 +168,19 @@ ty_expr_simple
 | UNDERSCORE { make TWildcard }
 | SBR_OPN effct SBR_CLS { make ($2).data }
 | CBR_OPN ty_field_list CBR_CLS { make (TRecord $2) }
+| KW_HANDLER effct_bind ty_expr KW_IN ty_expr ARROW2 ty_expr
+  { make (THandler ($2, $3, $5, $7)) }
+| KW_HANDLER effct_bind ty_expr ARROW2 ty_expr
+  { make (THandler ($2, $3, $5, $5)) }
 ;
 
+effct_bind
+: CBR_OPN UID CBR_CLS { Some $2 }
+| CBR_OPN UNDERSCORE CBR_CLS { None }
+| /* empty */         { None }
+;
+
+
 /* ------------------------------------------------------------------------- */
 
 type_annot
diff --git a/src/Lang/Surface.ml b/src/Lang/Surface.ml
index 2b5abb3c..4d3413c0 100644
--- a/src/Lang/Surface.ml
+++ b/src/Lang/Surface.ml
@@ -92,7 +92,7 @@ and type_expr_data =
     (** Effectful function: the last parameter is an effect *)
 
   | THandler of (** First-class handler *)
-    { effct    : tvar;
+    { effct    : tvar option;
         (** Effect variable bound by this handler (it's bound in [cap_type],
           [in_type], and [in_eff] *)
 
diff --git a/src/Lang/UnifCommon/Pretty.ml b/src/Lang/UnifCommon/Pretty.ml
index 42e50d22..fdac0300 100644
--- a/src/Lang/UnifCommon/Pretty.ml
+++ b/src/Lang/UnifCommon/Pretty.ml
@@ -354,25 +354,38 @@ let rec print_type env (tp : type_tree) prec =
 
   | PP_THandler h ->
     paren env prec 0 (fun () ->
-      let name = gen_tvar_name (fun n -> fresh_for_type env n tp) "E" in
+      let name =
+        match Env.lookup_tvar env h.eff_var with
+        | Found name -> name
+        | Anon(name, _) -> name
+        | Unbound _ -> gen_tvar_name (fun n -> fresh_for_type env n tp) "E"
+      in
       let env1 = Env.add_tvar env name h.eff_var in
       Env.print_string env "handler ";
+      Env.print_string env "{";
       Env.print_string env name;
-      Env.print_string env " of ";
+      Env.print_string env "} ";
       print_type env1 h.cap_tp 1;
-      Env.print_string env " with [";
-      print_effect_body env1 h.in_eff;
-      Env.print_string env "] ";
-      print_type env1 h.in_tp 1;
-      begin match h.out_eff with
-      | [ PP_EffWildcard ] ->
-        Env.print_string env " ->> "
-      | effs ->
-        Env.print_string env " ->[";
-        print_effect_body env effs;
-        Env.print_string env "] "
-      end;
-      print_type env h.out_tp 1)
+      let print_comp env eff tp =
+        begin match eff with
+        | [ PP_EffWildcard ] -> ()
+        | _ ->
+          Env.print_string env " [";
+          print_effect_body env eff;
+          Env.print_string env "]"
+        end;
+        Env.print_string env " ";
+        print_type env tp 1
+      in
+      if h.in_eff = h.out_eff && h.in_tp = h.out_tp then (
+        Env.print_string env " =>";
+        print_comp env h.out_eff h.out_tp
+      ) else (
+        Env.print_string env " in";
+        print_comp env1 h.in_eff h.in_tp;
+        Env.print_string env " =>";
+        print_comp env h.out_eff h.out_tp
+      ))
 
   | PP_TEffect eff -> print_effect env eff prec
 
diff --git a/src/TypeInference/Type.ml b/src/TypeInference/Type.ml
index 5543f961..8ddd92dc 100644
--- a/src/TypeInference/Type.ml
+++ b/src/TypeInference/Type.ml
@@ -50,7 +50,11 @@ let rec infer_kind env (tp : S.type_expr) =
 
   | THandler { effct; cap_type; in_type; in_eff; out_type; out_eff } ->
     let (in_env, _) = Env.enter_scope env in
-    let (in_env, eff_var) = Env.add_tvar ~pos in_env effct T.Kind.k_effect in
+    let (in_env, eff_var) =
+      match effct with
+      | Some effct -> Env.add_tvar ~pos in_env effct T.Kind.k_effect
+      | None -> Env.add_anon_tvar ~pos ~name:"E" in_env T.Kind.k_effect
+    in
     let cap_type = tr_ttype  in_env cap_type in
     let in_type  = tr_ttype  in_env in_type in
     let in_eff   = tr_effect in_env in_eff in