4 ms·

What is algebraic about algebraic effects?

96 points by iamwil 1y ago

taeric 1y ago
I started a thread last time Algebraic Datatypes were discussed that hit a similar vein. I assert most programmers know the middle school version of "algebra" and think of it in terms of what they can do with the values they are working with. This is in contrast to doing operations on either the "types" or the "effects" that are happening during code. So, you have to show people what are the equivalent of + and * in types and effects to show them how these can be thought of algebraically. I still think this would be easier if a type system was made that let you use + and * in defining something. It would give an obvious path to seeing how things relate to algebra. Would almost certainly make some things harder, of course. Maybe it would be a good worksheet asking questions about stuff? The big underline, though, is getting people to realize what algebra there is is not on the values that your code represents. It is treating something else as the value for the algebra.
- andrewflnr 1y ago
  OCaml (and its relatives I think) use * for type products. It's a lot trickier with sum types though because the variant tags realistically have to show up in the syntax, and that's going to really stretch any syntax that tries to use +... I guess it would sort of work if you made Variant(foo, bar) types of things usable standalone types, but that's either a product without a * or another non-algebraic level between + and *.
  - taeric 1y ago
    Yeah, I think I agree? It did amuse me how quickly this got annoying from the existence of String and how people use it. :D That is, I think this is what you are saying? That it wouldn't be hard to show that an Optional<String> is the same as a variable that is (String + None) or some such. But having Either<String, String> kills this, since there is no way to distinguish the left and right String types, there. Now, if you forced it to be Either<ErrorString, ResponseString>, that can work. And that nicely explains why you have to tag the types to be distinguishable from each other.
  - rixed 1y ago
    It's not +, but it's |, like OR which is the + of logical operators.
    - andrewflnr 1y ago
      Type sum is more like XOR though, in that it excludes overlap. I think of | for types as a set-like union type, with overlap allowed. At least that's how Typescript uses that operator (which makes sense for modeling JS APIs, but does not bring the joy of algebraic sums).
- daxfohl 1y ago
  It'd be good to start with a preamble "what is algebraic about boolean algebra" since most coders should be familiar with the concept. That helps clarify what is even meant by the term "algebra" in abstract contexts. Then you could show how these things relate to ADTs and effects.
  - taeric 1y ago
    The problem with this is still that you are sticking with the algebra over the boolean values. And you are going to use + and * in doing so. Then, you are going to move to discussing the algebra over types and effects. In such a way that you don't actually use + or * to represent the operations.
    - Quekid5 1y ago
      I'm not if sure if this is what you're asking for, but to make it very explicit, e.g. Console Output might be modeled as data ConsoleOutput = PrintLn String | PrintWithMode (Mode * String) | ... where | is another spelling of + (which is pretty standard if you look at boolean algebra) and the product is the usual tuple constructor. The is a simple algebraic data type which defines 'an effect' ... it doesn't define the semantics (that's defined by a handler), but it's an 'api' for an effect of some sort. Obviously, the above definition is a bit contrived, but that's my understanding of why these things are called 'algebraic' effects. It's not that ConsoleOutput and ConsoleInput (however you define that using + or *) are magically 'composable' just because they're both algebraic... for that composition you need extra rules (however you specify that) because effects don't (in general) compose.
      - oisdk 1y ago
        > that's my understanding of why these things are called 'algebraic' effects. This is a misconception. Algebraic effects are not algebraic because they come from algebraic data types, the two features are completely independent (you can have algebraic effects without algebraic data types and vice versa). > It's not that ConsoleOutput and ConsoleInput (however you define that using + or *) are magically 'composable' just because they're both algebraic... for that composition you need extra rules (however you specify that) because effects don't (in general) compose. Actually, if you have two algebraic effects they can automatically compose. And this is a consequence of them both being algebraic. It's just that an algebraic effect is unrelated to an algebraic data type.
