I often see the claim that AE generalizes control flow, so you can (for example) implement coroutines. But the most obvious way I would implement AE in a language runtime is with coroutines, where effects are just syntactic sugar around yield/resume.

What am I missing?

• herrington_d

  today at 7:23 PM

  One thing AE provides but not coroutines is type safety. More concretely AE can specify what a function can do and cannot do lexically in code. A generator/coroutine cannot.

  For example, a function annotated with say `query_db(): User can Datebase` means the function can call database and the caller must provide a `Database` handler to call the `query_db`.

  The constraint of what can do and not is pretty popular in other programming fields, most notably, NextJS. A server component CANNOT use client feature and a client component CANNOt access server db.

• FjordWarden

  today at 7:02 PM

  Yes, this is what Effect-TS is doing for JavaScript, minus the syntactic sugar, but I don't know if this is a good idea in the end. It reminds me of the Spring framework, DI is also a form of AE, but it spreads like cancer through the code. The other day I was watching this talk[1] from EffectDays on how to use effects on the frontend and the entire talk was a dude showing boilerplate that did nothing. I think that AE is a beguiling idea, it lets you express imperative code in a functional language, but in a language like JS the added work of wrapping everything in a function feel like a step down from writing the simples JS you can imagine. Just as a counter example, there is also canvasmotion[2] which also uses coroutines to express scenarios for 2D graphics and this feels like it is making something hard easier.

  [1] https://www.youtube.com/watch?v=G_jp87gxILE [2] https://motioncanvas.io/

I see two downsides. Looking at this snippet:

    my_function (): Unit can AllErrors =
      x = LibraryA.foo ()
      y = LibraryB.bar ()

