3 ms·

To expand on the “classifying Lawvere theories“ part, the relevant concept here is algebras over a monad. An algebra a over m is determined by a function merge

by yccs27 4y ago

To expand on the “classifying Lawvere theories“ part, the relevant concept here is algebras over a monad. An algebra a over m is determined by a function merge :: m a -> a which “plays nice“ with the monad structure [0]. For example, integers with the sum function form an algebra over the list monad, because 1) for any list of ints, the sum is an int 2) the sum of [n] is just n 3) summing recursively is the same as summing over the flattened list. More generally, the algebras over the List monad are exactly the monoids, with ‘merge [a, b]‘ as the monoid operation. Algebras over the Maybe monad are pointed sets, with ‘merge Nothing‘ as the distinguished point. A lot of algebraic structures (Lawvere theories) can be defined by a monad this way. [0] Laws that ‘merge‘ should satisfy: merge (return x) == x fmap merge (merge mx) == merge (join mx)

spion 4y ago
I don't understand how this is related to monads - there is nothing in the general monad interface that even allows you to go `m a -> a`, so something being a monad doesn't seem sufficient to be able to define that algebra. Seems to me that the entire interesting bit is "provided" by `a` being a monoid. (I agree that monoids are really interesting)
- hither_shores 4y ago
  > there is nothing in the general monad interface that even allows you to go `m a -> a`, so something being a monad doesn't seem sufficient to be able to define that algebra. You've got the direction backwards: the point is to characterize all `m`-algebras, not to construct particular ones. This is closely related to the usual duality between types and values. It's very common for people new to TypeScript, for instance, to think that `{a: string} | {b: number}` should be `{a: string, b: number}`, because they're thinking primarily in terms of records as sets of fields, not types as sets of values. But making the type bigger makes the set of things you can say about its values (i.e. the space of functions out of it) smaller. Algebras are similarly the "value-like" counterparts to "space-like" monads.
  - spion 4y ago
    I have no idea what you mean.
- kmill 4y ago
  Here's another way to say the general idea, by way of example. Secretly, list is "the" exemplary universal monoid. Given any `a`, then `list a` gives you the free monoid generated by `a`, with composition given by `++` and the identity given by `[]`. Now, let's say you have some `a` such that you're able to come up with a function `ev : list a -> a` that's a monad algebra (i.e., it satisfies the two axioms given by yccs27). Then you're able to conclude that `a` is a monoid(!) and you can extract the monoid structure in the following way: `\ (x y : a) -> ev [x, y]` is the binary operation and `ev []` is the unit. (In particular, `ev` must be some `list.fold`.) I called it `ev` because it's an evaluator/interpreter. To be able to write such a `m a -> a` function, `a` needs to have the same kind of structure that `m` is somehow representing, and you need to be able to map the operation that `m` "contains" to corresponding operations for `a`. This is that business about free monads being useful for organizing how you write interpreters I believe.
  - spion 4y ago
    > Then you're able to conclude that `a` is a monoid Yep, which is why I'm saying all the interesting bits come from `a` being the monoid in that example. In the free monad interpreter example, I have no idea though.
    - kmill 4y ago
      If there's a point to any of this, I think it's monads let you package up some algebraic structure in the form of a function `m a -> a` that satisfies certain properties, and then you can pass such a function around without any reference to the fact that `a` implements that algebraic structure. This function is the interface. (Is there real practical significance? I'm not sure, but I'm not trying to argue that :-) ) > all the interesting bits come from `a` being the monoid in that example. Yeah, there's nothing deep there. I just said what I said to underscore that the converse is true, that if anyone were to hand you such a `list a -> a` function then it's encoding some monoid structure on `a` (one of often very many).
- yccs27 4y ago
  The important point is that each monad (e.g. list) corresponds to an algebraic structure (like monoid). To study the set of algebraic structures, you can also study monads

by yccs27 4y ago

spion 4y ago

I don't understand how this is related to monads - there is nothing in the general monad interface that even allows you to go `m a -> a`, so something being a monad doesn't seem sufficient to be able to define that algebra. Seems to me that the entire interesting bit is "provided" by `a` being a monoid. (I agree that monoids are really interesting)

hither_shores 4y ago
> there is nothing in the general monad interface that even allows you to go `m a -> a`, so something being a monad doesn't seem sufficient to be able to define that algebra. You've got the direction backwards: the point is to characterize all `m`-algebras, not to construct particular ones. This is closely related to the usual duality between types and values. It's very common for people new to TypeScript, for instance, to think that `{a: string} | {b: number}` should be `{a: string, b: number}`, because they're thinking primarily in terms of records as sets of fields, not types as sets of values. But making the type bigger makes the set of things you can say about its values (i.e. the space of functions out of it) smaller. Algebras are similarly the "value-like" counterparts to "space-like" monads.
- spion 4y ago
  I have no idea what you mean.
kmill 4y ago
Here's another way to say the general idea, by way of example. Secretly, list is "the" exemplary universal monoid. Given any `a`, then `list a` gives you the free monoid generated by `a`, with composition given by `++` and the identity given by `[]`. Now, let's say you have some `a` such that you're able to come up with a function `ev : list a -> a` that's a monad algebra (i.e., it satisfies the two axioms given by yccs27). Then you're able to conclude that `a` is a monoid(!) and you can extract the monoid structure in the following way: `\ (x y : a) -> ev [x, y]` is the binary operation and `ev []` is the unit. (In particular, `ev` must be some `list.fold`.) I called it `ev` because it's an evaluator/interpreter. To be able to write such a `m a -> a` function, `a` needs to have the same kind of structure that `m` is somehow representing, and you need to be able to map the operation that `m` "contains" to corresponding operations for `a`. This is that business about free monads being useful for organizing how you write interpreters I believe.
- spion 4y ago
  > Then you're able to conclude that `a` is a monoid Yep, which is why I'm saying all the interesting bits come from `a` being the monoid in that example. In the free monad interpreter example, I have no idea though.
  - kmill 4y ago
    If there's a point to any of this, I think it's monads let you package up some algebraic structure in the form of a function `m a -> a` that satisfies certain properties, and then you can pass such a function around without any reference to the fact that `a` implements that algebraic structure. This function is the interface. (Is there real practical significance? I'm not sure, but I'm not trying to argue that :-) ) > all the interesting bits come from `a` being the monoid in that example. Yeah, there's nothing deep there. I just said what I said to underscore that the converse is true, that if anyone were to hand you such a `list a -> a` function then it's encoding some monoid structure on `a` (one of often very many).
yccs27 4y ago
The important point is that each monad (e.g. list) corresponds to an algebraic structure (like monoid). To study the set of algebraic structures, you can also study monads