Please consider this article on effects gone wrong

[safinaskar]

Hi. It seems you are implementing effect system for Rust. Great idea. Please, read this beautiful @lexi-lambda's article on what happens when effects implementations diverge:

https://twitter.com/lexi_lambda/status/1627720785736466434
https://github.com/lexi-lambda/eff/blob/8c4df4bf54faf22456354be18095b14825be5e85/notes/semantics-zoo.md

[Nadrieril]

For those not familiar with Haskell, here's what I understand from the linked article. The main point of background is that when a piece of code mixes multiple effects, what should happen depends on more than just the individual effects; one must often specify how they interact.

For example, when a piece of code both modifies state and uses a try/catch mechanism, one option is that when we catch an error we revert the state to what it was before the try. This is what parsers do for example. Another option is to not revert the state. That's what happens in rust when we do errors with Result and mutate state with &mut references.

The main point of the article is that the various Haskell effect libraries make different choices for these interactions. It's mostly not a bug since various choices can make sense for different contexts.

@safinaskar does that sound like a fair summary? I don't really see how that's relevant to the keyword-generics initiative right now; the initiative is pretty far from including enough genericity over effects to have to worry about that sort of thing

[yoshuawuyts]

The main point of background is that when a piece of code mixes multiple effects, what should happen depends on more than just the individual effects; one must often specify how they interact.

I'll have to give the article a more thorough read when I have some time. But going by this summary, it seems that what this article covers are the challenges of effect composition in a language with a generalized effect system (such as eff?).

We're intentionally not planning to create a generalized effect system through the keyword-generics-initiative. Instead, it's only scoped to the language's built-in modifier keywords. And those are a constrained set with clear composition semantics. Take for example the following:

// in today's syntax
async fn foo<E: Error>(..) -> Result<(), E> { .. }

// or if we had some sort of `throws` keyword
async fn foo(..) throws { .. }

We know that the return type of this function will always be -> impl Future<Result<..>>. And never: -> Result<impl Future, ..>. Those are the pre-defined composition rules at work, bypassing any composition problems. (Aside: Haskell's Monad abstraction also famously has challenges around composition. The solution there appears to be to use monadic transformer operations).

user-defined effects

But: being able to define effects by users is still a really useful thing to be able to do! But instead of putting it behind the same language feature as keyword generics, we believe there may be a better answer for that: contexts/capabilities. The paper "Capabilities: Effects for Free" ¹ goes into more detail how "effects" can be modeled as capabilities, and I believe even covers capability-safety. The way this basically would work is that "capabilities" would end up being a special kind of argument functions can take.

This wouldn't quite cover some of the control-flow things that a full fledged effect system can implement - but we also don't know how we would make that work with the borrow checker. We do know how that would work for capabilities and for keyword-generics, and when put together should give you enough to do most of what a generalized effect system can.

Thanks for your suggestion, and I hope this provides some more insight into our thinking here!

Footnotes

1. A. Craig, A. Potanin, L. Groves, and J. Aldrich, “Capabilities: Effects for Free,” in Formal Methods and Software Engineering, vol. 11232, J. Sun and M. Sun, Eds. Cham: Springer International Publishing, 2018, pp. 231–247. doi: 10.1007/978-3-030-02450-5_14. ↩

[lexi-lambda]

As the author of the linked document, I agree that it seems utterly unrelated.

[yoshuawuyts]

I think we can probably close this then?