Remix.run Logo
oisdk 6 hours ago

> For one, if algebraic isn't aiming at the ideas in an algebra, then they absolutely should be using a different name.

Algebraic effects are certainly algebraic, they're just not directly related to algebraic data types. Both ideas are using "algebraic" at different levels, and I think trying to understand algebraic effects by referencing algebraic data types will be more confusing than helpful.

> My point is that the "value" is not the written value of a variable in ways that people are used to working with in their program.

I'm saying that (in algebraic effects) the "value" in question is precisely a normal variable that people are used to working with in programming languages. It is not a type-level value, which is the kind of value in question when we're talking about algebraic data types.

For example, if we take Groups (the algebra referenced in the post), we have a binary operation (that we might call +) along with a few other operations. We could write a piece of code like the following:

    x = y + z
The "group" in question here could absolutely be an algebraic effect. And the line of code above could be implemented using algebraic effects, and interpreted using an algebraic effect handler. You don't even need types, if you didn't want them.

> For two, though, the whole idea is how to compose the "value" of different effects together?

No, not really.

Yes, algebraic effects compose well. But so do other effects systems and abstractions (applicatives, etc.). The fact that the effects compose is not what makes them algebraic, it's a consequence of it.

I don't think I can give a proper explanation in a comment, but I would point you to the paper I linked in another comment (https://arxiv.org/abs/1807.05923).

taeric 6 hours ago | parent [-]

I'm not positive on what you are aiming at. I'd assume "algebraic effects" are to talk about performing algebra on the effects. That is, you are specifically going to talk about how different things combine effects, preferably in ways that honor + and * that we are used to.

If you are just pointing out that this is not, necessarily, "type" related. Agreed. Apologies if I mislead there. I was highlighting that algebraic data types has a similar problem. I did not mean to imply that these were the same topic.

My point is simply that there is no value in the program that says an effect has or has not completed. This is why I compare it to stepping through the program. The "line of code" that is active in executing code is not a first class value in your program. It is very much there, of course. But it is not a value of the program.

oisdk 5 hours ago | parent [-]

> I'd assume "algebraic effects" are to talk about performing algebra on the effects. That is, you are specifically going to talk about how different things combine effects

This is a misconception. The "algebra" does not refer to an algebra of effects, or combining effects in any way.

It's more like it's the other way around: "algebraic effects" are effects generated from algebras. These algebras are precisely-defined mathematical objects (like groups, monoids, etc.), so you have an "effect" that corresponds to monoids, an "effect" that corresponds to groups, and so on.

> My point is simply that there is no value in the program that says an effect has or has not completed. This is why I compare it to stepping through the program. The "line of code" that is active in executing code is not a first class value in your program.

I know: I'm trying to say that the "algebra" of "algebraic effects" do refer to first-class values. The + and * from other algebraic operations are the algebraic operations you might use for an algebraic effect.

taeric 4 hours ago | parent [-]

I feel that you just spelled potato and then pronounced it differently. :D

If you have examples you recommend, I'd be game to look over them.

What is a first class "value" that is referenced in algebraic effects?

oisdk 4 hours ago | parent [-]

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 3 hours ago | parent [-]

Right, but this is just explaining algebra. Which, I get that. Connect this to effects, for me. (And fair that just because I assert that I get it, I would wager I don't have as strong of a handle as I should have.)

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 3 hours ago | parent [-]

For an algebra, you have some operations and some equations. The group algebra has the + operation, and 0 and -, and all the relevant equations.

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.

taeric 3 hours ago | parent [-]

I looked over the paper, but I confess I don't understand how it is helping. Would help a ton to have an example effect that didn't dive into distinguishing "Values", "Computations", "Value types," and "Computation types."

In fact, that it distinguishes values, computations, and the types of both seems more inline with my point? That what most "effect systems" are trying to capture are things that are not typically defined in programs?

So, again, give me some examples of effects and how you would model them. That will go a long way to demonstrate what you mean, here. Even better if you can show how this is already modeled in some code. (Note that I'm not trying to ask you to give this in a post. If you have some more things like that paper to look into, I don't mind looking there. I do plan on spending more time with the paper, already.)

oisdk 2 hours ago | parent [-]

Well, I gave the example of a logging effect above. In the post there’s also an example of a key-value store effect. What’s missing from these examples exactly?

All of these effects have simple operations (get and put for store, the `write` operation for the logging effect, etc.) These are all normal operations in your language: they just return values, like normal, and the laws that govern them are equivalent to the laws of any other algebra.

Elsewhere you mentioned Boolean algebra, and that people shouldn’t confuse that with algebraic effects: Boolean algebra can absolutely be another example of an algebraic effect! The operations are the Boolean operations (call them whatever you like, + or * or whatever), and the laws are the usual laws.

The point of algebraic effects is in noticing that traditional effects (logging, state, exceptions) can be thought of as algebraic the same way as Boolean algebras or monoids.

If you’re looking for an implementation, there are lots of implementations available in Haskell and other languages. However, to understand those you’d really already have to have a good understanding of the topic first, and then you’d also need to be comfortable with Haskell syntax (and probably free monads as well). I think that the paper really gives the best introduction to the topic, unfortunately there’s no way to simplify it much further.

taeric an hour ago | parent [-]

I don't think I mentioned boolean algebra? I responded to someone else mentioning it. My problem there is still that you are going to be taught how to operate over boolean values using an algebraic construction. (Looking, I think that is accurate. Apologies if I am the one that brought it up somewhere, I don't remember that.)

Which, fair that may help some people. I just feel that this is akin to asking for people to understand algebraic effects using basic algebra from middle school. In basic algebra practices, you lean heavily on the basic operations applied to reals and see how to manipulate equations to discover both solutions and other statements about the equations. (Advanced students will eventually extend to imaginary numbers, but I don't think that changes this statement?)

Similarly, with algebraic datatypes, you learn what it means to combine the domains of types together. Since it is an algebra, you learn this in terms of the basic operations. Hence SumTypes and ProductTypes. My assertion there is that this is hard for people because they don't actually do the algebra on the domains. And, by "they" I largely mean the software that they write.

So, with algebraic effects, I would expect that this is about the ways that effects can be combined using basic algebra tools. But what is it that you are combining? In the types, you were combining domains for analysis. In effects, I'd expect that you are combining whatever it is an effect is. You seem to be saying that an effect is a standard value? But, that seems at odds with the definitions that distinguish "pure" functions from those that have "effects" being defined by things that they cause to happen.

It doesn't help that we typically talk about things that we want to preserve some property on. It isn't enough to say "writes to stderr", we want to know that it does so without clobbering someone else currently writing to the same spot. At the least, we probably want to know that it line buffers output in such a way that that is preserved.

So, when asking for an example, I'm hunting for something to meet me somewhere in the middle. Sucks that this commonly comes down to "writes to a logger."