[johncolanduoni]

What you're describing as far as lifting is not unlike algebraic effects, like Eff[1] and Idris[2] have. Basically, you can have some sort of "exception" effect, except limited to particular type of error, and this system will mix them without having to use monad transformers. This particular application is not too dissimilar to checked exceptions, but the algebraic effect approach gives you a lot more power. It also makes it easy to deal with pure vs. impure functions, IO, etc. seamlessly.

Responding to internal errors differently based on the caller's desire is possible with Lisp; there's a good overview here[3]. It looks like algebraic effects can do something similar, as described in this paper[4] (search for lisp and the relevant portion should show up).

[1]: http://math.andrej.com/eff/

[2]: http://www.idris-lang.org/

[3]: http://www.gigamonkeys.com/book/beyond-exception-handling-co...

[4]: https://hal.archives-ouvertes.fr/hal-01079206/file/effects-p...

[dom96]

Another language worth looking into if you're interested in effect systems is Nim. It includes an effect system that deals with both exceptions and other effects (like for example IO read/write effects): http://nim-lang.org/docs/manual.html#effect-system-exception.... The exception tracking is similar to a checked exception system but is far less annoying than Java's. In my opinion it is the best way to ensure exceptions are handled.