Contrary to the claim from the comment you are replying to, according to Andrej Bauer, "algebraic" does not refer to the composition of different algebraic effects via composing their handlers.

When you see "algebra," think "algebraic structure," i.e., a set of operations and a set of equational laws on those operations.

An algebraic effect consists of a set of effectful operations. In that sense, each algebraic effect (reader, state, etc.) defines its own algebraic structure. In theory, the operations of an effect should also be related to each other by laws. Here is an example for the state effect from Andrej Bauer's paper:

    lookup(ℓ,λs.lookup(ℓ,λt.κst)) = lookup(ℓ,λs.κss)
    lookup(ℓ,λs.update((ℓ,s),κ)) = κ()
    update((ℓ,s),λ_.lookup(ℓ,κ)) = update((ℓ,s),λ_.κs)
    update((ℓ,s),λ_.update((ℓ,t),κ)) = update((ℓ,t),κ)

However, monads that cannot be defined in this equational style cannot be translated to algebraic effects. An example is the continuation monad: https://old.reddit.com/r/haskell/comments/44q2xr/is_it_possi... (I think you are involved in the Reddit comment chain that I'm linking to...)

AFAIK, another example is the "exception" monad, because the way that you interact with it is through the handler itself. I once saw a thread on r/Haskell discussing this, but can't find it.

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 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.

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).

> 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);
    }

    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);
    }

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.

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

There is one situation, however, where Standard ML prefers currying: higher-order functions. To take one example, the type signature of `map` (for mapping over lists) is `val map : ('a -> 'b) -> 'a list -> 'b list`. Because the signature is given in this way, one can "stage" the higher-order function argument and represent the function "increment all elements in the list" as `map (fn n => n + 1)`.

That being said, because of the value restriction [0], currying is less powerful because variables defined using partial application cannot be used polymorphically.

[0] http://mlton.org/ValueRestriction

@dang I think the account that I'm replying to might be a bot?

The article mixes together two distinct points in a rather muddled way. The first is a standard "premature optimization is the root of all evil" message, reminding us to profile the code before optimizing. The second is a reminder that async functions compile down to a state machine, so the optimization reasoning for sync functions don't apply.

[0] https://www.joelonsoftware.com/2002/11/11/the-law-of-leaky-a...

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.

EDIT: Parent comment was edited to amend the "impossible/unrepresentable" wording

Alexis King, the author of the original "Parse, Don't Validate" article, also published a follow-up, "Names are not type safety" [0] clarifying that the "newtype" pattern (such as hiding a nonzero integer in a wrapper type) provide weaker guarantees than correctness by construction. Her original "Parse, Don't Validate" article also includes the following caveat:

> Use abstract datatypes to make validators “look like” parsers. Sometimes, making an illegal state truly unrepresentable is just plain impractical given the tools Haskell provides, such as ensuring an integer is in a particular range. In that case, use an abstract newtype with a smart constructor to “fake” a parser from a validator.

So, an abstract data type that protects its inner data is really a "validator" that tries to resemble a "parser" in cases where the type system itself cannot encode the invariant.

The article's second example, the non-empty vec, is a better example, because it encodes within the type system the invariant that one element must exist. The crux of Alexis King's article is that programs should be structured so that functions return data types designed to be correct by construction, akin to a parser transforming less-structured data into more-structured data.

[0] https://lexi-lambda.github.io/blog/2020/11/01/names-are-not-...

Here's another way to explain this:

As you state, Prop has to do with proof-irrelevance. When doing constructive mathematics, proofs are programs (meaning they carry computational content), but sometimes it's useful to treat any two proofs of the same proposition as equal. As a consequence, proofs cannot be inspected or run as programs, and you get back the Law of Excluded Middle from classical mathematics.

Decidable has to do with decidability. This means that given some proposition P, there is an algorithm that can either produce a proof of P, or a proof of ~P. This is usually useful when P is a predicate, so that at each x, P(x) either has a proof or a disproof.

In classical mathematics, the Law of Excluded Middle holds for all propositions. In constructive mathematics, the Law of Excluded Middle only holds for decidable propositions. If P is decidable, it is safe to constructively assume P or ~P because an algorithm can produce the answer.

My personal experience with WebGPU wasn't the best. One of my dislikes was pipelines, which is something that other people also discuss in this comment thread. Pipeline state objects are awkward to use without an extension like dynamic rendering. You get a combinatorial explosion of pipelines and usually end up storing them in a hash map.

In my opinion, pipelines state objects are a leaky abstraction that exposes the way that GPUs work: namely that some state changes may require some GPUs to recompile the shader, so all of the state should be bundled together. In my opinion, an API for the web should be concerned with abstractions from the point of view of the programmer designing the application: which state logically acts as a single unit, and which state may change frequently?

It seems that many modern APIs have gone with the pipeline abstraction; for example, SDL_GPU also has pipelines. I'm still not sure what the "best practices" are supposed to be for modern graphics programming regarding how to structure your program around pipelines.

I also wish that WebGPU had push constants, so that I do not have to use a bind group for certain data such as transformation matrices.

Because WebGPU is design-by-committee and must support the lowest common denominator hardware, I'm worried whether it will evolve too slowly to reflect whatever the best practices are in "modern" Vulkan. I hope that WebGPU could be a cross-platform API similar to Vulkan, but less verbose. However, it seems to me that by using WebGPU instead of Vulkan, you currently lose out on a lot of features. Since I'm still a beginner, I could have misconceptions that I hope other people will correct.

This types-are-propositions persoective is called the Curry-Howard correspondence, and it relates to constructive mathematics (wherein all proofs must provide an algorithm for finding a "witness" object satisfying the desired property).