New blog post: An effect notation based on with-clauses

https://blog.yoshuawuyts.com/a-with-based-effect-notation

This is my third attempt at defining a notation for a full-fledged effect system in Rust. It's taken some influence from Flix, Koka, and Effekt. As well as including a little sprinkling of Python, Swift, and Scala.

With some luck people will hate this design less than the last time I had a go at this.

An effect notation based on with-clauses and blocks

@yosh That's looking more and more like what I hoped an eventual quantum programming language would like. There's two functions from impure functions impure functions that keep coming up in quantum programming; Q# named those "adjoint" and "controlled." They act a bit like macros as far as the compiler is concerned, but setting that aside, you'd often write something like `operation ApplyX is Adj + Ctl` to tell the compiler that a given operation should be made adjointable and controllable.

@yosh That then led to the problem where every stdlib *pure* function from impure functions to impure functions needed to be defined four times, for no transformations, for adjointability, for controllability, and for both.

I always wanted to be generic over that, and that effects notation is really close to what I was hoping we could land at.

@yosh (The main difference then being that adjoint and controlled aren't true effects, in that they don't imply the existence of monads that act on those effects, as in your create/propagate/consume table. For example, "adjoint" means "reverse the order of the instructions in this function and add adjoint to every subroutine call.")

@xgranade I mention it in the footnotes of the post, but effects don't neatly map to monads! At least not in the way that most people expect they do.

For example: "divergence" is a primitive effect and only means that you're allowed to loop indefinitely. The only reason why it exists is to inform the compiler of it. And the only reason it's an effect is because it makes it a lot easier to work with than if it were some special kind of annotation.

@yosh Ah, I missed that footnote, sorry!
@xgranade ohhh, if you have links to an example of that I'd love to see it!
@yosh I don't know how many links have survived docs.microsoft.com getting turned into learn.microsoft.com, that's all well after I was laid off. I don't know if the language is even still around...

@yosh The simplest example would be Bound/Bind. The bits needed to make sense of this example are that:

- subroutines defined as "function" are always pure, and cannot have any effects whatsoever other than panicking the entire process
- operations are the more general case and can support `is Adj`, `is Ctl`, or `is Adj + Ctl`
- the language at the time supported partial application but not lambdas
- by convention, functions are named as nouns or adjectives, operations as verbs

(con'd)

@yosh So if you want "apply this operation then that operation," you'd get something like

operation Bind<'T>(op1 : 'T => (), op2 : 'T => (), arg : 'T) => () { op1(arg); op2(arg); }

function Bound<'T>(op1 : 'T => (), op2 : 'T => ()) -> ('T => ()) { return Bind(op1, op2, _); }

But then you'd need to repeat that whole block for each effect combination, so you'd get shit like BindA or BoundCA.

@yosh Ah, two other notation things I forgot:

- ' means "generic type parameter," similar to ML-style languages
- thin arrows mean functions, thick arrows mean operations

@yosh Anyway, I always wanted to write Bound<'T, #f> to be generic over Adj and Ctl, so you could have something like `-> ('T => () is #f)`.

Sorry for the long sequence of replies!

@xgranade Thank you, this is very helpful!
@yosh I’m not going to comment on the content as it’s way way over my head but can we use effect instead of eff? It’s not much longer and, in my opinion, is clearer.
@miaouPlop I started with effect as the keyword, but after a while it just seemed too long. I suspect this might be an instance of Stroustrup's rule.
@yosh you’re probably right! Like I said, I know absolutely nothing about language design, it was just my feeling reading it.
@yosh Reminder of my Swift-based suggestion from last time: putting the effect syntax before the return arrow, because it's things that happen before the function returns. Possibly more palatable if you consider "returns a T" as an effect itself.

@jrose I should really try that out!

FWIW the reason why I put it last is so that it would feel like it has some parity with where-clauses. And also Rust doesn't support return ascriptions on inline blocks. But maybe we should!

@jrose

Oh I also just realized: parsing ambiguity!

@yosh Yeah, if you want to use fn syntax. I don't really consider that new, though, you also have the existing ambiguity of with gen(Foo) -> &dyn Bar + Baz (is Baz an effect or another trait of the return value?). Especially since the most common generators need neither a resume nor a final result.

@yosh For a while I've been thinking of what I'd like this to look like for integer overflow behavior, and have settled on something like

fn foo(x: i32) -> i32 where i32: wrapping { }

@ekuber @yosh if I write a function taking multiple i32s it should also be possible to write per-arg behavior no ? Not all i32s are created equal, though for the vast majority of functions they likely would share the same so having a default through the type would be a good default
@poliorcetics @yosh for per arg behavior you can just accept `Wrapping<i32>` already.
@ekuber @yosh I know but your example seems to indicate you want a different way to specify it ?
@poliorcetics @yosh right. We already have the granular version, I want a "scope global" option.
@poliorcetics @yosh this would also let you change the behavior of functions being called unless they also override the default behavior, so it'd be transitive. This would also make it easier to write a function that always has a specific math behavior, regardless of what the cargotoml says.