Earlier quoted context omitted.
> Near the end of the article: >> Because algebraic effects are coming from statically typed languages, Though in fact the origins come from dynamically typed languages like Lisp, where condition signalling systems were developed in the 1970s. When they started appearing in statically typed languages in the late 80s, they were only used for errors, and by the time they were caught the stack had already been unwound.…
Sure but I mean most work on algebraic effects (or at least the papers I know of) deals with the associated type system . Instead most people here seem to focus on the semantics, which indeed boil down to call/cc + handlers or previous condition systems.
The curry-howard equivalence is only as useful as the strength of the type system. We ideally want proof irrelevance, that is, any program satisfying the types is sufficient, but while some things remain outside the type system this is only true up to a point (think: time and space costs). Putting effects into types helps this along.