yosh3d ago

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

Show threadCassandra is only carbon now3d ago
@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.
Show threadCassandra is only carbon now3d ago

@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.

Show threadCassandra is only carbon now3d ago
@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.")
Show threadyosh

@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.

Mar 20 at 5:42pmWeb
Show threadCassandra is only carbon now3d ago
@yosh Ah, I missed that footnote, sorry!