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.
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) 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.
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.
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.
5 comments
[ 0.27 ms ] story [ 24.4 ms ] threadThis 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.
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.
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
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 The canonical example being something like And a simple example of a handler being something like a 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.