1) Agree, the issues with (checked) exceptions and error monads mostly stem from expressive limitations of a specific language than the model itself.
2) The next step up is making the exception continuation first class, then I don't think there is any difference. I think you can recover the efficiency of the simple non-local goto by optimizing after CPS transform, but I'm not a compiler writer.
3) As you point out, I think the continuation monad should be able to do resumable exceptions.
You mention algebraic effects, which are probably the right way to implement Error types/Exceptions/Resumable Error handlers.
- For the longest time, languages with typed (“checked”) exceptions lacked any parametric polymorphism worth a damn. That made the typing... less than optimally useful, especially with fallible callbacks. Sum types can borrow all that from the existing language, and you’d feel intensely awkward if you tried to go with untyped errors there (it’s of course still possible, through Dynamic or interface{} or whatever Rust’s thing is).
Though looking at the boilerplate fest that is the latest Rust (sum-types-based) error handling article posted here[1], I’m not entirely convinced the situation has improved. Perhaps open union types of some sort really are needed? That’s where the algebraic-effects languages seem to be going, anyway.
- Exceptions are more strict about what you can do with them: you can return or you can bind, monadically speaking. If an exception was raised, everything stops until it’s caught. With sum types (concrete ones, not an abstract error monad you can’t run), you are allowed to have several propagation chains at once and manipulate them as data. The lack of that additional flexibility is what makes exceptions (more cheaply?) implementable in terms of stack unwinding.
(Traditionally, stack unwinding is thought of as expensive, but I don’t really see why. Sure SJLJ-induced register spills are bad, and sure table-based unwinding is slow as hell, but a linked list of frames as in Win32 SEH[2] has to be cheaper than the same thing implemented as conditional jumps in every unwinding path, right? Right? I must be missing something here, expired Borland patent aside.)
- Concrete sum types cannot implement resumable exceptions[3], as far as I can tell. I’m almost sure an abstract error monad could, but for some reason I have never seen it done. Besides, working with that is going to require more syntactic support than what you’ve shown. (Yes, I know, such syntactic support is possible to implement and has in fact been implemented.)
[1] https://sabrinajewson.org/blog/errors, discussed at https://news.ycombinator.com/item?id=35502874
[2] http://bytepointer.com/resources/pietrek_crash_course_depths...
[3] https://gigamonkeys.com/book/beyond-exception-handling-condi...