The relationship between call/cc, shift/reset, and effect handlers

Learning
1

Tonight I stumbled upon a cute implementation of an aborting lazy stream using call/cc and foldr:

let validate xs =
  call/cc (λk → Right (foldr (λx xs → if alnum? x then x ∷ xs else k (Left x)) ◻ xs))

...

case validate "abc#d" {
  Left x → print x
  Right xs → iterate print xs
}

I tried it out with Guile (using pairs and thunks) and a friend did with SML/NJ and it actually works, laziness and all.

The idea is that xs would be a possibly infinite character stream ['a', 'b', 'z', 'h', ...] and this validate function would lazily fold over it, initially returning a Right identical lazy stream, until it reaches a non-alphanumeric character. Once it does, it will stop the computation, “go back in time” and return a Left with the incorrect character.

When approaching this behavior using e.g. OCaml exceptions or effects, it becomes apparent that you have to ensure that the handler surrounds the forcing. Another approach would be to create a different data structure which encodes failure, and fold to that. Both ideas would result in leaking the implementation to the caller. Therein lies the cuteness of this implementation: consumer code does not need to install a handler or use a different data structure—it’s all self-contained.
But that’s not the point, there ought to be approaches which allow us to recover all the nice properties of validate in its current form after all, the point is just having fun and playing with weird control flow.

Now I feel like I sort-of understood what was going on here: the reason this “time rewind” works is because there actually is a “handler surrounding forcing”, call/cc turns its evaluation context inside-out, and forcing happens within the evaluation context of call/cc. So then I tried to limit the context to that of the definition site:

let validate xs =
  reset (shift k → Right (foldr (... else k (Left x)) ...))

Tried that in Guile (using ice-9 control), and my expectation was that it would just return the wrong type of argument on evaluation… it’d act like an early return, rather than reaching out to outside context (case) and re-running it. indeed that was what happened.

Now I just want to know if I’m on the right track in understanding this, and I’m also curious if there is any kind of trick to recover call/cc’s undelimited control from shift/reset’s delimited control (without converting the whole program to CPS…

Oh! One more thing, if I see any (reset .. (shift k ..) ..) in the wild, is there a mechanical way to translate it effect handlers? I’m looking for a 1:1 correspondence if there is any… I can translate examples, I just want to make sure if there’s a principled approach to the translations, and possible nuance I’m missing. My current approach is: take shift body out into a function, replace calls to k in it with perform ∘ Eff, move reset body into the handler, as continue k body, with the vacancy (shift ..) has left being replaced with k’s input. So does that sound right?

2

Consider an effect system for delimited continuations/effect handlers. If
validate : char stream -> char stream, then it’s a pure function that maybe uses effects internally and you won’t have time travel.
If validate : char stream -[TimeTravel]-> char stream then calling it may perform effects, which have to be handled somewhere.

I just had an idea that default handlers (which once were included in OCaml multicore) could be used for all-encompassing handlers and simulate call/cc, but they don’t receive the continuation and implicitly resume immediately.

So you can’t construct fun toys like this without installing a handler, but in practice containment of weird time travel tricks to a small scope is good.

Deep effect handlers correspond to shift0/reset0 and shallow effect handlers correspond to control0/prompt0. The standard way is translate shift0 (fun k -> e) into perform (Shift0 (fun k -> e)) and deep-handle it with Shift0 f k -> f k. Shift/reset is weaker because shift leaves the delimiter intact, you can’t escape from the innermost delimiter and reach further ones.

To express shift, you may first express it in terms of shift0:

shift (fun k -> e) = shift0 (fun k -> reset e)

1 Like
3

Advertisement!: Paulo de Vilhena’s PhD dissertation, whose main theme is formal reasoning about programs that involve effect handlers, contains chapters about the connections between callcc/throw, shift/reset, and effect handlers (including encodings between these combinators and proofs that these encodings give rise to the expected reasoning rules).

It also contains a specification and a proof of correctness for invert, a function that uses effect handlers to turn an iter function into a lazy sequence.

6 Likes
4

Coincidentally, just last night I stumbled upon two constituent papers: A type system for effect handlers and Verifying an effect-handler-based define-by-run reverse-mode AD library (didn’t know they were part of a thesis) and indeed found them very good at elucidating connections between previous work (the novel stuff needs more time to digest).

5

Many thanks to François for sharing my PhD thesis! In Chapter 6, one finds the encoding of callcc and throw in terms of effect handlers. This encoding is written in a formal lambda calculus, but it can be easily ported to a language with support for effect handlers and multi-shot continuations. In OCaml 5, continuations are one-shot, but, in Multicore OCaml 4.12.0+domains+effects, one can simulate multi-shot continuations via the feature Obj.clone_continuation[1]:

module type CALLCC = sig
  type 'a cont

  val callcc : ('a cont -> 'a) -> 'a
  (* [callcc (fun k -> e)] reifies the _encompassing evaluation context_ as [k]
      and executes [e]. *)

  val throw : 'a cont -> 'a -> 'b
  (* [throw k' w] erases the encompassing context restoring the one that
     is reified as [k'], which is then filled with the value [w]. *)

  val run : (unit -> unit) -> unit
  (* [run (fun () -> e)] defines the meaning of the _encompassing evaluation
     context_ as the context delimited by [run].
     1. [callcc] and [throw] have meaning only in the scope of [run].
     2. Applications of [run] cannot be nested.
     3. Effect handlers cannot be used in the scope of [run].
   *)
end

module Callcc : CALLCC = struct
  type 'a cont = (unit -> 'a, unit) continuation

  effect Callcc : ('a cont -> 'a) -> (unit -> 'a)
  effect Throw : ('a cont * 'a) -> 'b

  let callcc t = (perform (Callcc t)) ()
  let throw k w = perform (Throw (k, w))

  let run main =
    match main() with
    | effect (Callcc t) k ->
        continue (Obj.clone_continuation k) (fun () -> t k)
    | effect (Throw (k, w)) _ ->
        continue (Obj.clone_continuation k) (fun () -> w)
    | () -> ()
end

The thesis also includes the implementation of invertcc, a version of invert (the function that transforms an iter function into a lazy sequence) using callcc instead of handlers. It is straightforward to translate invertcc to OCaml:

open Callcc

type 'a iter = ('a -> unit) -> unit
type 'a seq = 'a Seq.t

(* Transforms an iteration method [iter] into a lazy sequence. *)
let invertcc : 'a iter -> 'a seq = fun iter () -> callcc (fun kc ->
  let r = ref kc in
  let yield x = callcc (fun kp ->
    throw !r (Seq.Cons (x, fun () -> callcc (fun kc ->
      r := kc; throw kp ()))))
  in
  iter yield;
  throw !r Seq.Nil
)

Now, your original question is whether callcc can be implemented using shift/reset. I believe the answer is yes. Here is an encoding using shift0 and reset0:

let callcc t = (shift0 (fun k -> k (fun () -> t k))) ()
let throw k w = shift0 (fun _ -> k (fun () -> w))
let run main = reset0 main

Your second question is whether there is a principled translation of shift/reset using handlers. I believe that the best reading to answer this question is the paper On the expressive power of user-defined effects by Forster et al. The “principled” translation for which you were looking is the notion of a macro translation. The nuance that you might be missing is the preservation of typeability across these translations.

  1. This operation has bugs: https://gitlab.inria.fr/pdevilhe/hazel/-/blob/master/src/test.ml. ↩︎

3 Likes
6

Thank you a lot ! If all the advertising of the internet were of this quality, I could remove my ad blocker from my browser. :slight_smile: Recently I was searching something to read for my evening, I think I found what I was looking for.

@vilhena : congratulations for your thesis. I’ve only read the first two chapters (I guess I should improve a little bit my skill in Separation logic and have a look at Iris to understand all the subtleties) and it’s very interesting, especially the notion of protocol. I just have a little naming question: could you explain the origin of the name Hazel, Maze and Tes?

7

Thank you for these words, @kantian! I hope you enjoy the reading.

There is actually nothing special about the origin of these names:

  1. Ha in Hazel stands for handlers and zel stands for Separation Logic.

  2. Maze is suggestive of the operational complexity of multi-shot continuations and sounds similar to Hazel.

  3. Tes is an acronym for type-and-effect system.

8

I am overwhelmed by the quality of the replies, thank you all for the pointers and links. I’ve been reading through this paper and realized just how little I actually know about the semantics of these control flow operators

9

Does this mean a supposed effect-capable type system should be able to figure out the effect escapes under laziness somehow?

speaking of typing, I’ve tried to implement the equivalence monoidoid outlined:

type _ Effect.t += Shift : (('a, 'b) continuation -> 'b) -> 'b t
let shift f = perform (Shift f)
let reset f = try_with f () {
  effc = fun (type a) (e : a t) : ((a, _) continuation -> _) option ->
    match e with
    | Shift f ->  Some f
    | _ -> None
}
(* (reset (+ 1 (shift k ( * 3 (k 2))))) ;; 9 *)
let _ = assert (9 = reset (fun _ -> 1 + shift (fun k -> 3 * continue k 2)))

and I don’t think it’s generally typeable (I did use concrete types though to verify it’s doing the right thing).
Is shift/reset actually typeable? (I guess I’ll find out as I continue to read the paper).

Worth noting that I used to do it by running the shift/reset in my head then “specializing” like this:

type _ Effect.t += K : int -> int t
let k e = perform (K e)
let nine = try_with (fun _ -> 3 * k 2) () {
  effc = fun ... -> match e with
  | K e -> Some (fun k -> continue k (1 + e))
  | ...
}

as I mentioned in the first post.

Also what really is shift0? what does inserting a delimiter inside the body of shift0 imply? guile doesn’t seem to have shift0. Where can I play with all of those prims?

10

If you replace the type first line with

type _ Effect.t += Shift : (('a, int) continuation -> int) -> 'a t

then your example type-checks.

Ideally, one would like to assign shift a type that conforms to the following shape:

type ('a, 'b) t = (('a -> 'b) -> 'b) -> 'a

The type variable 'a stands for the type of the expression shift f, and the type variable 'b stands for the type of the evaluation context delimited by the innermost reset (it is therefore known as the answer type). However, to infer the instance of 'b, the type system needs to remember the type assigned to the innermost reset. In your example, the applications of reset always delimit an integer term, so it suffices to assign shift the type ('a, int) t.

Yes, the paper A Functional Abstraction of Typed Contexts documents a type system with support for shift and reset. The main idea is to extend typing judgments (and consequently arrow types) with the type assigned to the innermost reset.

To type-check shift0, we could imagine extending typing judgments with a list of types ρ that were assigned to the len(ρ) enclosing reset’s: Γ ⊢ e : ρ : τ (τ is the type of e’s result, and Γ is a typing context).

The syntax of types would be as follows:

κ, τ ::= ... | τ -{ρ}-> τ
ρ ::= ⟨⟩ | τ · ρ

Here is a sketch of the typing rules that I have in mind:

  Γ ⊢ e : τ · ρ : τ
---------------------- (Reset0Typed)
 Γ ⊢ reset0 e : ρ : τ

 Γ ⊢ f : ⟨⟩ : (τ -{ρ}-> κ) -{ρ}-> κ
------------------------------------ (Shift0Typed)
      Γ ⊢ shift0 f : κ · ρ : τ

    Γ; x : τ ⊢ e : ρ : κ
---------------------------- (LambdaTyped)
 Γ ⊢ λx. e : ⟨⟩ : τ -{ρ}-> κ

Using the encoding of shift proposed by @monoidoid shift f ≜ shift0 (λk. reset0 (f k)), it would then be possible to write the typing rule of shift as a derived rule:

 Γ ⊢ f : ⟨⟩ : (τ -{ρ}-> κ) -{κ · ρ}-> κ
---------------------------------------- (ShiftTyped)
      Γ ⊢ shift f : κ · ρ : τ

The Racket programming language implements most of these operators. The documentation is complete and very well written: https://docs.racket-lang.org/reference/cont.html

2 Likes
11

For sure, I enjoy. :slight_smile: I’m sure I’ll have more questions after more reading, but surely in PM (french or english?).

For the name Maze and Tes, that’s what I had imagined, but I didn’t get Hazel. For Maze, you could have this a posteriori acronym: Multishot Aware SEparation logic. When I read this name I imagined this logic as Ariadne helping Theseus in order to beat the Minotaur of multishot continuation :wink:

12

Thank you so much for the comprehensive answers
Also welcome to OCaml discuss!