Effective Programming in OCaml
Please log in to watch this conference skillscast.
Effect handlers have been gathering momentum as a mechanism for modular programming with user-defined effects. Effect handlers allow for non-local control flow mechanisms such as generators, async/await, lightweight threads and coroutines to be composably expressed. The Multicore OCaml project retrofits effect handlers to the OCaml programming language to serve as a modular basis of concurrent programming. In this talk, I will introduce effect handlers in OCaml, walk through several examples that illustrate their utility, describe the retrofitting challenges and how we overcome them without breaking the existing OCaml code. Our implementation imposes negligible overhead on code that does not use effect handles and is efficient for code that does. Effect handlers are slated to land in OCaml after the addition of parallelism support.
Q&A
Question: What is the efficiency hit you take by using exceptions?
Is it leveraging the existing machinery for exceptions in OCaml?
Answer: Good question. We retain the exception implementation as is. So no performance hit there. Results are there in the Table 1 in https://kcsrk.info/papers/retro-concurrency_pldi_21.pdf
Question: How do you see LWT / Async changing to make use of this work?
Is there space for new libraries to exploit effects in OCaml?
Answer: Thanks to the modularity of effect handlers, we can in fact aim to merge Lwt and Async modulo small breaking changes. In the meantime, we’re building the next gen high performance multithreaded I/O library using effect handlers here: https://github.com/ocaml-multicore/eioio
Question: Is the implementation similar Alexis King's delimited continuations proposal for GHC?
Answer: Good question. yes, it is similar. Alexis’ library builds on top of existing support for threads in the GHC runtime system. We build that support into OCaml.
Question: Can implement the same mechanism in GHC to give us algebraic effects in Haskell? Or is typing the problem?
Answer: Typing is a separate issue. See Alexis King’s eff library which achieves something very similar building on top of GHC existing support for lightweight threads: https://github.com/hasura/eff
Question: Curious what the types look like for the `match f() with` from the sample code. Can you show what the types look like? I assume the type inferencing from OCaml continues to work without annotations
Answer: One major difference from other studies of effect handlers (I’m thinking Eff, Koka, etc), is that the current OCaml implementation does not give you effect safety — No static guarantee that all the effects that you perform are handled. This is only as bad as exceptions.
Type inference continues to work. See Section 4.1 in https://kcsrk.info/papers/retro-concurrency_pldi_21.pdf for the types.
We’ve built prototype OCaml implementation with an effect system. See https://www.janestreet.com/tech-talks/effective-programming/
Question: Was there thoughts to use polymorphic variants to represent the types rather than using exceptions?
Answer: The effect system that Leo proposes in the talk above uses structural typing (similar to polymorphic variants) IIRC. The distinction doesn’t matter that much unless you want to ensure effect safety. It turns out that structural typing makes it easier when using abstraction (something like hiding types using modules).
Question: Need to watch Leo’s talk then, exhaustive pattern matching is such a good property in building software I’m loath to give it up.
Answer: Agreed. The current plan is to only upstream the runtime support for effect handlers (i,e fibers) now, and add the syntactic support with the effect system. This is to ensure that OCaml doesn’t end up with both untyped and typed versions of effects.
The runtime support will be exposed as functions in Obj module. As
a library writer, you can build direct style code that takes advantage of the
ability to suspend and resume computations. And when the effect system lands,
you can change your library to use the effect system, without breaking code for
the user of your library.
Question: Is there a way to encode preëmptive concurrency as well?
Answer: Really good question. We do not support preemptive
concurrency using handlers now. But we have a good idea of how to do this. The
challenge there is to get the asynchronous Yield effect only to
appear in the context where there is a handler for Yield .
We’ve written some thoughts about it in Section 4.2 of https://kcsrk.info/papers/system_effects_feb_18.pdf
Question: Is it likely that ocaml will ever get linearity to ensure the usage of those continuations?
Answer: Highly likely, though there isn’t anyone actively hacking on it now. https://arxiv.org/abs/1803.0279
Question: In the paper linked in the concurrency question above, (https://kcsrk.info/papers/system_effects_feb_18.pdf) you note that for an async exceptions, a Break effect would intentionally not continue the continuation.
Answer: IUC, you are talking about Sys.Break .
Sys.Break is an exception not an effect. There is no way to resume
here. If I am mistaken, please let me know.
Question: Quote from the paper:
“By treating Break as an asynchronous effect, we can mix synchronous and asynchronous cancellation reliably.
...
Asynchronously-cancellable code can be implemented by handling the Break effect and discarding the continuation.”
Answer: Good point. I think “discarding a continuation” was a lazy phrase. Really, it should have said, you should discontinue the continuation with an exception just to run the resource cleanup code. For example,
try ignore (discontinue k Unwind) with Unwind -> ()
This code discontinues the continuation with Unwind exception so
that all the resource cleanup gets to run, and ignores the Unwind
exceptions.
Also, the TFP paper was return a few years ago before we fully understood what the backwards compatibility expectations should be.
YOU MAY ALSO LIKE:
Thank you to our sponsors and partners
Platinum
Silver
Bronze
Effective Programming in OCaml
K C Sivaramakrishnan
Research AssociateUniversity of Cambridge