> Conditions and restarts are kind of like try/throw exception handling you know from more mainstream languages, except much more powerful.
This reminds me of the arguments for call/cc in scheme. A very general construct! It can implement exceptions, backtracking, it can even implement "if", so "if" wouldn't even need to be primitive. You know what else lets you do all that? Good old GOTO.
I don't care about "power" for a language construct. I need guarantees a lot more. Does using this construct allow me to put some things in the "that doesn't matter here" bin, so I can focus on some things without worrying about everything at once? GOTO is better at punching holes in bins of compartmentalization, and call/cc isn't much better.
I don't know much about algebraic effects, but usually "algebraic" implies various guarantees about composability and idempotence, which are exactly what you want when dealing with state and the world.
> Does using this construct allow me to put some things in the "that doesn't matter here" bin
I've been doing this year's Advent of Code in Unison (https://unison-lang.org/, no affiliation) and I've found the form of algebraic effects used there (Abilities in Unison parlence) great for "that doesn't matter here".
For example, the `Abort` ability allows me to stop control flow deep down inside my code at without having to "thread" a bunch of monads or Maybes or Eithers through all the intermediate layers.
In one case I also used the `Store` ability to accumulate some metadata about a simulation as it progressed without having to "pollute"[^1] all of the intermediate layers with explicit handling of the metadata.
[^1]: the abilities do appear in the type signatures, though.
One big difference: GOTO ist not bound to any scope. Which ist no wonder, its usually just syntactic sugar for an omnipresent assembly instruction: JMP.
Algebraic effects are less general and play nicer with scoped constructs like finalizers and exceptions. The downside is that they work via stack unwindindig, so they incur some performace penalties.
I highly recommend reading the original article - "Algebraic Effects for the Rest of Us". It demonstrates their operation via Javascript by renaming try/catch, and I think it will answer your questions nicely.
I know that, and I did read that article. I wasn't criticising algebraic effects, I suggested it may indeed have something on the mere "power" of constructs that can implement the same flow.
That said, the article didn't make me much wiser on what's the point. I could sort of see it if it came with guarantees in the type system, I guess.
Yeah thats fair I guess, it IS hard to see whats so special about it.
Imho, it's the same deal as with monads: Outside of pure functional languages with a strong type system there is not much appeal. But for e.g. a Haskell programmer its like the next coming of christ...
But I think it could be very useful if combined with the equivalent of javas checked exceptions, even in other languages.
Hah, when I wrote that I was thinking of qualifying it a bit better to prevent the very obvious objections.
It really depends on the language
and what kind of goto you mean.
But in the context of the post I replied to, yes, because you cannot replace algebraic effects with "neutered" gotos (like the ones in c), you need the equivalent of longjmp, or maybe gosub.
You can obviously design a language where goto does implicitely run finalizers or does similar fancy stuff, but this is again leaving the scope of the original discussion I think...
Goto tags and blocks/return-from have lexical scope and dynamic extent. Lexical scope means that one can goto to enclosing goto tags and one can return from enclosing blocks. "dynamic extent" means that corresponding scoping constructs tagbody and block not have been exited yet.
CATCH/THROW has dynamic scope and dynamic extent. Means that the CATCH targets will be looked up on the stack.
Then Common Lisp has UNWIND-PROTECT, which sets up a dynamic scope. When leaving this scope by a non-local control transfer, it is ensured that some specified code will be executed.
These are then building blocks for higher-level control, like the Condition System, which provides condition types, handlers, restarts, ... which is used then for error handling, where on error the stack is left like it is.
> Assembly lets you jump anywhere
it's just that jumping to some arbitrary place might not make sense.
setjmp/longjmp (aka goto on steroid) is a better example. Algebraic effects are sort of a structured (and, depending on the language, typed) form of sjlj.
As far as I can tell, algebraic effects are a kind of typed delimited continuations. As for call/cc, some people agree that it's too general and powerful for its own good: https://okmij.org/ftp/continuations/against-callcc.html
> The only reward for the hard work to capture the whole continuation efficiently is more hard work to get around the capture of the whole continuation. Both the users and the implementors are better served with a set of well-chosen control primitives of various degrees of generality with well thought-out interactions.
> I don't care about "power" for a language construct. I need guarantees a lot more. Does using this construct allow me to put some things in the "that doesn't matter here" bin, so I can focus on some things without worrying about everything at once?
Conditions and restarts aren’t much better or worse than standard exceptions in that[1] respect.
You can basically implement them[2] on top of those + dynamic scope: the gist is that when an exceptional condition happens, instead of destructively unwinding the stack immediately the code only invokes a callback (selected by condition type, installed by some dynamically enclosing code), which then can choose one of the available handling strategies and unwind the stack to the requisite point (using try / throw if implementing on top of that). The fun part is that it can unwind less than to the point where the callback was installed: e.g. a REPL installs a handler that, on an undefined variable error, asks the user interactively for the value to use instead, invokes the language-provided USE-VALUE restart and proceeds; no debugger-level carnal knowledge of the language runtime is necessary at any point. (Compare also the DOS abort/retry/ignore prompt. Win32 SEH is also capable of expressing a certain degree of resumable exceptions not exposed by C++ runtime, as seen in classic VB’s On Error Resume Next—though that is admittedly a bad idea.)
The advantage[3] of this construct is that it enables you to structure APIs differently, in that the knowledge of how to recover need not exist at the same level as the decision to recover that way. (The potential recovery strategies become part of the API the same way that potential errors are.) That eliminates the “handle-those-errors-this-way” flag awkwardness that exception handling can’t really mitigate. The API-design expressive power, so to say, is different even if the control-flow expressive power[4] is basically the same.
(A minor point is that because there’s no mandatory unwinding, the signalling code can also decide to proceed if the condition is unhandled. This subsumes warning systems such as the one in Python[5]. The point is minor because I haven’t seen those play an important role.)
> I don't know much about algebraic effects, but usually "algebraic" implies various guarantees about composability and idempotence, which are exactly what you want when dealing with state and the world.
The guarantees of composability are the point, yes—compared to monad transformers. In that respect the article, to me, seems to miss some of the point of the algebraic effects research: the languages there usually try to isolate all non-referentially-transparent execution in the effect system, not to introduce it as an additional system. This includes ordinary mutability (of things that outlive a function call, you’re free to mutate temporaries as long as you destroy them at the end). The ultimate in function colouring, so to say. Monads were a previous attempt at the same, and monad transformers do add some composability to them, but using the result kind of sucks. We’ll see how well effects do.
Algebraic effects are also more powerful than resumable exceptions, because exception resumption is usually one-shot—either you resume or you don’t—whereas both Eff and Koka allow you to define a nondeterminism effect that allows you to resume more than once (e.g. for backtracking).
I’d still say the article’s point is interesting, because conditions systems originate from the Lisp tradition and so there doesn’t seem to be a lot of literature on typing them statically. It’s nice to realize that research has already been done under the banner of typing algebraic effects.
I still don't understand how effects allow taming mutability. Can you point me to some resource (possibly understandable by a layman without knowledge of advanced type theory)?
Considering that React with function components is popular and their hook mechanism is seemingly weird, should people also learn algebraic effects as the beautiful theory behind it?
Also, if React hooks is the way to describe UI components, I think the mechanism behind it should be either formalised as a proper language feature in JS or in some new language used for frontend development. For example, I noticed this teaser bit in the first materials about Verse: "The full Verse language also has a statically-checked effect system, including both mutable references and input/output." https://simon.peytonjones.org/verse-calculus/ Discussed earlier here: https://news.ycombinator.com/item?id=33946933
Or is this something that e.g. ClojureScript with Reagent already formalises and we all should study that?
Well there's https://crank.js.org that uses native js generators where you would you normally put hooks in. Never used it but looked like a very neat idea.
I believe Reagent utilises Clojure's native "atom" to accomplish what hooks try to do but with much better language level guarantees.
I guess what js needs is an actual proper language level immutable type, and it wouldn't need all the hooks trickery?
> I don't know much about the scope of the theoretical work there. The missing ingredient is implied to be "continuations", which are not supported in Common Lisp.
„I have a partial understanding of a related concept and zero knowledge on the actual topic, so let me write a blog post“
CL condition system is a strict subset of algebraic effects (or any effect system)
> „I have a partial understanding of a related concept and zero knowledge on the actual topic, so let me write a blog post“
Would you prefer me to not write about related concepts I do know about, or just to omit the disclaimer next time and confidently pretend I know everything?
I believe restarts are a special case of invoking a continuation. The difference in Lisp is that you can't actually capture and pass around the continuation as a first class object, like you can in Scheme, and I don't believe there is a way to invoke more than one restart for a given condition. I think this limited special case covers the majority of what people would want to do with continuations, and prevents people from doing the messy stuff that you shouldn't be doing anyway. From what I recall, the new algebraic effects system in OCaml has similar limitations (you can only invoke the continuation once), and I think Koka has a special case for it in their compiler & encourages it.
This reminds me of the arguments for call/cc in scheme. A very general construct! It can implement exceptions, backtracking, it can even implement "if", so "if" wouldn't even need to be primitive. You know what else lets you do all that? Good old GOTO.
I don't care about "power" for a language construct. I need guarantees a lot more. Does using this construct allow me to put some things in the "that doesn't matter here" bin, so I can focus on some things without worrying about everything at once? GOTO is better at punching holes in bins of compartmentalization, and call/cc isn't much better.
I don't know much about algebraic effects, but usually "algebraic" implies various guarantees about composability and idempotence, which are exactly what you want when dealing with state and the world.