3 ms·
What do you mean "an effect system is redundant to code"? An effect system may or not come with additional static typing. I would argue that static effect types
by grumpyprole 5y ago
What do you mean "an effect system is redundant to code"?
An effect system may or not come with additional static typing. I would argue that static effect types are certainly not redundant, having programmed Haskell professionally for many years. But that's just the usual static types debate.
Unrelated to typing, algebraic effect handlers probably have the most ergonomic implementation of async I have ever seen (looking at the OCaml multicore previews).
- matu3ba 5y agoThe point I was trying to make is that you can get comparable guarantees, if you structure the code with atomticity + rollback and trace generalizations. Most people do not code like this due to missing language support for good error handling. (explicitly encoding errors as integers sucks and more so that you need to do it globally) Yes. That is compiler provided functionality on top, which looks excellent.
- Twisol 5y ago> algebraic effect handlers probably have the most ergonomic implementation of async I have ever seen (looking at the OCaml multicore previews) Just dropping in to say strong agree. The biggest stumbling block for me has been that the effect handlers are captured as part of the continuation; I was expecting them to need to be manually re-established every time the continuation is resumed. The way it works makes sense when you always `continue` within the body of an effect handler, but it feel a little unfortunate that there's no way to change the handlers for future resumptions. Other than that, the possibilities for userland coroutines, dynamically-scoped variables, and centralization of state (like `ref` but provided by a scoped allocator) are incredibly exciting. I've wanted a system like this for a long time, and for some use-cases (scheduling of concurrent simulation tasks) I had to abuse threads and thread-locals to get the separation I wanted.
- octachron 5y agoThis is the difference between deep and shallow handlers for effects. Since shallow handlers can easily implement deep handlers (by re-installing the handler itself) but deep handlers are simpler to use when they fit your use case, the plan for OCaml 5.0 is to give access to both version to users (without syntactic sugar nor a type system however).
- Twisol 5y agoOh, that's great to hear -- and thanks for the terminology! Do you have any pointers for where shallow vs. deep handlers can be compared in the Multicore OCaml literature? I've seen the non-syntactic support via `try_with`; I'd guess there's a similar function for the other flavor of handlers, but as a newcomer to the OCaml community it's not obvious where I should be looking.
- octachron 5y agoUntil recently Multicore OCaml was focused on deep handlers. The people working on the formalization of effects (either for program proofs or typed effects) were quite keen to have shallow handler integrated however. Thus, the effect module of the OCaml 5 preview contains both (see https://github.com/ocaml-multicore/ocaml-multicore/blob/5.00/stdlib/effectHandlers.mli#L79 https://github.com/ocaml-multicore/ocaml-multicore/blob/5.00...) since September. I fear that non-academic literature has not followed this change (on the academic side, see https://dl.acm.org/doi/10.1145/3434314 https://dl.acm.org/doi/10.1145/3434314 for a program proofs point of view).
- Twisol 5y agoThat paper's introduction really lays things out very nicely. Thanks for the refs!