Is the author mixing up “effect systems” with “algebraic effects”?

My understanding is that “algebraic effects” are the dynamic feature, almost like resumable exceptions, while “effect systems” are the static feature where side effects are checked in the type system.

The linked post about React is talking about algebraic effects, not an effect system.

On the other hand I’d say Java has an effect system (checked exceptions!) but not really algebraic effects.

The author wants to look up “type variance”. They will find that effects are intuitively contravariant, just like functions.

For those unfamiliar with the terminology, here two examples:

Lists are covariant. A list of apples is a list of fruits. When you are supposed to provide a list of fruits you can provide a list of apples.

Functions (and also effects) are contravariant. A function that works with any fruit as input will work with an apple as input (mind the reversed logic compared to lists). Hence, when you are supposed to provide a function that works with an apple, you can provide a function that works with any fruit.

The same applies to effects and their combinations.

This is very cool but it is odd to me that I/O reading is not considered an effect. For one, it’s not idempotent and also you have no idea what reading the file could do. You could be reading off a FUSE filesystem that makes a network request or something.

Okay, this comment is pretty long, but I’ve been thinking about something similar to this for a few months now. I think something in this design space could provide a lot of the control that pure functional languages provide, but with less overhead (runtime, compile time, and mental).

Background

Monads encode effects, but they also encode the sequencing of those effects. They do this by reifying the effects as data structures and wrapping the values they are tracking. The runtime is able to interpret those effects and execute them. This allows the language to perform fine grained tracking over the effects and enable optimizations that might not be possible if there were fewer guarantees. This also gives the programmer confidence that if the effect isn’t part of the type system then it isn’t possible (modulo unsafe functions).

However, this means that there is a lot of wrapping and unwrapping of values, which has compile time costs, runtime costs, and general mental overhead costs. The effects are also not as composable because of the sequencing. E.g., a maybe io is not the same thing as io maybe.

Idea

If you weakened the monad by removing the sequencing property, I think you would get something like a set. Tracking effects in a set based manner would give you less information/power, but more composability. You could also take advantage of set based operations to restrict the effects that your children are allowed to call. For example, if we extend the syntax from the article with a block that explicitly chooses the effects that it’s contents have access to we could get something like this:

pub fn main() -> [io, network] {
  with io {
    println("Hello, world!");  
  }
}

Or maybe we want a block that excludes certain effects like this:

pub fn main() -> [io, network] {
  without network {
    println("Hello, world!");  
  }
}

This would give the programmer the power to project guarantees down the stack without polluting the value space.

If you moved the values out of the runtime and into a parallel set based type system like the article suggests, then you could unwrap the values and thin out the language runtime. Since the values are simpler, the compiler would need to do less work to optimize the code and the optimizations would probably be less fragile. Since you don’t need the runtime to interpret the effects, you can just perform them, which might be faster. Additionally, FFI would probably be simpler with a thinner runtime allowing easier access to established ecosystems.

Differences from the Article

The article notes that these annotations could be a lot of work and I agree. However, I disagree on the solution: I think that effects should be inferred/unspecified by default. Obviously, there are exceptions to this:

1. The public API of a library
2. Areas of a code base that need effects specified for logic and/or correctness reasons

The second exception is a bit vague so let me elaborate with a few examples:

• A web service probably doesn’t need to specify all of its effects.
• A one off script/command line app probably doesn’t need this level of rigor either.
• A build system might need to specify the allowed effects in some areas to prevent different kinds of attacks.
• An embedded DSL might need to specify the allowed effects to prevent arbitrary code from being executed.

So the more you are in the end user realm, the less you need to define the effects. However, you can still benefit from the tracking: the compiler can probably put all of the effects in the docs so people can learn more about the application.

I have more thoughts on how this compares to effect systems, the article, specific properties I would like to see, and more, but I don’t want to find out what the comment length limit on lobste.rs is.

Is this similar to Koka’s effect system?.

Just imagine how intricate optimization algorithms could get with knowledge of effects like this!

One effect that people don’t talk about often is potential non-termination. I’d imagine knowing that a function always terminates could be useful for optimising.

Speaking of going beyong type systems, why stop at effects? You could have the type system statically check that your function runs in polynomial time (see Linear Types and Non-Size-Increasing Polynomial Time Computation by Martin Hofmann (1999)).

Flix [1] looks like, based on my understanding of both, it has what the author describes as a static effect system. It doesn’t look like it has a dynamic one outside of Java interop [2].

[1] https://doc.flix.dev/effects.html [2] https://doc.flix.dev/exceptions.html

The author is correct that effects can be made separable from types, provided you are careful to restrict inference such that types may inform effects but never vice-versa, even in the presence of complex type system features like typeclasses/traits and type projection. I’ve implemented this in my own language. Like Rust lifetimes, their inference can be left to a later pass and doing so does simplify the design of the type solver somewhat. However, like lifetimes, they are still statically inferred terms and, as such, I still like to think of them as ‘part of the type system’.

I think a better approach is reified capabilities combined with linear types. To make this ergonomic/practical, though, you also would want borrow checking and implicity-passed contexts, and likely context requirement inference.

All of this combined would allow typical imperitive code, but with statically inferred “effects” like “does IO”, “reads from a global”, “writes to a global”, all of which would be reified into types/traits, which means the language doesn’t need to know the possible “effects” when the language is designed, they can be defined in a host platform layer (a la Roc) or “unsafe” super-language (a la Rust).

This also means you could refine capabilities arbitrarily, i.e. “reads from this particular global memory within this lifetime bound”.

This wouldn’t really address function totality checking, though, unless you prevented any operations that could lead to an infinite loop by default and required a capability for things that could loop. So you would still need a separate totality checker, although it could be integrated into this system as another capability.