4 ms·
There are two aspects to effects as a language feature- first there is the runtime behavior, and then there is the type system. Ruling out categories of effects
by Rusky 2y ago
There are two aspects to effects as a language feature- first there is the runtime behavior, and then there is the type system. Ruling out categories of effects is the job of the type system, and you don't have to commit to (or avoid) any particular runtime approach to use it that way.
This is related to the vagueness of your two categories. While exceptions, yields, and awaits don't really make sense without a handler, all that matters to the type system is which operations an expression might perform in addition to producing a result of their primary type. Handlers only interact with the type system in the sense that they remove an effect from their handle-ee expression.
So even in a language that committed to coroutines as its approach handling effects at runtime, the type system could still track and rule out effects like divergence or system calls. (For what it's worth, nondeterminism, state, etc. can all also be defined in terms of handlers. And at the same time, though, unsafety is not an effect because it is not entirely captured by "can this expression perform operation X.")