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.
@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 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
Cassandra is only carbon now