Skip to content

Concrete syntax for handler types #337

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
JakubZojdzik wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Concrete syntax for handler types #337

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
dc29e18
to surface
JakubZojdzik Apr 12, 2026
5e3cf74
Fix pretty printer, allow wildcard
JakubZojdzik Apr 12, 2026
10fff97
Fix THandler type
JakubZojdzik Apr 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 22 additions & 4 deletions src/DblParser/Desugar.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
Expand All @@ -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
Expand All @@ -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) =
Expand Down
3 changes: 3 additions & 0 deletions src/DblParser/Raw.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
11 changes: 11 additions & 0 deletions src/DblParser/YaccParser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)) }
;
Comment on lines +171 to 175
Copy link
Copy Markdown
Member

@ppolesiuk ppolesiuk May 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree. It would be nice to have some tests for the new feature.


effct_bind
: CBR_OPN UID CBR_CLS { Some $2 }
| CBR_OPN UNDERSCORE CBR_CLS { None }
| /* empty */ { None }
Comment on lines 175 to +180
Copy link
Copy Markdown
Member

@ppolesiuk ppolesiuk May 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree. Proposed change should remove shift-reduce conflicts, or at least reduce their number.

;


/* ------------------------------------------------------------------------- */

type_annot
Expand Down
2 changes: 1 addition & 1 deletion src/Lang/Surface.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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] *)

Expand Down
43 changes: 28 additions & 15 deletions src/Lang/UnifCommon/Pretty.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Comment on lines +357 to +362
Copy link
Copy Markdown
Member

@ppolesiuk ppolesiuk May 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is no point in looking up the environment here, as the variable is not bound in this scope (it would be bound in the next line). I know, that asking the environment for a name that is meaningful for the programmer is tempting, but the binding structure doesn't work that way. Such an programmer-friendly name could be stored in a variable metadata, but we could do this a separate issue.

Suggested change
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 name = 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 (
Copy link
Copy Markdown
Member

@ppolesiuk ppolesiuk May 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To be fully correct, we should also check, that h.eff_var doesn't appear in inner type and effect, because handler {E} T in [E] _ => [E] _ doesn't mean the same as handler {E} T => [E] _. However, such a case is extremely rare, and I'm not able to write an example in the concrete syntax that would exhibit this error.

Copy link
Copy Markdown
Member

@ppolesiuk ppolesiuk May 4, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Moreover, structural equality is bad (for many reasons). Maybe a custom function that checks α-equivalence modulo permutations of effects, and understands, that the scope of compared types/effects are different would solve all the problems.

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

Expand Down
6 changes: 5 additions & 1 deletion src/TypeInference/Type.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading