Conversation
|
We used the effects syntax in early versions of Eio, and personally I found it more confusing, even though it is shorter. In all other control structures, execution starts at the top, exits at the bottom, and then we're done. For example: begin
try foo ()
with _ -> bar ()
end;
baz ()Here, once we reach the
But that's not the case with effects. Using functions for the callbacks is clearer I think. We expect functions to be called after they're defined, and for control to go elsewhere after they finish. Also, installing an effect handler and creating a new stack seems important enough that you'd like to see easily when it's happening. But: try foo ()
with
| A -> ...
| B -> ...
...Here, I have to check every case to discover whether this is an effect handler or not. |
|
I prefer the new syntax. |
|
Was gating this change on ocaml/ocaml/RFCs#27 discussed? The keyword part has an implementation in #11252 (which I think is aiming to be ready for 5.2 as well, so this shouldn't pose a problem per se) but I don't think we have converged on a solution for the driver part. IIRC the effects syntax was removed from multicore prior to #10831 both because of the question of its utility and also because of compatibility concerns with the impact of the syntax change? |
|
IIRC I switched all my later branches to use: effect E, k ->rather than: effect E k ->because it allowed you to write: effect Foo(a, b), k ->instead of needing to do: effect (Foo(a, b)) k -> |
|
It is worth noting that this locks us in to a couple of big design decisions that I think we should make sure we are happy with before proceeding. Deep handlersThis makes the default form of handlers deep handlers. Personally, I've gone back on forth on deep vs. shallow handlers, but I currently think that either is a reasonable primitive, since it is pretty easy to encode each using the other. Since deep handlers are much easier to give good syntax for I think it is fine to lock in this decision. For reference, I think the best way to write a shallow handler using this PR is something like: type 'a int_state =
| Get : int int_state
| Set : int -> unit int_state
effect State : 'a int_state -> 'a
type 'a ret =
| Ret : 'a -> 'a ret
| Op : 'k int_state * ('k, 'a) continuation -> 'a ret
let handle_int_state f i =
let rec loop s = function
| Ret x -> x
| Op(Get, k) -> loop s (continue k s)
| Op(Set s', k) -> loop s' (continue k ())
in
loop i
(match f () with
| x -> Ret x
| effect (State op) k -> Op(op, k))Operations are extensible variant constructorsThis locks in the decision to use values of an extensible variant type type 'a state = effect
| Get : 'a
| Set : 'a -> unit
effect Counter : int state
let handle_counter f =
(match f () with
| x -> fun _ -> x
| effect Counter Get k -> fun s -> continue k s s
| effect Counter (Set s) k -> fun _ -> continue k () s) 0
let incr () =
perform Counter Set(1 + perform Counter Get)Here This division gives a lot of additional flexibility. For example, you can write a generic handler for state: handle_state name f =
match f () with
| x -> fun _ -> x
| effect name Get k -> fun s -> continue k s s
| effect name (Set s) k -> fun _ -> continue k () swith type: val handle_state : 'a state eff -> (unit -> 'b) -> 'a -> 'bYou can even make my shallow handler code from above generic: type ('a, 'e) ret =
| Ret : 'a -> ('a, 'e) ret
| Exn : exn -> ('a, 'e) exn
| Op : ('k, 'e) operation * ('k, ('a, 'e) ret) continuation -> ('a, 'e) ret
let shallow name f a =
match f a with
| x -> Ret x
| exception e -> Exn e
| effect name op, k -> Op(op, k)with type: val shallow : 'e eff -> ('a -> 'b) -> 'a -> ('b, 'e) retsuch that the shallow handler could have been written: let rec loop s = function
| Ret x -> x
| Op(Get, k) -> loop s (continue k s)
| Op(Set s', k) -> loop s' (continue k ())
in
loop 0 (shallow Counter f ())In addition to the increased flexibility, this approach is more likely to be somewhat forwards compatible with a checked version of effects -- since it can use the same effect type definitions. Finally, I think this version is better from a pedagogical perspective. It much more clearly separates effects from operations -- distinguishing If people are interested in this more flexible approach, I'd be happy to code it up ready in good time for 5.2. There isn't much to do that I don't already have on various existing branches. Since I mostly think that in the long run we'll want to deprecate the unchecked effects, it wouldn't be too bad to stick with the current system. Still, it's worth making sure we are happy with it before committing to it for the foreseeable future. |
|
As I stated during the meeting, I believe that we should give ourselves a chance to design a static type/effect system for effects, and I hope to get a better picture of how realistic that is during the next year -- because I will be spending a part of the year gently pushing people interested in the topic to come up with plausible proposals. If it turns out that we can have an effect system in a reasonable timeframe (3 years?), I would prefer to wait for it to make the syntax available. We discussed, as a compromise, making this effect syntax available "out the main track" as an experimental variant of the language. I would be fine with the idea of upstreaming the code in the compiler distribution (so that we collectively maintain it, instead of imposing the burden on a few users), but I would prefer if it stayed as a separate switch, for example by being presented as a configure option. (Having it as a runtime option makes it a wee bit too tempting in my opinion.) Why wait for a static effect system?The expressivity of effect handlers is very limited by their untyped nature. There are many functions for which a natural effect is polymorphic on the type of its inputs, and this currently cannot be expressed. For example, consider a function that inverts control of a callee-has-control iterator Why discourage usage of the effect syntax in everyday programs?Generally there are two arguments.
|
Note that with my proposed approach this is representable in a reasonable way as something like: type 'a yield = effect
| Yield : 'a -> unit
type 'a yielder = 'a yield eff -> ('a -> unit) -> unit(Actually, I find your types a bit confusing -- but since the translation from the type with an effect system is mechanical I responded anyway) |
|
If you are happy to write everything in an environment monad, then you can also abstract over the function |
|
Thanks @lpw25 for your thoughts on a more flexible API. What does your API look like when desugared without syntax changes? It's not clear to me if the separation of the @gasche wrote:
Having a configure option often seems like the worst of all worlds to me; we're just forking our own language every time we add one :-) I'm most worried by the added complexity to the type-checker if upstreaming this as a configure switch, as the A few other options:
I'll adjust the syntax next I come to this PR for @lpw25's suggestion of |
If we upstream the code, then we have to maintain it. You see this this as a downside (more maintenance work for a hidden feature), but I see this as an upside (for people interested in this syntax): this greatly increases the chance that this experimental feature keeps working with the current version of OCaml. It is of course possible to maintain this as an experimental switch completely out of tree, but history suggests that such experimental trees stay on older versions of OCaml and only get updated fairly rarely. I am not sure @avsm what is your intention regarding the current PR. Do you intend it for upstreaming in the current form (after some changes and review)? Or you opened it for awareness, but then you want to actually maintain it out-of-tree? There is no meta-commentary about this in the PR description itself, so by default I would assume that this is proposed for upstreaming as-is. (A very minor point: if most of the code is from @lpw25, I would expect him to be listed as author or co-author in the commit metadata.) Note: the current status of ocaml/RFCs#27 is to be found #11252 . There is a PR, it needs a rebase and some changes, someone else than @stedolan should probably do it, and either @OlivierNicole or myself could probably do it. |
|
I opened the PR up as a followup to the brief discussion at the developer meeting. Once there's consensus on what we'd like for 5.2, I'll clean up the PR and finish up TODOs and turn it into a 'proper' PR, with the right Co-authored-by attributions. If the syntax isn't accepted, then I'm planning to maintain it out-of-tree for at least 5.2, since I need it for my own teaching use. |
I like this example. Thanks for sharing. It makes me feel a little bit better about the deep handler semantics. The example shows that the one useful pattern which is naturally expressed using shallow handlers can also be expressed in a similar fashion using deep handlers.
The reading here is that
Leo is correct about the fact that in OCaml 5.0, unlike effect systems in literature, we have a single "effect" type Summarising the benefits of separating out "operations" from "effects":
Overall, I like the idea of separating out effects from operations as proposed and proposing that upstream. But I am not an expert in the parts of the code that this proposed feature would touch (which I assume is mostly the type system side). I would be happy to port the programs that we have to this syntax and offer feedback. |
|
Hi! I have read the discussion and will now post a few responses (in separate messages, for clarity). |
|
@avsm writes: it is occasionally more ergonomic to use the low level syntax when the existential type variables introduced by the pattern matching need to be accessed. I believe he refers to this pattern: try main () with
effect (Ref init) k ->
(* trick to name the existential type introduced by the matching: *)
(init, k) |> fun (type a) (init, k : a * (a t, _) continuation) ->I think it is not very natural to have to do this. Could we instead allow the following syntax? try main () with
effect (type a) (Ref (init : a)) (k : (a t, _) continuation)) ->Or, even better, could we somehow let the type-checker work without any type annotation in this situation? (I am not quite sure why an annotation is required.) try main () with
effect (Ref init) k -> |
|
@talex5 makes the point that one must scan an entire |
|
@lpw25 writes: this makes the default form of handlers deep handlers. This may be true in the current proposal, but I do not see why it has to be so. We could (and I believe that we should) offer syntax for both deep handlers and shallow handlers. @lpw25 writes: it is pretty easy to encode each using the other. Whether these encodings are "easy" is subjective, and depends on one's level of experience and familiarity with effect handlers. Unlike Leo and KC, I do not find these encodings simple or "easy" to reinvent, and I certainly don't think that we should encourage people to pollute their code with such encodings. Regarding syntax, a simple proposal would be to introduce To avoid this problem, one could use different keywords. E.g., one could use Perhaps a better suggestion is to replace |
|
Regarding the separation of "operations" and "effects", @lpw25 writes: This division gives a lot of additional flexibility. While I am not opposed to this proposal, I note that a similar level of abstraction can be achieved in OCaml 5.0 by abstracting over a module. (This requires either a functor or a first-class module.) Here is a complete demonstration: open Effect
open Effect.Shallow
(* This can be done today: a handler for a state of type [int]. *)
type _ Effect.t += Get : unit -> int Effect.t
type _ Effect.t += Set : int -> unit Effect.t
let rec loop_int : type x y . int -> (x, y) continuation -> x -> y =
fun s k x ->
continue_with k x {
retc = (fun y -> y);
exnc = raise;
effc = fun (type b) (e : b Effect.t) ->
match e with
| Get () ->
Some (fun (k : (b, _) continuation) -> loop s k s);
| Set s ->
Some (fun (k : (b, _) continuation) -> loop s k ());
| _ ->
None
}
let handle_state_int (s : int) (f : 'x -> 'y) (x : 'x) : 'y =
loop s (fiber f) x
(* This can be done today as well: using a module type and a functor,
abstract over the type [a] and over the dynamic effect labels
denoted by the names [Get] and [Set]. *)
module type STATE = sig
type a
type _ Effect.t += Get : unit -> a Effect.t
type _ Effect.t += Set : a -> unit Effect.t
end
module Make (S : STATE) = struct
let rec loop : type x y . S.a -> (x, y) continuation -> x -> y =
fun s k x ->
continue_with k x {
retc = (fun y -> y);
exnc = raise;
effc = fun (type b) (e : b Effect.t) ->
match e with
| S.Get () ->
Some (fun (k : (b, _) continuation) -> loop s k s);
| S.Set s ->
Some (fun (k : (b, _) continuation) -> loop s k ());
| _ ->
None
}
let handle_state (s : S.a) (f : 'x -> 'y) (x : 'x) : 'y =
loop s (fiber f) x
end
(* If desired, the above functor can be turned into a function that
takes a first-class module as an argument. *)
let handle_state (type a) (state : (module STATE with type a = a)) (s : a) f x =
let open Make(val state : STATE with type a = a) in
handle_state s f x
(* An example: using [handle_state] to handle a state of type [bool]. *)
module M = struct
type a = bool
type _ Effect.t += Get : unit -> a Effect.t
type _ Effect.t += Set : a -> unit Effect.t
end
let () =
let f () =
let b = perform (M.Get()) in
perform (M.Set (not b));
let b = perform (M.Get()) in
b
in
let (y : bool) =
handle_state (module M : STATE with type a = bool) false f ()
in
assert (y = true)This encoding suggests that Leo's proposed extension does not really add expressiveness. However, the proposed extension certainly allows writing simpler and more concise code. Perhaps an ideal situation would be one where effect declarations remain as they are now (in OCaml 5.0) but new sugar for first-class modules is introduced, so that Leo's example can be expressed? |
Yes, that's right. |
Without the addition of type 'e t = ..
type ('a, 'b) continuation
val perform : 'e t -> ('a, 'e) operation -> 'a
val continue : ('a, 'b) continuation -> 'a -> 'b
val discontinue : ('a, 'b) continuation -> exn -> 'b
val discontinue_with_backtrace : ('a, 'b) continuation ->
exn -> Printexc.raw_backtrace -> ('b, 'c) handler -> 'c
val get_callstack : ('a, 'b) continuation -> int -> Printexc.raw_backtrace
module Deep : sig
type ('a, 'b, 'e) handler = {
retc : 'a -> 'b;
exnc : exn -> 'b;
opc : 'k. ('k, 'e) operation -> ('k, 'b) continuation -> 'b;
}
val match_with : 'e t -> ('c -> 'a) -> 'c -> ('a, 'b, 'e) handler -> 'b
type ('a, 'e) effect_handler = {
opc : 'k. ('k, 'e) operation -> ('k, 'a) continuation -> 'a;
}
val try_with : 'e t -> ('a -> 'b) -> 'a -> ('b, 'e) effect_handler -> 'b
end
module Shallow : sig
type ('a, 'e) ret =
| Ret : 'a -> ('a, 'e) ret
| Exn : exn -> ('a, 'e) ret
| Op : ('k, 'e) operation * ('k, ('a, 'e) ret) continuation -> ('a, 'e) ret
val fiber : 'e t -> ('a -> 'b) -> ('a, ('b, 'e) ret) continuation
endIn addition to the various simplifications in the API that this change allows, it is also worth noting that finding the right handler when doing a perform no longer requires running any user code. Each handler is associated with a particular effect name, which the runtime can use to find the right handler before running any user code. This should improve performance of code using more than one handler.
If we add something like: effect Legacy : 'a eff -> 'aThen it the old API can be implemented as uses of the new API for the effect
I actually think that
It is true that you can do similar things by abstracting over a module, and for cases like parameterized state, where you are only abstracting over a non-parameterized type you can even use first-class modules to do it in the core language. However, when you want to abstract over effects as a whole you cannot do it in the core language without my proposal, because the abstraction is fundamentally higher-kinded. My proposal really amounts to adding simple support in the core language for a very specific form of higher-kinded polymorphism. This is makes primitives like module type Effect = sig
type 'a op
type 'a eff += Op : 'a op -> 'a eff
end
module Fiber (E : Effect) : sig
type 'a ret =
| Ret : 'a -> 'a ret
| Exn : exn -> 'a ret
| Op : 'k E.op * ('k, 'a ret) continuation -> 'a ret
val fiber : ('a -> 'b) -> ('a, ('b, 'e) ret) continuation
endwith individual handlers looking like: let foo ... =
...
let module C = struct
type 'a op = ('a, int) state
type 'a eff += Counter : 'a op -> 'a eff
end
let main () = ... perform (C.Counter(Get)) ... in
let module F = Fiber(C) in
let k = F.fiber main in
...instead of just: let foo ... =
...
let effect Counter : int state in
let main () = ... perform (Counter(Get)) ... in
let k = fiber Counter main in
...The particular case that I'm most interested in is that I wish to provide the following API as well: type 'e handler
val perform : 'e handler -> ('a, 'e) operation -> 'a
val fiber : ('a -> 'e handler -> 'b) -> ('a, ('b, 'e) ret) continuationwhere the type 'e handler
val perform : local 'e handler -> ('a, 'e) operation -> 'a
val fiber : ('a -> local 'e handler -> 'b) -> ('a, ('b, 'e) ret) continuationessentially giving a simple form of effect system for free. Here we have basically swapped out notion of "name" ( Note that if we do later add support for higher-kinded polymorphism in the core language -- as hinted at in the discussion here -- then my proposal will just become some convenient sugar for a specific form of ordinary higher-kinded type definitions. Beyond the convenience and flexibility benefits, I would like to reemphasise the pedagogical ones. I think separating effect names from operations will give people a better mental model of effects and nudge them to produce better code. |
|
I think I am generally in favor of the distinction between names and operations; it sounds reasonable and attractive indeed. |
|
@lpw25 writes: The key is to have an operation like I am not (yet?) convinced that this is a natural thing to do. An argument against this approach is that the type It seems that we have several possible approaches:
The last approach is the one that (I think) I would favor. I am not certain that I fully understand the pros and cons of each approach, though, so if anyone here can shed light on them, I would be happy to be enlightened. |
That is a reasonable description of what I propose. Deep handlers and fundamentally and fold over the computation tree, whilst shallow handlers are a match. From that perspective, my proposal is similar to giving people a list type with only In practice, I've found this interface to be more convenient to use than one based around let state init f x =
let rec loop : 'k. int -> ('k, 'a) continuation -> 'k -> 'a * int =
fun s k x ->
continue k x with
| v -> v, s
| effect State Get, k -> loop s k s
| effect State Set s', k -> loop s' k ()
in
loop init (fiber f) xwhere the type annotation on let state init f x =
let rec loop s = function
| Ret v -> v, s
| Op(Get, k) -> loop s (continue k s)
| Op(Set s', k) -> loop s' (continue k ())
in
loop init (continue (fiber State f) x)which has no need of polymorphic recursion. |
|
A note for myself: I think that the |
Note that This remains true even if you associate the handlers with the parent stack, as is more natural for shallow handlers, rather than the child stack, as is done in OCaml 5. For instance, you see the same choice in the design of effect handlers for WASM. |
Does this scale to polymorphic effects? It seems that each instantiation requires a new module with a concrete type |
|
I took the liberty to push directly to this PR:
|
|
I added (as tests) some examples of effect handling taken from the literature and from my lectures. They work fine and look pretty good with the new syntax! As discussed recently with @Octachron and @shindere , this PR does not rebase cleanly, because of nasty conflicts with the changes to Once the rebase is over, I think this PR will be in good enough shape to be reviewed. |
|
Don't you want to update the manual before merging ? |
|
I think it is fine to have the manual update in a separate PR since we are unlikely to forget it. |
|
The manual update and other improvements are included in the last section of the main PR message: #12309 (comment). Of the three todos, "Improve the implementation of typecore.ml" will be addressed by #13135. |
|
This PR is a collective work of several folks who both developed and reviewed the PR. Not sure how to capture this well in the Changes file. Currently I have
Does this work @Octachron? |
|
We could mention that most of the authors also reviewed other parts of the code. For instance, reusing one of the "collective review" pattern from my changelog analyzer:
|
|
Don't merge this just yet. I've got a half finished port of the effects examples to this and am seeing warning 34 activated. See avsm/ocaml-eff-example@04e00a9 -- this was done very quickly so I might just have messed something up as well. ( |
|
Now looks good to me! PR opened for the new syntax over at the effects example repo: ocaml-multicore/effects-examples#42 |
|
The PR feels good to go. Feel free to merge if you agree @Octachron. |
|
Note that I am on holidays until Monday. If no one has been daring enough to merge the PR yet, I will do so at this point. |
Done. Thanks for all the hard work from everyone involved! I'll make issues (where relevant) for the pending work (see todos in the original message). |
|
Thanks @kayceesrk! I've also now merged the corresponding examples repository into https://github.com/ocaml-multicore/effects-examples, so that's consistent with 5.3.0+trunk now (and left a |
16 participants
This ports the effect syntax that was available in Multicore OCaml but not included in the original multicore PR in #10831. The new syntax added is support for pattern matching:
and try/with
Since the continuation is dependently typed, there is also corresponding support in the type checker for the syntax.
This was originally written in 2015 by @lpw25 in ocaml-multicore/ocaml-multicore@d54b760 and then ported through 4.06 (@kayceesrk) and 4.12 (@ctk21) and now 5.2 trunk by me. The most significant change is the readdition of a builtin type
efffor the type checker to use, and corresponding type aliases toEffect.Deepdefinitions. This allows for the current "low level" syntax for deep handlers to be freely intermixed with the new concrete syntax (it is occasionally more ergonomic to use the low level syntax when the existential type variables introduced by the pattern matching need to be accessed).A tree of effects examples using the concrete syntax with this PR can be found at https://github.com/avsm/ocaml-eff-example/tree/effect-syntax, and the diff at ocaml-multicore/effects-examples@78cf6f6 shows how much simpler and nicer the effect syntax is to use.
Discussion at the most recent OCaml developer meeting had split opinions on the utility of this PR:
I believe both of these statements to be true -- I would like to use this PR for teaching effect systems in my undergraduate courses in Cambridge, but think we should stick to our current recommendation that the untyped effect interface is still undergoing revision and is not intended for consumption without careful consideration of whether they are actually needed or not.
TODO
finish ocamldoc supportTODO in future PRs
last_fiberargument from effect handler function and reperform (Add effect syntax #12309 (comment))