Named handlers #129

dhil · 2025-09-22T13:32:12Z

This patch implements a semantics for named handlers. It is a fairly direct transcription of multi-prompt continuations as found in the literature. This patch adds the following new types and instructions:

handler ts*
- A new reference type for handler names.
resume_with $ct (on ...) : [ts1* (ref null $ct)] -> [ts2*]
- where $ct ~~ func [ts1* (ref $handler)] -> [ts2*]
- and $handler ~~ handler ts2*
- Operationally, it works like resume, but with the small tweak that it generates and passes a unique name to the continuation.
suspend_to $handler $tag : [ts1* (ref null $handler)] -> [ts2*]
- where $handler ~~ handler $ts3
- and $tag ~~ func [ts1*] -> [ts2*]
- It is similar to suspend, but rather than suspending to the nearest enclosing handler, it suspend to a particular given handler.

I've added a few tests too.

This patch implements a semantics for named handlers. It is a fairly direct transcription of multi-prompt continuations as found in the literature. This patch adds the following new types and instructions: * `handler ts*` - A new reference type for handler names. * `resume_with $ct (on ...) : [ts1* (ref null $ct)] -> [ts2*]` - where `$ct ~~ func [ts1* (ref $handler)] -> [ts2*]` - and `$handler ~~ handler ts2*` - Operationally, it works like `resume`, but with the small tweak that it generates and passes a unique name to the continuation. * `suspend_to $handler $tag : [ts1* (ref null $handler)] -> [ts2*]` - where `$handler ~~ handler $ts3` - and `$tag ~~ func [ts1*] -> [ts2*]` - It is similar to `suspend`, but rather than suspending to the nearest enclosing handler, it suspend to a particular given handler. I've added a few tests too.

rossberg · 2025-09-24T09:35:02Z

interpreter/syntax/types.ml

 and array_type = ArrayT of field_type
 and func_type = FuncT of result_type * result_type
 and cont_type = ContT of heap_type
+and handler_type = HandlerT of result_type


To avoid confusion with exn handlers, and to match the Prompt admin instruction, shouldn't this rather be called a prompt_type?

rossberg · 2025-09-24T09:37:54Z

interpreter/binary/decode.ml

  | -0x17 -> (Null, ExnHT)
  | -0x18 -> (Null, ContHT)
+  | -0x19 -> (Null, HandlerHT)
+  | -0x1a -> (Null, NoHandlerHT)


It's getting crowded here...

rossberg · 2025-09-24T09:41:53Z

interpreter/valid/match.ml

    | DefArrayT _, ArrayHT -> true
    | DefFuncT _, FuncHT -> true
    | DefContT _, ContHT -> true
+    | DefHandlerT _, HandlerHT -> true


Shouldn't there be a new case for DefHandlerT in match_str_type as well?

rossberg · 2025-09-24T09:48:06Z

interpreter/valid/valid.ml

+         let FuncT (ts3, ts4) =
+          match hrt with
+          | Some rt ->
+            let FuncT (ts3, ts4) = func_type_of_tag_type c (tag c x1) x1.at in
+            FuncT (ts3, ts4 @ [RefT rt])
+          | None -> func_type_of_tag_type c (tag c x1) x1.at
+        in


Suggested change

let FuncT (ts3, ts4) =

match hrt with

| Some rt ->

let FuncT (ts3, ts4) = func_type_of_tag_type c (tag c x1) x1.at in

FuncT (ts3, ts4 @ [RefT rt])

| None -> func_type_of_tag_type c (tag c x1) x1.at

in

let FuncT (ts3, ts4') = func_type_of_tag_type c (tag c x1) x1.at in

let ts4 = ts4' @ match hrt with Some rt -> [RefT rt] | None -> [] in

rossberg · 2025-09-24T09:49:28Z

interpreter/valid/valid.ml

+  | SuspendTo (x, y) ->
+    let _hty = handler_type c x in
+    let tag = tag c y in
+    let FuncT (ts1, ts2) = func_type_of_tag_type c tag x.at in


Suggested change

let FuncT (ts1, ts2) = func_type_of_tag_type c tag x.at in

let FuncT (ts1, ts2) = func_type_of_tag_type c tag y.at in

rossberg · 2025-09-24T10:01:09Z

interpreter/exec/eval.ml

+        let args, href =
+          match args with
+          | Ref r :: rest -> rest, r
+          | _ -> Crash.error e.at "type mismatch at suspend to"


Suggested change

| _ -> Crash.error e.at "type mismatch at suspend to"

| _ -> Crash.error e.at "type mismatch at suspend_to"

rossberg · 2025-09-24T10:02:58Z

interpreter/exec/eval.ml

+        let name =
+          Ref (HandlerRef (ref (Some Name)))
+        in


Suggested change

let name =

Ref (HandlerRef (ref (Some Name)))

in

let name = Ref (HandlerRef (ref (Some Name))) in

rossberg · 2025-09-24T10:08:49Z

interpreter/exec/eval.ml

+      | ResumeWith (x, xls), Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
+        let hs = handle_table c xls in
+        let args, vs' = i32_split (Int32.sub n 1l) vs e.at in
+        let exception Name in


Instead of abusing exceptions, can we define our own extensible datatype prompt_name above and extend that here? Unfortunately, this:

Suggested change

let exception Name in

let type prompt_name += Name in

doesn't work, you'll have to do

Suggested change

let exception Name in

let module N = struct type prompt_name += Name end in

and use N.name.

rossberg · 2025-09-24T10:14:41Z

interpreter/exec/eval.ml

-       let args = cont' :: vs1 in
-       cont := None;
-       vs' @ vs, [Prompt (hso, ctxt (args, [])) @@ e.at]
+    | Prompt (Some h, (hs, _), (vs', {it = Suspending (tagt, vs1, None, Some (HandlerRef ({contents = Some h'} as href)), ctxt); at} :: es')), vs


I wonder if we can avoid doubling the rules by factoring out an auxiliary

let matches_name name1 name2 = match name1, name2 with | None, _-> true | _, None -> false | Some n1, Some n2 -> n1 == n2

rossberg · 2025-09-24T10:19:00Z

interpreter/exec/eval.ml

+      [Ref (ContRef (ref (Some (Int32.add (Lib.List32.length ts) 1l, ctxt'))))] @ vs1 @ vs,
+      [Plain (Br (List.assq tagt hs)) @@ e.at]
+
+    | Prompt (None, ((_, hs) as hso), (vs', {it = Suspending (tagt, vs1, Some (ar, ContRef ({contents = Some (_, ctxt)} as cont)), None, ctxt'); at} :: es')), vs


Isn't this missing an equivalent rule for bubbling a named Suspending? (But see previous comment about avoiding duplication.)

rossberg reviewed Sep 24, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Named handlers #129

Named handlers #129

Uh oh!

dhil commented Sep 22, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

rossberg Sep 24, 2025

Uh oh!

Uh oh!

	let FuncT (ts1, ts2) = func_type_of_tag_type c tag x.at in
	let FuncT (ts1, ts2) = func_type_of_tag_type c tag y.at in

	\| _ -> Crash.error e.at "type mismatch at suspend to"
	\| _ -> Crash.error e.at "type mismatch at suspend_to"

	let exception Name in
	let module N = struct type prompt_name += Name end in

Named handlers #129

Are you sure you want to change the base?

Named handlers #129

Uh oh!

Conversation

dhil commented Sep 22, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!