This is a little off topic because I’m not asking about OCaml specifically, but I did start thinking about this while watching talks about implementing typed effects in OCaml.
One of the questions that came up was, why not use monads instead of effect handlers?
The answer was that jumping through the stack after the pattern of exceptions was much cheaper than mondadic binding.
A little later, someone asked if mutation in OCaml could be completely replaced with the effect handlers. The answer was that it’s much cheaper to just write a couple bytes than to invoke an effect handler, but that basic mutation could still be represented in the type system as an effect.
This got me to thinking: If I were to create a programming language with typed effects, would it be possible to create errors with an interface similar to the Result monad, but implemented in terms of simple stack jumps?
When I think about it, it seems very possible. I’m just wondering if anyone sees any reasons why it wouldn’t work, or perhaps some additional layers of complexity that I haven’t considered. Seems similar to checked exceptions, in theory.
And also effects handlers compose unlike monads, and monadic style is annoying.
If I were to create a programming language with typed effects, would it be possible to create errors with an interface similar to the Result monad, but implemented in terms of simple stack jumps?
What interface exactly?
But not really, I think. Where would you jump? Effect handlers are clear delimiters, and you jump to the closest handler on the stack. They are more structured in a way. The result monad is different, it’s more like an ambient context with error bubbling (for lack of a better explanation).
Let’s say we have an expression e : t result.
We can write f e. The function f is free, it may or may not “handle” the result in e.
Let’s say we have an effectful expression e : t / err.
We write f e. The potential error in e cannot be handled here, there is no handler. It would have to be installed explicitly.
Now, the Frank language has functions that act as handlers, and you could write f e where f can handle the err in e. But it’s really implicitly installing handlers (for the effects the function declared to handle) at each application. So maybe Frank is what you were looking for.
The kind of interface where the call that triggers the exception is explicitly marked even if it’s not handled, perhaps a bit like the ? operator in Rust.
To wherever the error was unwrapped.
I think the only real difference between this and exceptions in my mind is:
the error is part of the type signature
the calls that potentially trigger the error are marked at the call site.
One possible benefit of this approach is that perhaps errors could be polymorphic, which is difficult with monads but works well with exceptions—although it’s a two-edged sword. This kind of polymorphism tends to make types much uglier. (like, e.g. polymorphic variants can get)
The unwrapping happens after the error. You can’t determine if some part of the continuation (that may involve arbitrary indirect function calls etc.) will unwrap or not.
The type system will ensure that every error is eventually unwrapped, since the error will be part of function types that generate errors. I’m quite sure this can be determined with static analysis.
If the compiler can’t determine where the error is handled, the program doesn’t compile. The Java compiler does this e’ry day.
edit: The more I consider it, the more I think this is really just a variation on checked exceptions
let f x =
if rand() < 0.5
then match x with Some x -> Some (x+1) | None -> None
then x
f (... raise ...)
Does raise magically “jump” to the match? Or half of the time? Or we always jump to f, since it’s potentially handling, an we’re back to Frank, which I mentioned at the beginning.
I guess functions which don’t raise would in some sense be polymorphic over their inputs with regard to errors. I guess then the program should jump back in the stack to the caller of f, convert the value to true monadic value and pass it into f.
Something like that.
I can see how this might complicate certain aspects of language implementation. Thanks for this helpful line of questioning.
It’s been a long time since I knew this stuff, but:
0. let’s set aside imperative features like mutating update (“:=”)
you can take a language with control flow and exceptions and convert it to pure lambda-calculus using a CPS transformation with two continuations: the “normal continuation” and the “exception continuation”
separately, IIUC computational effects are a version of shift/reduce, which can be coded in Scheme using callcc and a single mutable cell. This can then be converted back into Scheme with two CPS transformations. The Danvy&Filinski shift/reset paper (from 1991?) lays all this out.
