I started playing with effect handlers and wondered if they could be used to implement toplevel breakpoints. It’s a big hack and probably unsound at the moment, but it works and here’s an example interaction:
let arr =
let fact n =
let arr = Array.make (n+1) 1 in
let rec loop i =
if i <= n then begin
Break.break ["i", i; "arr", arr];
arr.(i) <- arr.(i-1) * i;
loop (i+1)
end
in
(loop 1; arr)
in
fact 5;;
# (* We hit a breakpoint and obtain the continuation k *)
k ();;
- : bool = true
# (* the bools are leaking from the execute_phrase function
* inside the toplevel *)
k ();;
- : bool = true
# i;;
- : int = 3
# arr;;
- : int array = [|1; 1; 2; 1; 1; 1|]
# (* let's disturb the computation of factorials *)
arr.(i-1) <- 42;;
- : unit = ()
# k ();;
- : bool = true
# (* btw: here the user is like a scheduler for yield-based async *)
k ();;
- : bool = true
# k ();;
val arr : int array = [|1; 1; 42; 126; 504; 2520|]
- : bool = true
Currently I don’t try to clean up bindings or values, which is a source of unsoundness. After the last k () we got two results: First the computation of let arr ... finished, and then the computation of k () finished. But k is a part of the execution of let arr ..., so these two executions “intersect” without one being contained in the other. This makes the question of what should the current variable bindings be complicated. Setting the bindings at end of execution is futile, when a continuation may in such a way leak bindings from breakpoint time.
Possibly a stack discipline for the execution of phrases is required to make the environments behave properly: at the end of executing a phrase we cancel (with another effect, maybe) other executions which “depend” on the current execution (evaluate the k obtained from a breakpoint in the current execution). This should eliminate these “intersections” and we could throw out the bindings added by the cancelled executions.
I haven’t tried anything with polymorphism yet, but type variables should probably be changed into abstract types inside the binders.
Well, this might have been unnecessary, as most of it can be done properly in userspace (with more syntactic overhead).
open EffectHandlers
open Deep
type ('a, 'b) res =
| Bp of 'a * ((unit, ('a, 'b) res) continuation)
| Fin of 'b
module type P1 = sig val i : int val arr : int array end
type payload = P1 of (module P1)
type _ eff += Break : payload -> unit eff
let arr () =
let fact n =
let arr = Array.make (n+1) 1 in
let rec loop i =
if i <= n then begin
perform (Break (P1 (module struct let i = i let arr = arr end)));
arr.(i) <- arr.(i-1) * i;
loop (i+1)
end
in
(loop 1; arr)
in
fact 5;;
let with_break th =
try_with (fun () -> Fin (th ())) ()
{ effc = fun (type a) (e : a eff) ->
match e with
| Break p -> Some (fun (k : (a,_) continuation) -> Bp (p, k))
| _ -> None }
let cont = function
| Bp (_, k) -> continue k ()
| Fin _ -> failwith "computation finished, cannot continue"
let get = function
| Bp (r, _) -> r
| Fin _ -> failwith "computation finished, no breakpoint payload"
let get1 r = match get r with P1 m -> m
# let r = with_break arr;;
val r : (payload, int array) res = Bp (P1 <module>, <abstr>)
# open (val get1 r);;
val i : int = 1
val arr : int array = [|1; 1; 1; 1; 1; 1|]
The main pain point is having to define the payload types. In basic cases the payload type could be just a simple polymorphic variant. It would be nice if it could be completely inferred, but it’s unlikely as Break has to have a statically known argument.
With a bit of help from tooling (ppxes for code generation and shorthands in the toplevel), this could be better than printf debugging.
This reminds me of the idea of high-level stack inspection for debugging and security (articulated for instance in Clements’ PhD thesis Portable and high-level access to the stack with Continuation Marks; here’s another more recent paper from the Racket people that might be relevant). One can ask whether a PPX can provide high-level stack inspection or if one needs support from the compiler for that. It’s nice to experiment.
A few years ago someone asked whether there could be a use to untyped algebraic effects in OCaml (in the sense that they do not appear in the effect annotation in function types). I proposed debugging as an example. Someone suggested that it is not too hard to adapt the interface types of all functions in the call chain to add the appropriate effect annotation (and remove it afterwards), but I was not convinced.