hutao

First of all, nice post! I can tell that you put deliberate effort into using a concrete example, introducing a problem and then building up to how to solve it.

However, the continuation monad has limitations. In your example, it serves a similar purpose to an abstract monad "typeclass"; where you can write an abstract "task" function and run it in the Result effect, or the Promise effect, or any other effect. However, this "task" function can only use map/bind/return, and cannot perform any specific "effectful" operation, such as throwing an error or performing async IO. At the point in the code where it performs an operation, it has to pick a concrete type for the continuation result type `t`. So, a function that performs async IO would need to return `K(Promise(b), a)`, and a function that throws an error would need to return `K(Result(b, Nil), a)`. What would be really useful would be to have a function can perform an effectful operation (such as throwing an error) and still return something like `M(b)` for some abstract effect `M`. This is one of the main problems of "effect systems," and to my understanding, what algebraic effects are currently trying to solve.

This is the gist of Andrej Bauer's paper:

- An algebraic theory consists of a "signature" (specifying a set of operation symbols with their arities) and a set of equations about those operations. An algebraic theory is purely syntactic, and does not give meaning to the operations or equations.

- An interpretation of an algebraic theory maps each operation symbol to a concrete mathematical object. It maps syntax to semantics.

- A model is an interpretation in which the algebraic theory's equations hold.

- A free model of an algebraic theory, generated by a set, is basically a model that can be mapped to any other model of the theory generated by the set.

So, an example of an algebraic theory is a group (as in the algebraic structure itself, not the various instances of a group). Its signature consists of the binary operation of combining, the unary operation of inverse, and the nullary operation of identity. The models of a group are its instances, such as the integers under additions and subtraction, or permutation functions on a set. The integers are the free group (that is, the free model of the group) generated by the set {1}.

Algebraic theories can also describe the effects of a programming language (e.g. reader, writer, or state). The free model of an algebraic effect is given by the syntax trees describing its effectful computations. Effect handlers are maps from syntax trees, transforming computations into other computations within the programming language.

> On the other hand I think it would mean that things like Future and general IO wouldn't be algebraic effects.

For what it's worth, Example 2.3 in the paper states that IO is an algebraic effect, albeit one with no equations. What might be confusing is that the handler of the IO effect cannot have the level of concreteness to actually implement the IO operations. Effect handlers only map computations to computations within the "pure" programming language. From the paper:

> What we still lack is a mathematical model of computational effects at the level of the external environment in which the program runs. There is always a barrier between the program and its external environment, be it a virtual machine, the operating system, or the underlying hardware. The actual computational effects cross the barrier, and cannot be modeled as handlers. A handler gets access to the continuation, but when a real computational effects happens, the continuation is not available. If it were, then after having launched missiles, the program could change its mind, restart the continuation, and establish world peace.

I'm curious about the other Stack Exchange sites. Have they seen the same decline as Stack Overflow?

Stack Overflow was the "flagship" product of the Stack Exchange company, and if the company pivots to AI, I wonder what the future holds for the other Q&A sites on the SE network.

I was not looking to disagree with your point, I only wanted to make additional commentary. Sorry if my comment came across the wrong way.

I do think "There are no function colors in Go in the way being discussed," versus "all functions [in Go] are red" are two slightly different ways of formulating the same set of facts, and the distinction between them is insightful, so that was what I wanted to touch upon. Namely, I wanted to point out that there is an "implicit" color within the programming language itself.

Go (and other language with threads) implicitly run inside the "async IO monad." In the function color analogy, what this means is that all functions are red, and the "ordinary" function call corresponds to "await" in languages such as JavaScript or C#.

Async/await is one implementation of cooperative concurrency, where the programmer must explicitly annotate the points where a context switch may occur. However, one can imagine a program transformation that marks every function as async, and makes every function call an await. After making that transformation, the async/await annotations would no longer be necessary. The end result is pre-emptive concurrency, where the runtime may potentially interrupt the active thread at any function call.