- oisdk 1y ago
  The "algebraic" in "algebraic effects" is not really related to algebraic data types, or sum or product types. I mean, I suppose they're related, since they both refer to algebra in the general sense, but there's no type-level algebra in a description of algebraic effects. (and, I suppose, you could do some type-level algebra with effects, like taking the "sum" of two effects, but again that's not what the "algebra" in "algebraic effects" is referring to) > The big underline, though, is getting people to realize what algebra there is is not on the values that your code represents. This is not correct. In the case of algebraic effects, the algebra is absolutely value-level.
  - taeric 1y ago
    I'm not sure I follow? For one, if algebraic isn't aiming at the ideas in an algebra, then they absolutely should be using a different name. For two, though, the whole idea is how to compose the "value" of different effects together? 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. It will be a meta-value about some state represented by the program. Is that not the case? If my use of the word "value" there is confusing things, I'm open to using some other words. My point is largely that the "value" of concern in effect systems is not the same as the value of a variable as people are used to reasoning. You are specifically meta-reasoning about the state of the program in ways that may not be represented by an explicit value of the program. Not that that alone is unheard of. If you asked people to tell you the program counter of a function, they would largely get what you mean. Even if it is not something that is represented in the values of the program, itself.
    - oisdk 1y 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 https://arxiv.org/abs/1807.05923).
- zdragnar 1y ago
  I have this mental block that keeps me forgetting which is which when discussing sum and product types. I have to go back to thinking of them as operations on sets. Almost certainly a lack of formal education in maths higher level than simple calculus, but "unions" and "interface" or whatever the latter might be called in the language of choice is just so much easier to remember.
  - nutjob2 1y ago
    It's usually described as tagged unions and records, and the easy way to remember it by thinking about how many different values they can contain. Given that each type represents some number of possible values, the number of values for the unions is the sum of values for each allowable type and for records its the product of each field type.
  - ndriscoll 1y ago
    * is and, + is or. This agrees with Boolean algebra, so you can think in terms of a single bit. If you can also remember that functions A->B are exponentials B^A, then you can do a quick check that everything lines up: C^(A+B) = C^A*C^B. A function that handles A or B is the same as a function that handles A and a function that handles B.
- dleeftink 1y ago
  The Algebra of Graphics package for Julia[0] has a interesting ('tangible') use-case for algebraic operators here. [0]: https://aog.makie.org/stable/#Example https://aog.makie.org/stable/#Example
oisdk 1y ago
I would encourage anyone interested in this question to check out the paper "What is algebraic about algebraic effects and handlers?" (https://arxiv.org/abs/1807.05923 https://arxiv.org/abs/1807.05923) which is a write-up of the lecture series linked in the post above. I don't think the paper is too difficult to understand, but I know that if you're not familiar with the subject area it might be intimidating. While I like the above blog post, I don't think that it will be very useful to people trying to understand algebraic effects. I see a lot of explainers like this one that shy away from some of the more gnarly-looking maths terms in an effort to appear more approachable, but as a result they can end up giving imprecise or vague definitions. When coupled with some subtle mistakes I think it can leave beginners more confused than helped (for instance, this author seems to conflate a few different notions of "composition", and they seem to think that the presence of equations makes an effect algebraic, which isn't really what the term "algebraic" is referring to in a technical sense). The paper I linked above is not easy, and it would probably take at least a few hours to understand, but that's because it takes about that long to understand the material.
- sestep 1y ago
  Just to clarify, are you saying that you recommend that writeup over the lecture, or just linking the writeup for people who'd prefer it over watching a video?
  - oisdk 1y ago
    I'm just recommending the writeup, but only because I haven't watched the lecture series myself (although I'm sure it's good, I've seen other lectures by the lecturer that were excellent). As far as I know, they cover basically the same material.
- iamwil 1y ago
  > they seem to think that the presence of equations makes an effect algebraic, which isn't really what the term "algebraic" is referring to in a technical sense Author here! Open to learning. Can you expand on this? What is algebraic referring to in a technical sense?
shiandow 1y ago
That is interesting, I hadn't really given it much thought but my first instinct would be to assume the algebra in algebraic effect was not about having algebra like definitions but was in fact a direct reference to an algebra of a monad (though that might be the same thing). At least the monad algeba gives a nice hint on how to view algbraic effects. Instead of using a monad so you can raise an exception f :: a -> E b You use an E-algebra (h :: E a -> a) instead to create a function that takes both an input and an exception handler to produce an output g :: (a, E b -> b) -> b The canonical example being something like g x h = h (f x) And a simple example of a handler being something like a default value h :: Maybe a -> a h Some x = x h None = default_value With the advantage of course that given a handler you can be much more flexible in how you handle exceptions and where. You're not limited to just returning early, you can handle the exception and carry on.
aap_ 1y ago
That was a very approachable explanation. Makes a lot of sense. Essentially by encoding the program algebraically you can prove that it is invariant under the action of the semi-lattice. Very neat! Maybe lean is worth a look.
deleted 1y ago
[deleted]

96 points by iamwil 1y ago

I started a thread last time Algebraic Datatypes were discussed that hit a similar vein. I assert most programmers know the middle school version of "algebra" and think of it in terms of what they can do with the values they are working with. This is in contrast to doing operations on either the "types" or the "effects" that are happening during code. So, you have to show people what are the equivalent of + and * in types and effects to show them how these can be thought of algebraically. I still think this would be easier if a type system was made that let you use + and * in defining something. It would give an obvious path to seeing how things relate to algebra. Would almost certainly make some things harder, of course. Maybe it would be a good worksheet asking questions about stuff? The big underline, though, is getting people to realize what algebra there is is not on the values that your code represents. It is treating something else as the value for the algebra.

andrewflnr 1y ago
OCaml (and its relatives I think) use * for type products. It's a lot trickier with sum types though because the variant tags realistically have to show up in the syntax, and that's going to really stretch any syntax that tries to use +... I guess it would sort of work if you made Variant(foo, bar) types of things usable standalone types, but that's either a product without a * or another non-algebraic level between + and *.
- taeric 1y ago
  Yeah, I think I agree? It did amuse me how quickly this got annoying from the existence of String and how people use it. :D That is, I think this is what you are saying? That it wouldn't be hard to show that an Optional<String> is the same as a variable that is (String + None) or some such. But having Either<String, String> kills this, since there is no way to distinguish the left and right String types, there. Now, if you forced it to be Either<ErrorString, ResponseString>, that can work. And that nicely explains why you have to tag the types to be distinguishable from each other.
- rixed 1y ago
  It's not +, but it's |, like OR which is the + of logical operators.
  - andrewflnr 1y ago
    Type sum is more like XOR though, in that it excludes overlap. I think of | for types as a set-like union type, with overlap allowed. At least that's how Typescript uses that operator (which makes sense for modeling JS APIs, but does not bring the joy of algebraic sums).
daxfohl 1y ago
It'd be good to start with a preamble "what is algebraic about boolean algebra" since most coders should be familiar with the concept. That helps clarify what is even meant by the term "algebra" in abstract contexts. Then you could show how these things relate to ADTs and effects.
- taeric 1y ago
  The problem with this is still that you are sticking with the algebra over the boolean values. And you are going to use + and * in doing so. Then, you are going to move to discussing the algebra over types and effects. In such a way that you don't actually use + or * to represent the operations.
  - Quekid5 1y ago
    I'm not if sure if this is what you're asking for, but to make it very explicit, e.g. Console Output might be modeled as data ConsoleOutput = PrintLn String | PrintWithMode (Mode * String) | ... where | is another spelling of + (which is pretty standard if you look at boolean algebra) and the product is the usual tuple constructor. The is a simple algebraic data type which defines 'an effect' ... it doesn't define the semantics (that's defined by a handler), but it's an 'api' for an effect of some sort. Obviously, the above definition is a bit contrived, but that's my understanding of why these things are called 'algebraic' effects. It's not that ConsoleOutput and ConsoleInput (however you define that using + or *) are magically 'composable' just because they're both algebraic... for that composition you need extra rules (however you specify that) because effects don't (in general) compose.
    - oisdk 1y ago
      > that's my understanding of why these things are called 'algebraic' effects. This is a misconception. Algebraic effects are not algebraic because they come from algebraic data types, the two features are completely independent (you can have algebraic effects without algebraic data types and vice versa). > It's not that ConsoleOutput and ConsoleInput (however you define that using + or *) are magically 'composable' just because they're both algebraic... for that composition you need extra rules (however you specify that) because effects don't (in general) compose. Actually, if you have two algebraic effects they can automatically compose. And this is a consequence of them both being algebraic. It's just that an algebraic effect is unrelated to an algebraic data type.
oisdk 1y ago
The "algebraic" in "algebraic effects" is not really related to algebraic data types, or sum or product types. I mean, I suppose they're related, since they both refer to algebra in the general sense, but there's no type-level algebra in a description of algebraic effects. (and, I suppose, you could do some type-level algebra with effects, like taking the "sum" of two effects, but again that's not what the "algebra" in "algebraic effects" is referring to) > The big underline, though, is getting people to realize what algebra there is is not on the values that your code represents. This is not correct. In the case of algebraic effects, the algebra is absolutely value-level.
- taeric 1y ago
  I'm not sure I follow? For one, if algebraic isn't aiming at the ideas in an algebra, then they absolutely should be using a different name. For two, though, the whole idea is how to compose the "value" of different effects together? 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. It will be a meta-value about some state represented by the program. Is that not the case? If my use of the word "value" there is confusing things, I'm open to using some other words. My point is largely that the "value" of concern in effect systems is not the same as the value of a variable as people are used to reasoning. You are specifically meta-reasoning about the state of the program in ways that may not be represented by an explicit value of the program. Not that that alone is unheard of. If you asked people to tell you the program counter of a function, they would largely get what you mean. Even if it is not something that is represented in the values of the program, itself.
  - oisdk 1y 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 https://arxiv.org/abs/1807.05923).
zdragnar 1y ago
I have this mental block that keeps me forgetting which is which when discussing sum and product types. I have to go back to thinking of them as operations on sets. Almost certainly a lack of formal education in maths higher level than simple calculus, but "unions" and "interface" or whatever the latter might be called in the language of choice is just so much easier to remember.
- nutjob2 1y ago
  It's usually described as tagged unions and records, and the easy way to remember it by thinking about how many different values they can contain. Given that each type represents some number of possible values, the number of values for the unions is the sum of values for each allowable type and for records its the product of each field type.
- ndriscoll 1y ago
  * is and, + is or. This agrees with Boolean algebra, so you can think in terms of a single bit. If you can also remember that functions A->B are exponentials B^A, then you can do a quick check that everything lines up: C^(A+B) = C^A*C^B. A function that handles A or B is the same as a function that handles A and a function that handles B.
dleeftink 1y ago
The Algebra of Graphics package for Julia[0] has a interesting ('tangible') use-case for algebraic operators here. [0]: https://aog.makie.org/stable/#Example https://aog.makie.org/stable/#Example

oisdk 1y ago

I would encourage anyone interested in this question to check out the paper "What is algebraic about algebraic effects and handlers?" (https://arxiv.org/abs/1807.05923 https://arxiv.org/abs/1807.05923) which is a write-up of the lecture series linked in the post above. I don't think the paper is too difficult to understand, but I know that if you're not familiar with the subject area it might be intimidating. While I like the above blog post, I don't think that it will be very useful to people trying to understand algebraic effects. I see a lot of explainers like this one that shy away from some of the more gnarly-looking maths terms in an effort to appear more approachable, but as a result they can end up giving imprecise or vague definitions. When coupled with some subtle mistakes I think it can leave beginners more confused than helped (for instance, this author seems to conflate a few different notions of "composition", and they seem to think that the presence of equations makes an effect algebraic, which isn't really what the term "algebraic" is referring to in a technical sense). The paper I linked above is not easy, and it would probably take at least a few hours to understand, but that's because it takes about that long to understand the material.

sestep 1y ago
Just to clarify, are you saying that you recommend that writeup over the lecture, or just linking the writeup for people who'd prefer it over watching a video?
- oisdk 1y ago
  I'm just recommending the writeup, but only because I haven't watched the lecture series myself (although I'm sure it's good, I've seen other lectures by the lecturer that were excellent). As far as I know, they cover basically the same material.
iamwil 1y ago
> they seem to think that the presence of equations makes an effect algebraic, which isn't really what the term "algebraic" is referring to in a technical sense Author here! Open to learning. Can you expand on this? What is algebraic referring to in a technical sense?

shiandow 1y ago

That is interesting, I hadn't really given it much thought but my first instinct would be to assume the algebra in algebraic effect was not about having algebra like definitions but was in fact a direct reference to an algebra of a monad (though that might be the same thing). At least the monad algeba gives a nice hint on how to view algbraic effects. Instead of using a monad so you can raise an exception f :: a -> E b You use an E-algebra (h :: E a -> a) instead to create a function that takes both an input and an exception handler to produce an output g :: (a, E b -> b) -> b The canonical example being something like g x h = h (f x) And a simple example of a handler being something like a default value h :: Maybe a -> a h Some x = x h None = default_value With the advantage of course that given a handler you can be much more flexible in how you handle exceptions and where. You're not limited to just returning early, you can handle the exception and carry on.

aap_ 1y ago

That was a very approachable explanation. Makes a lot of sense. Essentially by encoding the program algebraically you can prove that it is invariant under the action of the semi-lattice. Very neat! Maybe lean is worth a look.

deleted 1y ago

[deleted]