(no title)
oisdk
|
5 months ago
I mean, the program snippet that I gave above contains 3 first-class values. If you write `x = y + z + 0`, or any other statement that uses the group algebra (or any other algebra), you can use algebraic effects to describe the semantics. The “first-class values” here are the x, y, and z: there’s nothing fancy going on. You can even use the group laws to show that the statement is equivalent to `x = y + z` (or whatever). It’s just normal, value-level algebra.
taeric|5 months ago
My understanding for effects was more like "writes to stdout" and such. Probably better to have "opens a stream," "writes to an open stream," and "closes a stream." The algebra that I typically see is to show that you can combine some of these in such a way to either highlight a bug, or to help prevent them.
I got this because many effects typically go through hurdles to find a way to let you log to stderr without it polluting your entire effects system.
oisdk|5 months ago
You can also form an algebra from logging. One operation might be “write to stdout”. And then a law might be `write x; write y = write (x ++ y)` where ++ is string concatenation.
This is the algebra, the algebra isn’t for combining effects at all. (Yes, you can combine algebraic effects, and the fact that they’re algebraic does help, but that’s for technical reasons that aren’t relevant)
The paper I linked in another comment has a good overview of the topic. It’s really not the kind of thing you can understand from reading a few comments, and the paper is well-written and goes over all of the main points from a pretty basic starting point.