Comment by tome
8 hours ago
> They're really just a protocol.
Thanks, that clarifies where you're coming from. Is it possible to specify this protocol somehow, by defining an interface for it? Or by extending lambda calculus with the bits it needs?
(Maybe that's what the Koka folks do in their papers, and if so feel free to say, "yeah read their papers").
I'm thinking a less formally than that. Protocol in a very layman-y "perform is supposed to do this, resume is supposed to do this".
For example, Koka compiles handlers differently depending if they do multi-shot continuations or not. It can do this because all that matters is "perform is supposed to do this, resume is supposed to do this", not what they turn into (same as "if" turning into "cmov" in certain cases). I think it uses a continuation-passing style sort of implementation, but I can't quite remember.
Daan's libhandler implements effects for C in an entirely different manner. It captures the stack much like my example or a stackful coroutine library would.
I'm sure there a formal definitions in both the koka papers and the libhandler paper, but I just skim that stuff ;)
> Protocol in a very layman-y "perform is supposed to do this, resume is supposed to do this".
OK, but at the very least it has two primitives "perform" and "resume"? And they're supposed to interact in some particular way?
Yeah, there's three things you're supposed to implement: try/handle, perform, and resume. The names can vary (e.g., perform is often called "raise" or "do"). They have well defined interactions.
I don't actually know what the original paper describing what algebraic effects are supposed to do is, I just know them informally from Koka, Effekt, etc.
1 reply →