The second thing to note is that, once you ascertain that foo and bar can fail, how do you find the code that will run when they do fail? You would have to traverse the callstack upwards until you find a 'with' expression, then descend into the handler. And this cannot be done statically (i.e. your IDE can't jump to the definition), because my_function might be called from any number of places, each with a different handler.

I do think this is a really neat concept, but I have major reservations about the readability/debuggability of the resulting code.

• cryptonector

  today at 7:00 AM

  > how do you find the code that will run when they do fail?

  That's part of the point: it's dynamic code injection. You can use shallow- or deep-binding strategies for implementing this just as with any dynamic feature. Dynamic means just that bindings are introduced by call frames of callers or callers of callers, etc., so yes, notionally you have to traverse the stack.

  > And this cannot be done statically (i.e. your IDE can't jump to the definition),

  Correct, because this is a _dynamic_ feature.

  However, you are expected not to care. Why? Because you're writing pure code but for the effects it invokes, but those effects could be pure or impure depending on context. Thus your code can be used in prod and hooked up to a mock for testing, where the mock simply interposes effects other than real IO effects.

  It's just dependency injection.

  You can do this with plain old monads too you know, and that's a much more static feature, but you still need to look way up the call stack to find where _the_ monad you're using might actually be instantiated.

  In other words, you get some benefits from these techniques, but you also pay a price. And the price and the benefit are two sides of the same coin: you get to do code injection that lets you do testing and sandboxing, but it becomes less obvious what might be going on.

• edding4500

  today at 5:38 AM

  I wrote my bachelors thesis about IDE support for lexical effects and handlers: https://se.cs.uni-tuebingen.de/teaching/thesis/2021/11/01/ID...

  All of what you state is very doable.

• zvrba

  today at 6:08 AM

  > [...] how do you find the code that will run when they do fail? You would have to traverse [...]

  I work in a .NET world and there many developers have this bad habit of "interface everything", even if it has just 1 concrete implementation; some even do it for DTOs. "Go to implementation" of a method, and you end up in the interface's declaration so you have to jump through additional hoops to get to it. And you're out of luck when the implementation is in another assembly. The IDE _could_ decompile it if it were a direct reference, but it can't find it for you. When you're out of luck, you have to debug and step into it.

  But this brings me to dependency injection containers. More powerful ones (e.g., Autofac) can establish hierarchical scopes, where new scopes can (re)define registrations; similar to LISP's dynamically scoped variables. What a service resolves to at run-time depends on the current DI scope hierarchy.

  Which brings me to the point: I've realized that effects can be simulated to some degree by injecting an instance of `ISomeEffectHandler` into a class/method and invoking methods on it to cause the effect. How the effect is handled is determined by the current DI registration of `ISomeEffectHandler`, which can be varied dynamically throughout the program.

  So instead of writing

      void DoSomething(...) {
          throw SomeException(...);
      }
  

  you establish an error protocol through interface `IErrorConditions` and write

      void DoSomething(IErrorConditions ec, ...) {
          ec.Report(...);
      }
  

  (Alternately, inject it as a class member.) Now, the currently installed implementation of `IErrorConditions` can throw, log, or whatever. I haven't fully pursued this line of though with stuff like `yield`.

  • SkiFire13

    today at 7:17 AM

    > I work in a .NET world and there many developers have this bad habit of "interface everything", even if it has just 1 concrete implementation

    I work on a Java backend that is similar to what you're describing, but Intellij IDEA is smart enough to notice there is exactly one non-test implementation and bring me to its source code.

    • vrighter

      today at 2:03 PM

      not that familiar with java, but in .net when you do this, it is very common for the implementation to be in a separate assembly, part of a different project

      • cweld510

        today at 2:30 PM

        Doesn’t that imply an interface is necessary though, so you can compile (and potentially release) the components separately? I don’t use .net but this sounds quite similar to pulling things into separate crates in Rust or different compilation units in C, which is frequently good practice.

        • mystifyingpoi

          today at 5:46 PM

          Definitely that could imply the necessity of an interface, but often it's simply done, because everyone working in a project blindly follows an already established poor convention.

  • jiggawatts

    today at 7:52 AM

    The annoyance is that the .NET standard library already does this precise thing, but haphazardly and in far fewer places than ideal.

    ILogger and IProgress<T> comes to mind immediately, but IMemoryCache too if you squint at it. It literally just "sets" and "gets" a dictionary of values, which makes it a "state" effect. TimeProvider might be considered an algebraic effect also.

• abathologist

  today at 5:43 AM

  > The first thing to note is that there is no indication that foo or bar can fail

  I think this is a part of the point: we are able to simply write direct style, and not worry at all about the effectual context.

  > how do you find the code that will run when they do fail

  AFAIU, this is also the point: you are able to abstract away from any particular implementation of how the effects are handled. The code that will when they fail is determined later, whenever you decide how you want to run it. Just as, in `f : g:(A -> B) -> t(A) -> B` there is no way to find "the" code that will run when `g` is executed, because we are abstracting over any particular implementation of `g`.

  • skybrian

    today at 2:53 PM

    In languages like JavaScript, function calls that can throw are completely indistinguishable. In Go, calling a function that can fail is explicit and takes three lines of boilerplate, if you just want to propagate the error. That seems like too much. Rust has the ‘?’ operator, which is one character of boilerplate.

    Though it does add noise, one character of boilerplate to indicate a function call that uses effects seems like the right amount? Functions that use lots of effects will likely have this character on every function call, but that seems like a good indicator that it’s tricky code.

    • empath75

      today at 3:21 PM

      Rust and Go errors are not really effectful in the "side effect" sense, they're just an ordinary return value of a function. There's really no difference between returning a result and any other enum. Otoh, panics are effectful, and that's the kind of thing you'd want to capture in an effect system.

      • skybrian

        today at 6:26 PM

        Sure, but in a language with an effect system, it seems like effects would be used for errors, so it seems worth comparing error-handling techniques.

        Go uses a single base type (interface) for “expected” errors and panics for errors that aren’t normally caught. I suppose those would be two different effects? For the “expected” errors, some kind of annotation on the function call seems useful.

        • aatd86

          today at 7:15 PM

          The way I see it, effects would be implemented/assigned to the function where the error gets logged for instance. But as long as the error value remains local, a function can still be pure all else being equal.

          This is not the case with exception looking code (aka panics) since it escapes normal control flow and I guess makes an error "punch" through stacks as they are unwinded.

          A bit like being thrown toward global state. So if we consider panics as side effectful operations, we would have to change go to explicitly declare panics as side effects with a known function signature.

          I guess one would want the list of side effects to be part of a function signature for full visibility. I wonder how that would influence backward compatibility.

  • nine_k

    today at 5:55 AM

    It looks like exceptions (write the happy path in direct style, etc), but with exceptions, there is a `catch`. You can look for it and see the alternate path.

    What might be a good way to find / navigate to the effectual context quickly? Should we just expect an IDE / LSP color it differently, or something?

    • MrJohz

      today at 6:11 AM

      There's a `catch` with effects as well, though, the effect handler. And it works very similarly to `catch` in that it's not local to the function, but happens somewhere in the calling code. So if you're looking at a function and you want to know how that function's exceptions get handled, you need to look at the calling code.

      • today at 6:25 AM

      • naasking

        today at 3:22 PM

        This is the case anytime errors are propagated to callers instead of handled locally, which is probably most cases.

• MrJohz

  today at 5:27 AM

  > And this cannot be done statically (i.e. your IDE can't jump to the definition), because my_function might be called from any number of places, each with a different handler.

  I believe this can be done statically (that's one of the key points of algebraic effects). It works work essentially the same as "jump to caller", where your ide would give you a selection of options, and you can find which caller/handler is the one you're interested in.

  • HelloNurse

    today at 5:31 PM

    This suggests a novel plausible IDE feature: list callers of a function, but only those with a handler for a certain effect (maybe when the context sensitive command is invoked on the name of one of the effects rather than on the name of the function).

• wavemode

  today at 6:19 AM

  > there is no indication that foo or bar can fail

  Sounds like you're just criticizing try-catch style error handling, rather than criticizing algebraic effects specifically.

  Which, I mean, is perfectly fair to not like this sort of error handling (lack of callsite indication that an exception can be raised). But it's not really a step backward from a vast majority of programming languages. And there are some definite upsides to it as well.

  • skybrian

    today at 3:08 PM

    Since effects are powerful enough to implement generators and cooperative multitasking, it seems like it’s more than just exceptions? Calling some functions could task-switch and do arbitrary computation before returning at some arbitrary time later. It might be nice to know which function calls could do that.

    I’m not a fan of how ‘await’ works in JavaScript because accidentally leaving it out causes subtle bugs. But the basic idea that some function calls are simple and return immediately and others are not makes sense.

    • brokencode

      today at 4:56 PM

      Even regular sync functions in JavaScript can do lots of computations that take a long time. And others perform effects like starting a timer or manipulating the DOM. Should these be indicated with keywords too?

      I agree that await is a nice hint in the code that something more substantial is happening, but ultimately it’s limited and quite opaque.

      Great IDE support for algebraic effects would probably include inline hints to show effects.

      • skybrian

        today at 6:35 PM

        In a language with an effect system, presumably modifying the DOM would be an effect.

        Maybe some effects should have call sites annotated, like ‘async’, and others should not, like DOM manipulation? It seems like an API design issue. What do you want to call out for extra attention?

• tome

  today at 12:35 PM

  > no indication that foo or bar can fail ... how do you find the code that will run when they do fail

  If that's what you're looking for you might want to try my Haskell effects library Bluefin (it's not an "algebraic" effects library, though). The equivalent code would be

      myFunction :: e :> es -> Exception String e -> Eff es r
      myFunction ex = do
        x <- LibraryA.foo ex
        y <- LibraryB.foo ex
        z <- LibraryC.foo
        ...
  

  This answers the first part of your question: the presence of `ex` argument (an `Exception String` handle) shows that a String-value exception can be thrown wherever they are used. For example, we know that `LibraryC.foo` does not throw that exception.

  It also answers the second part of your question: the code that runs on failure is exactly the code that created the `Exception String` handle. Any exception arising from that handle is always caught where the handle was created, and nowhere else. For example, it could be here:

      try $ \ex -> do
          v <- myFunction ex
          ...
  

  `try` catches the exception and turns into into the `Left` branch of a Haskell `Either` type. Or it could be here:

      myFunction :: e :> es -> Exception String e -> Eff es r
      myFunction ex = do
        catch
          (\ex2 -> do
            x <- LibraryA.foo ex
            y <- LibraryB.foo ex2
            z <- LibraryC.foo
            ...)
          (\errMsg -> logErr errMsg)
  

  So the exception thrown by `LibraryB.foo` is always handled with the `logErr` (and nowhere else), and the exception thrown by `LibraryA.foo` is always handled by the exception handler higher up which created `ex` (and nowhere else).

  Let me know what you think!

  • itishappy

    today at 3:27 PM

    Looks slick!

    I'm a bit confused at the distinction of "algebraic" vs "non-algebraic" effects. Think you can give a brief example of what you mean?

    Also, I know you've taken a slightly different direction with Bluefin than other Haskell effects libraries (effects as values vs types). Is this related to the distinction above?

• suspended_state

  today at 2:22 PM

  > The first thing to note is that there is no indication that foo or bar can fail.

  I don't see how this is different from traditional programming.

  > I do think this is a really neat concept, but I have major reservations about the readability/debuggability of the resulting code.

  I don't think that readability will be harmed, but I can understand your concerns about debugging. I feel that cluttering the code with consistency/error checks everywhere actually harms much more readability.

• YmiYugy

  today at 12:28 PM

  I think the readability problem can be solved by having your LSP tell your editor to display some virtual text, indicating that the foo and bar calls might error.

  I have to admit I don't understand the second point. If you could statically determine from the definition of foo and bar what code handles their errors, than there would be no reason for foo or bar to error, they could just call the error handling code. If foo and bar return Result sum types and my_function just passes those errors up, it would be no different. You don't know what callers of my_function would do with those errors.

> You can think of algebraic effects essentially as exceptions that you can resume.

How is this substantively different than using an ApplicativeError or MonadError[0] type class?

> You can “throw” an effect by calling the function, and the function you’re in must declare it can use that effect similar to checked exceptions ...

This would be the declared error type in one of the above type classes along with its `raiseError` method.

> And you can “catch” effects with a handle expression (think of these as try/catch expressions)

That is literally what these type classes provide, with a "handle expression" using `handleError` or `handleErrorWith` (depending on need).

> Algebraic effects1 (a.k.a. effect handlers) are a very useful up-and-coming feature that I personally think will see a huge surge in popularity in the programming languages of tomorrow.

Not only will "algebraic effects" have popularity "in the programming languages of tomorrow", they actually enjoy popularity in programming languages today.

https://typelevel.org/cats/typeclasses/applicativemonaderror...

• SkiFire13

  today at 8:53 AM

  > How is this substantively different than using an ApplicativeError or MonadError[0] type class?

  If you're limiting yourself to just a single effect there's probably not much difference, however once you have multiple effects at the same time then explicit support for them starts to become nicer than nesting monads (which requires picking an order and sometimes reorder them due to the output of some functions not matching the exact set or order of monads used by the calling function).

  • tome

    today at 12:48 PM

    > nesting monads (which requires picking an order and sometimes reorder them due to the output of some functions not matching the exact set or order of monads used by the calling function).

    mtl-style (which is where `MonadError` comes from in Haskell), is exactly to defer picking an order, and indeed a handler, until handling time. (I gather the GP was talking about something in Scala, but I guess it's the same.)

• abathologist

  today at 5:49 AM

  It seems to me that monads and effects are likely best viewed as complementary approaches to reasoning about computational contexts, rather than as rivals. See, e.g., https://goto.ucsd.edu/~nvazou/koka/padl16.pdf or https://goto.ucsd.edu/~nvazou/koka/padl16.pdf .

  • gre

    today at 1:45 PM

    It's the same link twice

    • HelloNurse

      today at 5:35 PM

      A presentation and two more papers:

      https://goto.ucsd.edu/~nvazou/koka/

• davery22

  today at 4:53 AM

  Algebraic effects are in delimited continuation territory, operating on the program stack. No amount of monad shenanigans is going to allow you to immediately jump to an effect handler 5 levels up the call stack, update some local variables in that stack frame, and then jump back to execution at the same point 5 levels down.

  • tome

    today at 12:43 PM

    Quite the opposite, that's exactly what continuation monads do, for example `ContT`, and more structured versions such as `freer`. Those essentially simulate a stack rather than using the actual RTS stack. For the latter there are `eff` and `bluefin-algae` (the latter very much work in progress). So yes, in Haskell at least, monads are the right API for deli meted continuations.

    https://www.stackage.org/haddock/lts-23.15/transformers-0.6....

    https://hackage.haskell.org/package/freer-0.2.4.1

    https://github.com/lexi-lambda/eff

    https://hackage.haskell.org/package/bluefin-algae

  • grg0

    today at 5:05 AM

    That sounds like a fucking nightmare to debug. Like goto, but you don't even need to name a label.

    • cryptonector

      today at 7:02 AM

      > Like goto, but you don't even need to name a label.

      That's what exceptions are.

      But effects don't cause you to see huge stack traces in errors because the whole point is that you provide the effect and values expected and the code goes on running.

    • agumonkey

      today at 10:11 AM

      clos condition system is said to be just that, people seem to like it

      also this kind of non local stack/tree rebinding is one way to implement prolog i believe

    • vkazanov

      today at 6:31 AM

      Well, you test the fact that the handler receives the right kind of data, and then how it processes it.

      And it is useful to be able to provide these handlers in tests.

      Effects are AMAZING

• tel

  today at 4:52 PM

  They're pretty similar, but with different ergonomics. Algebraic effects are similar to some kind of "free" monad technique, but built in. For being built in they have nicer syntax and better composability, often. You can achieve the same in a language suitably dedicated to monadic approaches (Haskell being the poster child here) but it helps to have type class inference (giving you mtl-like composability) and built-in bind syntax a la Haskell's `do` or Scala's `for`.

  • HelloNurse

    today at 5:33 PM

    What is "mtl"?

• cryptonector

  today at 4:39 AM

  > How is this substantively different than using an ApplicativeError or MonadError[0] type class?

  It think it's about static vs. dynamic behavior.

  In monadic programming you have to implement all the relevant methods in your monad, but with effects you can dynamically install effects handlers wherever you need to override whatever the currently in-effect handler would be.

  I could see the combination of the two systems being useful. For example you could use a bespoke IO-compatible monad for testing and sandboxing, and still have effects handlers below which.. can still only invoke your IO-like monad.

  • tome

    today at 12:46 PM

    > with effects you can dynamically install effects handlers wherever you need to override whatever the currently in-effect handler would be.

    You can do that with mtl-style too. It's just more clumsy.

• tome

  today at 12:49 PM

  For the MonadError in Haskell at least, it's quite similar. However, mtl-style has a number of issues that effect systems don't well explained by the author of effectful under "What about mtl?" at https://hackage.haskell.org/package/effectful.

• threeseed

  today at 6:39 AM

  > they actually enjoy popularity in programming languages today

  They have enjoyed popularity amongst the Scala FP minority.

  They are not broadly popular as they come with an unacceptable amount of downsides i.e. increased complexity, difficult to debug, harder to instantly reason about, uses far more resources etc. I have built many applications using them and the ROI simply isn't there.

  It's why Odersky for example didn't just bundle it into the compiler and instead looked at how to achieve the same outcomes in a simpler and more direct way i.e. Gears, Capabilities.

• anon-3988

  today at 4:17 AM

  I don't really get it, but is this related to delimited continuation as well?

  • tempodox

    today at 4:36 AM

    Yes, see for instance https://github.com/ocaml-multicore/ocaml-effects-tutorial.

    • cryptonector

      today at 7:03 AM

      That's just an implementation detail. I don't think there's anything about effects that _requires_ delimited continuations to implement them.

      • tome

        today at 12:45 PM

        If you want multishot continuations then I don't really know of any way other than delimited continuations (other than undelimeted continuations or simulating delimited continuations, on the heap).

        • cryptonector

          today at 4:09 PM

          Why can't the handler be invoked as if it was called from the effect invocation site, then return?

          But apart from that and to answer your question there is an alternative to delimited continuations, and that's undelimited continuations (which essentially requires allocating call frames on the heap).

          • Rusky

            today at 4:21 PM

            The handler doesn't have to follow the pattern of "do its work, resume the computation, go away."

            It can instead do things like "do some work, resume the computation, do some more work."

            Or even more invasively, "stash the computation somewhere, return from the handler site, let the rest of the program run for a while, then resume the computation."

This Ante "pseudocode" is wonderful! It's like Haskell with Elixir's expressiveness, flavor and practicality. A Haskell for developers. Waiting for the compiler to mature. I would love to develop apps in Ante.

Algebraic effects seem very interesting. I have heard about this idea before, but assumed that it somehow belonged into the territory of static type systems. I am not a fan of static type systems, so I didn't look further into the idea.

But I found these two articles [1] about an earlier dynamic version of Eff (the new version is statically typed), which explains the idea nicely without introducing types or categories (well, they use "free algebra" and "unique homomorphism", just think "terms" and "evaluation" instead). I find it particularly intriguing that what Andrej Bauer describes there as "parameterised operation with generalised arity", I would just call an abstraction of shape [0, 1] (see [2]). So this might be helpful for using concepts from algebraic effects to turn abstraction algebra into a programming language.

[1] https://math.andrej.com/2010/09/27/programming-with-effects-...

[2] http://abstractionlogic.com

• nicoty

  today at 7:44 AM

  What's wrong with static type systems?

  • practal

    today at 8:49 AM

    I've summarized my opinion on this here: https://doi.org/10.5281/zenodo.15118670

    In normal programming languages, I see static type systems as a necessary evil: TypeScript is better than JavaScript, as long as you don't confuse types with terms...

    But in a logic, types are superfluous: You already have a notion of truth, and types just overcomplicate things. That doesn't mean that you cannot have mathematical objects x and A → B, such that x ∈ A → B, of course. Here you can indeed use terms instead of types.

    So in a logic, I think types represent a form of premature optimisation of the language that invariants are expressed in.

    • chongli

      today at 2:09 PM

      Your invocation of Strong AI (in the linked paper) seems like a restatement of the Sufficiently Smart Compiler [1] fallacy that’s been around forever in programming language debates. It’s hypothetical, not practical, so it doesn’t represent a solution to anything. Do you have any evidence to suggest that Strong AI is imminent?

      [1] https://wiki.c2.com/?SufficientlySmartCompiler

      • practal

        today at 3:00 PM

        I routinely describe code that I want in natural language, and it generates correct TypeScript code for me automatically. When it gets something wrong, I see that it is because of missing information, not because it is not smart enough. If I needed any more evidence for Strong AI since AlphaGo, that would be it.

        I wouldn't call it vibe coding; I just have much more time to focus on the spec than on the code. I'd call that a sufficiently smart compiler.

    • frumplestlatz

      today at 9:15 AM

      This is a very reductive definition of types, if not a facile category error entirely (see: curry-howard), and what you call "premature optimization" -- if we're discussing type systems -- is really "a best effort at formalizations within which we can do useful work".

      AL doesn’t make types obsolete -- it just relocates the same constraints into another formalism. You still have types, you’re just not calling them that.

      • practal

        today at 9:45 AM

        I think I have a reference to Curry in my summary link. Anyways, curry-howard is a nice correspondence, about as important to AL as the correspondence between the groups (ℝ, 0, +) and (ℝ \ 0, 1, *); by which I mean, not at all. But type people like bringing it up even when it is not relevant at all.

        No, sorry, I really don't have types. Maybe trying to reduce all approaches to logic to curry-howard is the very reductive view here.

        • frumplestlatz

          today at 10:12 AM

          If your system encodes invariants, constrains terms, and supports abstraction via formal rules, then you’re doing the work of types whether you like the name or not.

          Dismissing Curry–Howard without addressing its foundational and extricable relevance to computation and logic isn’t a rebuttal.

          • practal

            today at 10:24 AM

            Saying "Curry-Howard, Curry-Howard, Curry-Howard" isn't an argument, either.

            I am not saying that types cannot do this work. I am saying that to do this work you don't need types, and AL is the proof for that. Well, first-order logic is already the proof for that, but it doesn't have general binders.

            Now, you are saying, whenever this work is done, it is Curry-Howard, but that is just plain wrong. Curry-Howard has a specific meaning, maybe read up on it.

            • frumplestlatz

              today at 10:55 AM

              Curry–Howard applies when there’s a computational interpretation of proofs — like in AL, which encodes computation and abstraction in a logic.

              You don’t get to do type-like work, then deny the structural analogy just because you renamed the machinery. It’s a type system built while insisting type systems are obsolete.

              • practal

                today at 11:38 AM

                You seem to know AL very well, I didn't even know that there is a computational interpretation of AL proofs! Can you tell me what it is?

    • _flux

      today at 9:20 AM

      Personally I would enjoy if TLA+ would have types, though, and TLA+ belongs to the land of logic, right? I do not know how it differs from the abstraction logic referred in your writing and your other whitepapers.

      What is commonly used is a TypeOK predicate that verifies that your variables have the expected type. This is fine, except your intermediate values can still end up being of mis-intended values, so you won't spot the mistake until you evaluate the TypeOK predicate, and not at all if the checker doesn't visit the right corners of the state space. At least TypeOK can be much more expressive than any type system.

      There is a new project in the same domain called Quint, it has types.

      • practal

        today at 9:30 AM

        Practically, in abstraction logic (AL) I would solve that (AL is not a practical thing yet, unlike TLA+, I need libraries and tools for it) by having an error value ⊥, and making sure that abstractions return ⊥ whenever ⊥ is an argument of the abstraction, or when the return value is otherwise not well-defined [1]. For example,

            div 7 0 = ⊥, 
        

        and

            plus 3 ⊥ = ⊥, 
        

        so

            plus 3 (div 7 0) = ⊥.
        
        

        In principle, that could be done in TLA+ as well, I would guess. So you would have to prove a predicate Defined, where Defined x just means x ≠ ⊥.

        [1] Actually, it is probably rather the other way around: Make sure that if your expression e is well-defined under certain preconditions, that you can then prove e ≠ ⊥ under the same preconditions.

        • thechao

          today at 12:40 PM

          This looks like you've defined the abstract lattice extension as a proper superset of the concrete semantics. That sort of analysis is entirely subsumed by Cousot & Cousot's work, right? Abstract Interpretation doesn't require static types; in fact, the imposition of a two-level interpretation is secondary. The constraints on the pre-level are so that the behavior of the program can be checked "about as quickly as parsing", while also giving strong correctness guarantees under the systems being checked.

          Moving the whole thing to dynamic behavior doesn't tell us anything new, does it? Lisps have been tagged & checked for decades?

          • practal

            today at 1:45 PM

            I have not defined any "abstract lattice extension" explicitly; which is nice, why would I need to know about lattices for something as simple as this? It is just a convention I suggest to get a useful Defined predicate, actually. Nobody can stop you from defining mul 0 ⊥ = 0, for example, and that might make sense sometimes.

            I would suggest that abstraction logic compares to type theory as Lisp compares to Standard ML; but that is just an analogy and not precise.

            • thechao

              today at 5:29 PM

              My problem with your interaction on this forum, so far, is that it kind of ignores the practical (artisan) craft of programming. The use of static type systems by working engineers isn't math; it's more akin to "fast, formal checking". You can assert that you don't like types, or they're useless all day long; but, every working engineer knows you're wrong: static type systems have solved a real problem. Your arguments need to be rooted in the basic experience of a working engineer. Single-level programming has its place, but runtime checking is too error prone in reality to build large software. If you think this isn't true, then you need to show up to the table with large scale untyped software. For instance: the FORTH community has real advantages they've demonstrated. Where's your OS? Your database? Your browser? If you have real advantages then you'd have these things in hand, already.

              Otherwise, you're just another academic blowhard using a thin veneer of formalism to justify your own motivated reasoning.

              • practal

                today at 6:02 PM

                Strong opinion! Also, it seems you didn't read my interaction so far carefully enough. You also didn't read the summary I linked to, otherwise you would know that I fully approve the current use of types in programming languages, as they provide lightweight formal methods (another name for what you call "fast, formal checking"). But I think we will be able to do much better, we will have fast, formal checking without static types. Not today, not tomorrow, but certainly not more than 10 years from here.

      • deredede

        today at 10:15 AM

        > At least TypeOK can be much more expressive than any type system.

        Can you clarify what you mean by that? Dependent types or more practically refinement types (à la F*) can embed arbitrary predicates.

    • exceptione

      today at 9:38 AM

      > But in a logic,

      I am not sure if I misunderstand you. Types are for domain, real world semantics, they help to disambiguate human language, they make context explicit which humans just assume when they talk about their domain.

      Logic is abstract. If you implied people should be able to express a type system in their host language, that would be interesting. I can see something like Prolog as type annotations, embedded in any programming language, it would give tons of flexibility, but then you shift quite some burden onto the programmer.

      Has this idea been tried?

      • practal

        today at 10:00 AM

        Types for real-world semantics are fine, they are pretty much like predicates if you understand them like that.

        The idea to use predicates instead of types has been tried many times; the main problem (I think) is that you still need a nice way of binding variables, and types seem the only way to do so, so you will introduce types anyway, and what is the point then? The nice thing about AL is that you can have a general variable binding mechanism without having to introduce types.

        • frumplestlatz

          today at 11:16 AM

          AL as described sounds like it reinvents parts of the meta-theoretic infrastructure of Isabelle/HOL, but repackaged as a clean break from type theory instead of what it seems to be — a notational reshuffling of well-trod ideas in type theory.

          What am I missing?

          • practal

            today at 2:52 PM

            Given that I am an Isabelle user and/or developer since about 1996, similarities with Isabelle are certainly not accidental. I think Isabelle got it basically right: its only problem (in my opinion) is that it is based on intuitionistic type theory as a metalogic and not abstraction logic (nevertheless, most type theorists pretty much ignored Isabelle!). Abstraction logic has a simple semantics; ITT does not. My bet is that this conceptual simplicity is relevant in practice. We will see if that is actually the case or not. I've written a few words about that in the abstraction logic book on page 118, also available in the sample.

            > — a notational reshuffling of well-trod ideas in type theory

            Always fun to encounter disparaging comments (I see that you deleted the other one in the other thread), but I wrote this answer more for the other readers than for you.

    • cardanome

      today at 1:24 PM

      Is there any programming language based on abstraction logic?

      This is all a bit too abstract for me right now but seems interesting.

      • practal

        today at 2:39 PM

        There is nothing practically usable right now. I hope there will be before the end of the year. Algebraic effects seem an interesting feature to include from the start, they seem conceptually very close to abstraction algebra.

    • agumonkey

      today at 10:06 AM

      I'm not a logician but do you mean that predicates and their algebra are a more granular and universal way to describe what a type is.. basically that names are a problem ?

      • practal

        today at 10:15 AM

        Yes and no. Yes, predicates are more flexible, because they can range over the entire mathematical universe, as they do for example in (one-sorted) first-order logic. No, names are not a problem, predicates can have names, too.

        • agumonkey

          today at 12:09 PM

          so if names are not an issue, the problem with the usual static type systems is that they lack a way to manipulate / recombine user defined types to avoid expressive dead ends ?

          • practal

            today at 3:30 PM

            What is the type of x / y, for x : ℝ and y : ℝ?

            • agumonkey

              today at 6:33 PM

              I'm tempted to say ℝ but it seems too obvious

  • hinoki

    today at 8:30 AM

    Forget it Jake, it’s land of Lisp.

After spending a lot if time in Prolog, I want a nice way to implement and compose nondeterministic functions and also have a compile time type check. I’m eyeing all of these languages as a result. I’ll watch Ante as well. (Don’t forget developer tools like an LSP, tree-sitter or other editor plugins).

I did protohackers in ocaml 5 alpha a couple of years ago with effects. It was fun, but the toolchain was a lil clunky back then. This looks and feels very similar. Looking forward to seeing it progressing.

• abathologist

  today at 5:35 AM

  Effects in OCaml 5.3 are quite a bit cleaner than there were a few years back (tho still not typed).

What once was old is new again.

https://lisp-docs.github.io/cl-language-reference/chap-9/j-b...

https://jacek.zlydach.pl/blog/2019-07-24-algebraic-effects-y...

AE (algebraic effect) are very interesting! Great article, thank you.

Reading through, I have some concerns about usability in larger projects, mainly because of "jumping around".

> Algebraic effects can also make designing cleaner APIs easier.

This is debatable. It adds a layer of indirection (which I concede is present in many real non-AE codebases).

My main concern is: When I put a breakpoint in code, how do I figure out where the object I work with was created? With explicit passing, I can go up and down the stack trace, and can find it. But with AE composition, it can be hard to find the instantiation source -- you have to jump around, leading to yo-yo problem [1].

I don't have personal experience with AE, but with python generators, which the article says they are the same (resp. AE can be used to implement generators). Working through large complex generator expressions was very tedious and error-prone in my experience.

> And we can use this to help clean up code that uses one or more context objects.

The functions involved still need to write `can Use Strings` in their signature. From practical point of view, I fail to see the difference between explicitly passing strings and adding the `can Use Strings` signature -- when you want add passing extra context to existing functions, you still need to go to all of them and add the appropriate plumbing.

---

As I understand it, AE on low level is implemented as a longjmp instruction with register handling (so you can resume). Given this, it is likely inevitable that in a code base where you have lots of AE, composing in various ways, you can get to a severe yo-yo problem, and getting really lost in what is the code doing. This is probably not so severe on a single-person project, but in larger teams where you don't have the codebase in your head, this can be huge efficiency problem.

Btw. if someone understands how AE deal with memory allocations for resuming, I'd be very interested in a good link for reading, thank you!

[1]: https://en.wikipedia.org/wiki/Yo-yo_problem

I might be a bit dense but I didn't quite get it and the examples didn't help me. For instance, the first example SayMessage. Is it supposed to be an effect? Why? From the function signature it could well be a noop and we wouldn't know the difference. Or is it arbitrarily decided? Is this all about notations for side-effectful operations?

• scalaisneat

  today at 1:28 PM

  because it is declared as an effect - and implements a handle.

  Think of it more like an interface. It turns out that many common patterns - async, IO, yielding can all be expressed with a handle - and the effect can be represented in the signature.

  This allows the code to have which effect its ran in, at runtime - other commenters pointed out its very similar to dependency injection.

  • aatd86

    today at 7:04 PM

    Ok so we are basically defining a named function signature that represents a side effect shape.

    Then the implementation of these side effect is done elsewhere and assigned as the capability of a function, which is now deemed as impure by the compiler.

    You're right, it looks a bit like an interface.

• anon-3988

  today at 1:13 PM

  if I have to guess, it's something like this function will call fopen, fwrite, etc somewhere downstream.

  of course I am hoping to get corrected on this.

  • lblume

    today at 6:13 PM

    It might, if the effect is handled using these functions. You could also handle the effect using another handler, doing something entirely different. It is up to the caller how to handle effects, or propagate them up.

When I see a new (for me) idea coming from (presumably) category theory I wonder if it really will land in any mainstream language. In my experience having cohesion on the philosophical level of the language is the reason why it is nice to work with it in a team of programmers who are adept in both programming and in the business context. A set of programming patterns to solve a problem usually can be replaced with a possibly disjunct set of patterns where both solutions have all the same ilities in the code and solve the business problem.

My question is - can a mainstream language adopt the algebraic effects (handlers?) without creating deep confusion or a new language should be built from the ground up building on top of these abstractions in some form.

• ww520

  today at 8:25 AM

  > can a mainstream language adopt the algebraic effects (handlers?) without creating deep confusion or a new language should be built from the ground up building on top of these abstractions in some form.

  Algebraic Effect is a variant/enhancement of dependency injection formalized into a language. Dependency injection has massive usage in the wild for a long time with just library implementation.

  • threeseed

    today at 10:12 AM

    > Algebraic Effect is a variant/enhancement of dependency injection

    Every library so far that has implemented effects e.g. Cats, ZIO, Effects has done so to make concurrency easier and safer.

    Not for dependency injection.

• nwienert

  today at 8:00 AM

  React hooks are them, basically. Not at the language level, but widely adopted and understood.

> You can think of algebraic effects essentially as exceptions that you can resume.

So conditions in Common Lisp? I do love the endless cycle of renaming old ideas

• valcron1000

  today at 6:17 AM

  No, algebraic effects are a generalization that support more cases than LISP's condition system since continuations are multi-shot. The closest thing is `call/cc` from Scheme.

  Sometimes making these parallelism hurts more than not having them in the first place

  • wild_egg

    today at 1:19 PM

    Ah multi-shot does make a big difference, thanks for clarifying!

• riffraff

  today at 5:16 AM

  Also literal "resumable exceptions" in Smalltalk.

• Rusky

  today at 4:28 PM

  What a thought-terminating way to approach an idea. Effects are not simply renamed conditions, and we have a whole article here describing them in more detail than that one sentence, so you can see some of the differences for yourself.

• ww520

  today at 6:50 AM

  Also dependency injection.

This is neat, but you don’t need a new language to leverage these concepts. https://effect.website/ The effect library brings all of this goodness to typescript (and then some) and is robust and production ready. I hate writing typescript without it these days.

• chamomeal

  today at 2:53 PM

  I’ve heard that using effect in TS almost like using another language. Like it’s “all or nothing”, either your whole program is using effect or it’s not. But obvi you can still use all of typescript’s features and ecosystem.

  Do you also feel like effect is “or or nothing”? Or could you enclose certain parts of a program into effect parts?

  • evelant

    today at 3:33 PM

    You can definitely only write parts of your app in effect. That’s what I do and it works great. Just be mindful about where you want that boundary between effect and non effect parts to be and it’s easy. The effect parts end up so much more maintainable and robust.

Have you thought of using generators as a closest example to compare effects to? I think they are much closer to effects than exceptions are. Great explainer anyway, it was tge first time I have read about this idea and it was immediately obvious

• yen223

  today at 7:18 AM

  Exceptions are usually used because the syntax for "performing" exceptions (throw) vs handling exceptions (try-catch) is familiar to most programmers, and is basically the same as the syntax for "performing" an effect vs handling the effect, except that the latter also includes resuming a function.

  It would be cool to see how generators will be implemented with algebraic effects.

Maybe I'm too archaic but I do not share the author's hope that algebraic effects will ever become prevalently used. They certainly can be useful now and then, but the similitude with dynamic scoping brings too many painful memories.

• threeseed

  today at 7:03 AM

  I wouldn't worry. Even the simplest and most friendly effects library: https://effect.website

  Shows clearly why they will never be a mainstream concept. The value proposition is only there when you have more elaborate concurrency needs. But that is a tiny fraction of the applications most people are writing today.

  • lblume

    today at 6:18 PM

    > the simplest and most friendly effects library

    Highly unlikely. JavaScript simply isn't a language built with this kind of evaluation model in mind, so an external library introducing completely orthogonal concepts surely should not be modeled as "most friendly". Don't get me wrong — Effect can be great! But the library also deliberately does not market itself as simple, rather as modular and multi-faceted, a "toolbox" from which developers may (should?) choose some tools and omit others.

    A language that supports effects first-hand, like the proposed "Ante", would provide a much a more expressive, possibly simpler, and definitely friendlier approach than TS effect ever could.

I kinda want algebraic effects but where you can locally declare that certain effects are implicit/invisible in the types.

The state effects example seems unlike the others - the examples avoid syntax for indentation, omit polymorphic effect mention and use minimal syntax for functions - but for state effects you need to repeat "can Use Strings" each function? Presumably one may want to group those under type Strings or can Use Strings, at which point you have a namespace of sorts...

It feels powerful. I think the effects in return types could be inferred.

But I share the concerns of others about the downsides of dependency injection. And this is DI on steroids.

For testing, I much prefer to “override” (mock) the single concrete implementation in the test environment, rather than to lose the static caller -> callee relationship in non-test code.

As I understand it this was the inspiration for React's hooks model. The compiler won't give you the same assurances but in practice hooks do at least allow to inject effects into components.

• YuukiRey

  today at 6:35 AM

  I don’t see the similarity. Since hooks aren’t actually passed to, or injected into components, there’s no way to evaluate the same hooks in different ways.

  I can’t have a hook that talks to a real API in one environment but to a fake one in another. I’d have to use Jest style mocking, which is more like monkey patching.

  From the point of view of a React end user, there’s also no list of effects that I can access. I can’t see which effects or hooks a component carries around, which ones weren’t yet evaluated, and so on.

  • tubthumper8

    today at 6:22 PM

    This post from the React team has more detail on that topic: https://overreacted.io/algebraic-effects-for-the-rest-of-us/

  • ollysb

    today at 3:05 PM

    You're right, it's the use of the Context that allows for the injection of the effects. It's also all handled at runtime which does unfortunately mean that the contexts supplying the effects can't be required at compile time.

• ww520

  today at 6:36 AM

  It's different. Hooks in React is basically callback on dependency of state changes. It's more similar to the signaling system.

What’s the advantage here of using effects over monads? It seems to me that all the proposed benefits of effects are reproducible/reproduced already by monads. Is it simply to get stateful actions while still being pure in a dynamic type system rather than static?

• hocuspocus

  today at 5:31 PM

  Better ergonomics, direct style syntax, no need for monad transformers. There might be second order advantages like small performance gains compared to monadic effects.

First time in a long while where I’ve read the intro to a piece about new programming languages and not recognized any of the examples given at all even vaguely. How times change!

This doesn't give a focused explaination on why. I don't see how dependency injection is a benefit when languages without algebraic effects also have dependency injection. It doesn't explain if this dependency injections is faster to execute or compile or what.

• cryptonector

  today at 7:12 AM

  It's the same as with monads:

  1) Testing. Write pure code with "effects" but, while in production the effects are real interactions with the real world, in testing they are mocked. This allows you to write pure code that does I/O, as opposed to writing pure code that doesn't do I/O and needs a procedural shell around it that does do the I/O -- you get to write tests for more of your code this way.

  2) Sandboxing. Like in (1), but where your mock isn't a mock but a firewall that limits what the code can do.

  (2) is a highly-desirable use-case. Think of it as a mitigation for supply-chain vulnerabilities. Think of log4j.

  Both of these are doable with monads as it is. Effects can be more ergonomic. But they're also more dynamic, which complicates the implementations. Dynamic features are always more costly than static features.

  • charcircuit

    today at 8:13 AM

    Again you are listing things that are possible but not explaining why it's better to do it via algebraic effects as opposed to the alternatives.

    For example if you were in a meeting with Oracle to try and convince them to invest 100 million dollars for adding algebraic effects to Java and its ecosystem how would you convince them it would be providing enough value to developers to justify it over some other improvement they may want to do.

    For example, "Writing mocks for tests using algebraic effects is better than using jmock because ..."

    • threeseed

      today at 1:19 PM

      Take the following requirement:

      "A user has made an API call. I want you to in parallel race two concurrent tasks: check if the data is in (1) cache and (2) database. Whichever returns fastest return to the user. Otherwise kill the other task mid-flight and make sure the connection resources for both are cleaned up".

      This is trivial with an effect systems like ZIO and it will work flawlessly. That's the benefit of effect systems. Use cases like this are made easy.

      But now with JVM Virtual Threads there are frameworks like Ox: https://github.com/softwaremill/ox which allow you to achieve the same thing without effects. And how many times do you really need that sort of capability ?

    • cryptonector

      today at 8:38 AM

      The only reason I can think of -but I'm not the right person to ask- is ergonomics, that in many cases it might be easier to push an effect handler than to build a whole monad or whatever. Elsewhere in this thread there's talk of effects solving the color problem.

• yen223

  today at 4:38 AM

  The way dependency injection is implemented in mainstream languages usually involves using metaprogramming to work around the language, not with the language. It's not uncommon to get errors in dependency-injected code that would be impossible to get with normal code.

  It's interesting to see how things can work if the language itself was designed to support dependency injection from the get-go. Algebraic effects is one of the ways to achieve that.

  • vlovich123

    today at 4:41 AM

    Don’t algebraic effects offer a compelling answer to the color problem and all sorts of related similar things?

    • threeseed

      today at 6:55 AM

      But they also introduce their own color-like problems.

      For example with Scala we have ZIO which is an effect system where you wrap all your code in their type e.g. getName(): ZIO[String]. And it doesn't matter if getName returns immediately or in the future which is nice.

      But then the problem is that you can't use normal operators e.g. for/while/if-else you need to use their versions e.g. ZIO.if / ZIO.repeat.

      So you don't have the colour problem because everything is their colour.

      • OtomotO

        today at 7:15 AM

        But that's only a problem if it's a library and not done on the language level?!

        • threeseed

          today at 7:38 AM

          But in the research languages listed they still are colouring function types.

          So it doesn't seem to matter whether it's a library or in the language.

          Either everything is an effect. Or you have to deal with two worlds of code: effects and non-effects.

  • charcircuit

    today at 5:34 AM

    >It's interesting

    Which is why I was asking for that interesting thing to be written in the article on why it would better.

With AE you get for free: generators, stackful coroutines, dependency injection, "dynamic" variables (as in anti-lexical ones), resumable exceptions, advanced error handling and much more. all packaged neatly into ONE concept. I dream of TS and Effekt some day merging :)

• evelant

  today at 2:48 PM

  You can already have all of this goodness (and then some) in typescript https://effect.website/ -- Writing TS without Effect is difficult for me now, it's like a whole new and better language.

I like the idea of Algebraic effects but I'm a little skeptical of the amount of extra syntax.

Let's say I'm building a web server, my endpoint handler now needs to declare that it can call the database, call the s3, throw x, y and z... And same story for most of the functions it calls itself. You solved the "coloration problem" at the cost of adding a thousand colors.

Checked exceptions are the ideal error handling (imho) but no one uses them properly because it's a hassle declaring every error types a function may return. And adding an exception to a function means you need to add/handle it in many of its callers, and their callers in turn, etc.

• hocuspocus

  today at 2:46 PM

  Two things:

  - Only your outermost application entry-point will need to stack all effects; you'll wire the server, client, DB and so on in your `main` method that returns Unit \ (IO & Abort & Result & Transaction & Env ...). In specific modules individual functions should use only the narrowest effect.

  - Good ergonomics for type polymorphism and type inference are obviously paramount to adding algebraic effects in a way that is minimally invasive. It's obviously not trivial and mostly a PL research field at this point, but existing implementations show that there's potential for better DX compared to alternatives (monadic effect systems, mostly).

Yet another thing Common Lisp programmers have been doing since the time of hoe and axe.

• ctenb

  today at 7:16 AM

  But Lisp is untyped, which is a major difference. EDIT: dynamically typed I mean

  • today at 7:26 AM

Just seems to be a way of organising code really.