Conversation
|
CC @fpottier, who had volunteered to review the tutorial. |
|
Thanks! I will try to have a look soon-ish. |
|
Florian Angeletti (2022/04/06 13:49 +0000):
The "Language extensions" chapter has been a catalogue à la Prévert
for many years, this PR is not the right place for discussing this
issue.
Sorry. What would be the right place, according to you, @Octachron?
|
|
An independent issue or PR if you feel motivated seems like a better place. |
|
Florian Angeletti (2022/04/06 14:04 +0000):
An independent issue or PR if you feel motivated seems like a better
place.
I just opened #11164 for tracking
purposes.
|
|
One last thing (...): the chapter does not currently document the support decision for effect handlers, which is subtly half-way between "this is experimental/internal, please don't use it" and "cool new feature, please go ahead". Could we start the chapter with a paragraph that explains the current design decisions / stability state of the feature? Here is what I wrote on this topic elsewhere (the discussion was about the pre-5.0 effect syntax, so some of the points in this post don't apply to what is currently in trunk):
This is, of course, just my personal understanding of a not-so-obvious situation/decision regarding language support for handlers. But could we converge on a text of this nature that describes a current consensus? For a first proposal, here would be a variant of this text in more manualarial style:
(Note that we start by giving the OCaml version that introduces the feature, which is an important omission from the current version.) |
|
@gasche how about
|
|
This is fine, thanks! (I thought of adding "typing rules" as something that would be caracteristic of a new language feature. as you did, but in fact there arguably are typing rule coming from the types of the exposed API, that guarantee type-safety of values obtained through Effects primitives. What we don't have is a static discipline to reason on the operations a piece of code may perform, which brings a stronger form of runtime safety (no unhandled effects), but is also not strictly-speaking necessary to add effect handlers as a language feature. This is just thinking out loud, I'm not suggesting any change to your text.) |
|
Thanks @kayceesrk for being very patient on this PR. You are working on many sub-topics at the same time, and it must be a bit overwhelming, but I think that efforts in good documentation (and, in general, clear communication towards our users) definitely pay off. |
3fd7e78 to
6dabe77
Compare
I was thinking particularly about "effect safety" when I wrote "typing rules". But it is not appropriate to use "effect safety" at the start of the document especially since that term is not well known. The latest commit drops "and typing rules". The sentence reads better without it.
Indeed. Likewise, I appreciate the thoughtful reviews. The PR definitely improved quite a bit thanks to them. |
|
Thanks! Merged. |
| "comp1" performs "Xchg 0" and "Xchg 1" and receives the values "1" and "2" | ||
| from the handler respectively. Hence, the whole expression evaluates to "3". | ||
|
|
||
| It is useful to note that the we must use locally abstract type "(type a)" in |
| performs the "Xchg" effect, the control jumps to the corresponding handler. | ||
| However, unlike exception handlers, the handler is also provided with the | ||
| delimited continuation "k", which represents the suspended computation between | ||
| the point of "perform" and this handler. |
There was a problem hiding this comment.
At this point, I would have expected an explanation of the type parameter a of the type (a, _) continuation.
| raises the same exception. | ||
| \item Case "effc": If the computation performs the effect "Xchg msg" with the | ||
| continuation "cont", then we return "Suspended{msg;cont}". Thus, in this | ||
| case, the continuation cont is not immediately invoked by the handler; |
| contrast, a shallow handler monitors a computation until either the computation | ||
| terminates or the computation performs one effect, and it handles this single | ||
| effect only. In situations where they are applicable, deep handlers are usually | ||
| preferred. An example that utilises shallow handlers is discussed later |
There was a problem hiding this comment.
Could you justify why deep handlers are preferred?
| effect, the current task is suspended (inserted into the queue of ready tasks), | ||
| and the next task from the scheduler queue is run. If the effect is "Fork f", | ||
| then the current task is suspended, and the new task "f" is executed | ||
| immediately via a tail call to "spawn f". Note that this choice to run the new |
There was a problem hiding this comment.
The fact that you are specifying that the call is in the tail position makes the reader wonders about how non tail calls (and stack overflows) are handled inside effect handlers.
| \begin{caml_example}{verbatim} | ||
| open Printf | ||
|
|
||
| let _ = run (fun _ -> |
There was a problem hiding this comment.
The absence of yield in this example is a bit disappointing.
| consumed (i.e., used at least once) so as to ensure that the captured | ||
| continuation is used linearly. |
There was a problem hiding this comment.
I am not sure that this sentence can be understood by the average OCaml programmer.
A forward reference to the explanations about linear continuations could avoid the programmer to run away.
| resumed, the stack is restored to the previous state by linking together the | ||
| segment pointed to by "k" to the current stack. Since neither continuation | ||
| capture nor resumption requires copying stack frames, suspending the execution | ||
| using "perform" and resuming it using either "continue" or "discontinue" are |
|
|
||
| As discussed earlier~\ref{s:effects-discontinue}, the delimited continuations | ||
| in OCaml must be used linearly -- \emph{\textbf{every captured continuation | ||
| must be resumed either with a "continue" or "discontinue" exactly once}}. |
There was a problem hiding this comment.
In the render HTML page, only "continue" and "discontinue" are written in bold fonts. Is this intended?
| in OCaml must be used linearly -- \emph{\textbf{every captured continuation | ||
| must be resumed either with a "continue" or "discontinue" exactly once}}. | ||
| Attempting to use a continuation more than once raises a | ||
| "Continuation_already_taken" exception. For example: |
| In this case, if "k" becomes unreachable, then the finaliser ensures that the | ||
| continuation stack is unwound by discontinuing with an "Unwind" exception, | ||
| allowing the computation to free up resources. However, the runtime cost of | ||
| finalisers is much more than the cost of capturing a continuation. Hence, it is |
There was a problem hiding this comment.
What is costly exactly? Running the finalizer, installing the finalizer, or both?
A (probably naive) strategy to be safe could consist in systematically installing a finalizer on every resource critical continuations if the programmer is not completely sure that it will be correctly discontinued by the program logic.
If that's a discouraged strategy, the manual should probably say so.
| \end{caml_example} | ||
|
|
||
| We may implement the same example using deep handlers using reference cells | ||
| (easy, but unsatisfying) or without them (harder). We leave this as an exercise |
| \subsection{s:effects-shallow}{Shallow handlers} | ||
|
|
||
| The examples that we have seen so far have used \textit{deep} handlers. A deep | ||
| handles all the effects performed (in sequence) by the computation. Whenever a |
There was a problem hiding this comment.
A deep handles -> A deep handler handles
This PR adds an effect handlers tutorial to the manual. The rendered page is available at https://kcsrk.info/webman/manual/effects.html. It is easier to review the changes by reading the content in the rendered page.
The commit 0e890b0 does some minor formatting cleanup to the manual README file and can be safely ignored.