To make another analogy, Haskell requires all IO actions to run in the explicit IO monad, while most languages (C, Java, JavaScript, etc.) do not distinguish between "pure" and "impure" functions. Therefore, C, Java, and JavaScript could all be said to implicitly run in the IO monad.

Async IO is also an instance of a monad. In JavaScript, all async functions must run inside the explicit async IO monad, while Go does not distinguish between async and sync functions. Therefore, Go implicitly runs in the async IO monad. This is similar to the aforementioned distinction between cooperative (made explicit to the programmer) and pre-emptive (handled implicitly by the runtime) concurrency.

In fact, Eugenio Moggi, the PL theorist who realized monads could describe programming languages, was not looking for a programmer-facing abstraction. Rather, he was trying to describe the "implicit" monad in a programming language's semantics (such as the IO monad in most programming languages, or the async IO monad in Go).

> Propagating errors up the stack is not the same, because the top-level function is not developing an error return because of the 10-level-nested function. It is developing one because the function it called has one, and apparently, it needs to return it to its local caller. It's a local consideration ...

> By contrast, in a function coloring situation, if the color is wrong 10 layers down, you must change the calling function. It's a non-local consideration. You don't get to decide not to change it. You can't encapsulate it. You don't get a choice. It pollutes the entire stack, forcibly.

I think this is an interesting perspective, where I would raise a counterpoint. Both result types and async/await are instances of monads (the abstraction which approximates the article's idea of a function color, since you mentioned Haskell, I assume you know this). Just as you can "eliminate" the result type by explicitly handling the success and error cases, you could, theoretically, "eliminate" the async function by blocking on it. Doing so would treat the entire async subprogram, at the top-level function boundary, as synchronous IO, while the async subprogram would still benefit from concurrency internal to the function.

Compare Example #1:

    int topLevel() {
      return match fallibleSubprogram() {
        Ok(()) => 0,
        Err(_) => 255,
      };
    }

    Result<(), Err> fallibleSubprogram() {
      let x = f()?;
      let y = g()?;
      return h(x, y);
    }

Compare Example #2:

    int topLevel() {
      block_on(asyncSubprogram);
      return 0;
    }

    async void asyncSubprogram() {
      let promiseX = f();
      let promiseY = g();
      let [x, y] = await Promise.all([promiseX, promiseY]);
      return await h(x, y);
    }

In the above pseudo-code, you have the same program "structure," but the first uses results and the second uses promises. In the latter example, asyncSubprogram() gets called as if it were synchronous, but you still benefit from asynchronicity because f() and g() can execute concurrently within its body.

The main difference is that compared to pattern matching on Result types, programming languages typically make it unidiomatic to block on a promise. There are various reasons why this is the case, but my point is that Result types and async/await are more similar than they may initially appear.

To clarify: ML started out as a scripting language for Robin Milner's proof assistant, LCF. The formal system, or "logic," is implemented in a minimal, trusted kernel, and the proof data structure is protected as an abstract data type that can only be constructed through the trusted kernel. On top of the kernel, tactic scripts may be defined to manipulate proof objects and facilitate proof search/automation.

Then, ML grew into a general-purpose programming language (both OCaml and Standard ML are dialects).

Note that addition also won't overflow if one addend is greater than half the range, but the other addend is still small enough (e.g. for the range -128 to 127, adding 65 + 12 will not overflow, even though 65 is greater than half of 127).

Your intention of having the restricted domain "NonNegativeLessThanHalfMaxValue" is probably so that both addends have the same domain. If you go down that route, perhaps you'll also want the closure property, meaning that the range should also belong to the same set. However, then you have to deal with the overflow problem all over again...

The real point is that when adding two N-bit integers, the range must be N+1 bits, because the "carry bit" is also part of the output. I think this is a scenario where "Parse, Don't Validate" can't easily help, because the validity of the addition is intrinsically a function of both inputs together.