Algebraic Effects: Another mistake carried through to perfection?
11 points by veqq
11 points by veqq
I found this incoherent and extremely verbose, and difficult to read. But from a quick look, they are right that checked exceptions and static effects have the same problem, except the problem is exacerbated in static effect systems, because checked exceptions are just one type of effect. In an application there will be many more.
My thoughts on this is that effect systems are basically “functional programming, the good parts”. I have control over which code has what type of side effects, and how those side effects are performed, without any of the inconveniences and performance issues purely functional programming causes.
The issues with checked exceptions carry over to this style really well though. I recently wrote about this in a Koka discussion (a language with effects and handlers) and I want to solve this issue in my language. Haskell programmer have been dealing with these issues for decades with effect libraries/systems like mtl, which now evolved into much more convenient libraries like effectful. The problem of having a dozen or so effects in function type signatures existed with older and simpler libraries like mtl, and they still exist with more recent ones.
The author makes comparison with parameter passing, which I found strange, given that they mention resumable exceptions ealier in the post. In some systems effects can just be implicit parameter passing under the hood, but this is not true in general. For example, OCaml effect handlers can store the continuation of the effect invocation in the heap and call it later, allowing user-level implementations of threads and schedulers like Eio, and testing concurrent programs with model checking. In addition to the same flexibility, Koka allows continuations to be entered multiple times, allowing user-level implementation of fork. You can’t do these by implicitly passing functions and calling them (unless the function you pass invokes an effect, in which case you’re back just hiding effect invocation with a function call).
they are right that checked exceptions and static effects have the same problem, except the problem is exacerbated in static effect systems, because checked exceptions are just one type of effect. In an application there will be many more.
This ignores one of the primary features of effect systems: effect polymorphism. The problem with checked exceptions was that you were limited to the exceptions specified in, say, the interface you were implementing. The solution is to allow more exceptions/effects through, by making the caller polymorphic over them. (The Koka discussion you link does mention effect polymorphism briefly.)
The main challenge with effect polymorphism is how you deal with overlap between the effects used internally by the caller, and the effects used by the callee for its own purposes (e.g. to communicate back out past the caller). It is only if you fail to deal with this that you end up with the problems of dynamic scoping.
Here are two papers (one for exceptions and one for effects) that resolve this problem of “accidental handling” using something like the lexical scope mentioned in the article: https://www.cs.cornell.edu/~yizhou/papers/exceptions-pldi2016-tr.pdf, https://www.cs.cornell.edu/~yizhou/papers/abseff-popl2019-tr.pdf. They use the type signature of the caller to control which exceptions or effects “tunnel” from the callee out past the caller, and which the caller can handle itself. This is essentially the lexical approach mentioned in the article.
But this is not the only possible solution. Koka resolves this with its mask construct. This paper describes an approach that generalizes the two papers linked above, which allows different parts of the program to declare their own local effect labels that do not interfere with each other: https://link.springer.com/chapter/10.1007/978-3-031-30044-8_9
What is true is that different languages are still experimenting with different solutions to this problem, with various tradeoffs. But the author of the article seems to be unaware that there are multiple solutions to the problem they describe.
I see effects as also being a way to remove sources of implicit global state — for example, the filesystem. It’s not usually thought of as a global, but “/“ definitely qualifies, and once you drink the Capabilities kool-aid you start seeing these globals everywhere.
Yeah, effects can be used for that, too. When you have an expressive effect system (with first-class continuations, like in Koka or OCaml) it leads to programs that are testable by default, because you can handle effects like e.g. file IO, database operations, even concurrency, differently in tests to emulate failures, edge cases etc.
One of the things that I like to do when experimenting with effect systems is implementing a grep-like tool, and then testing it with an in-memory file system.
The author makes comparison with parameter passing, which I found strange, given that they mention resumable exceptions ealier in the post. In some systems effects can just be implicit parameter passing under the hood, but this is not true in general.
You’re confusing two things: A: the multi-prompt single-shot delimited continuations with which effects are implemented with at runtime, and B: the “effect system” which is an extension of the type system to ensure correct, well-defined usage of A at runtime.
The author is correct that B is replaceable with parameter passing (plus maybe some mechanism to prevent closure over effect handlers, i.e. prevent returning a function which uses an effect that’s valid in your dynamic context but maybe not in the parents).
A is a new runtime capability which isn’t so easily replaceable - though if you are using OS threads rather than user-spacs concurrency, you might not care about having the former anyway.
You’re confusing two things: A: the multi-prompt single-shot delimited continuations with which effects are implemented with at runtime, and B: the “effect system” which is an extension of the type system to ensure correct usage of those continuations.
The author is correct that B is replaceable with parameter passing (plus maybe some mechanism to prevent closure over effect handlers
I might certainly be misunderstanding what the author says, because the post was difficult to read for me.
However you also seem to be confusing things, you’re talking about replaing a type system feature with parameter passing..
Also, (A) does not need to be a runtime capability, you can transform the program to continuation passing style, either manually or as a compiler transformation. Then every effect invocation becomes a monadic bind where the effect handler gets the continuation that it can call. AFAIK Koka even does this, and that’s how they’re able to compile to C without a runtime system. The relevant paper says: (emphasis mine)
With all evaluation transitions localized, we can now define a direct monadic translation of effect handlers into a plain typed lambda calculus using a multi-prompt monad (Section 2.9, 2.11, and 4). Such program can be directly compiled to any target platform (including C/LLVM, WASM, JavaScript, Java VM, .NET, etc) without requiring special runtime mechanisms.
The continuation also doesn’t need to be single-shot. Koka continuations are multi-shot.
I feel that “industry programmer uses dependency injection in industry-standard OO languages and to handle polymorphic effects” is actually a validation of the idea of handling effects in new/modern languages - i.e. practicianers and theoreticians kind of agree here!
OO allows you to pass the handlers explictly to object constructors (and not their methods) while non-OO languages might require them to be passed to each function call, or implictly in a dynamically-scoped way - both of which were considered unsuitable in the article, and I think that’s a fair perspective. I expect we could make this would work in a pleasing way to the author in an actor-based language with a first-class effect system, or in other paradigms with better tooling.
One fundamental difference is that mainstream OO languages (and OS’s) don’t go to extremes limiting effects. You can’t limit memory allocation, you can’t “own” a portion of a file system for a duration in a transaction manner, etc, etc - there is still much work to do here so that programming is both safe and ergonomic. You really need something like linear types and lifetimes to cover effects completely. Beyond that, passing every effect handler explicitly through every intermediate function call is tiresome. Dynamically scoped effect handlers are hard to introspect in an IDE (you need to consider all contexts from which some code might be called in order to ctrl-click to effect handler(s), and such support is rarely provided in my experience, and can be challenging for “library code” where all handlers are abstract).
I’m personally quite appreciative of all those out there exploring better/different options for the future.
Abstractions hide details. Whether it’s effects, classes, mixins, macros, modules, libraries, functions, or GOTO, you have to look somewhere other than you currently are in the code to understand what is happening at the site where the code calls the results of using that abstraction.
Are effects like Common Lisp’s conditions system?