News for hackers. Stuff that matters.
Re:Monad Confusion and the Blurry Line Between Data and Comp... by yccs27 on Saturday August 06, 2022 @03:13PM (#32370748)
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)

Re:Monad Confusion and the Blurry Line Between Data and Comp... by spion on Saturday August 06, 2022 @03:48PM (#32370986)
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)

Re:Monad Confusion and the Blurry Line Between Data and Comp... by kmill on Saturday August 06, 2022 @06:52PM (#32372312)
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.

Re:Monad Confusion and the Blurry Line Between Data and Comp... by spion on Sunday August 07, 2022 @05:54AM (#32375224)
> 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.

Re:Monad Confusion and the Blurry Line Between Data and Comp... by kmill on Sunday August 07, 2022 @11:38AM (#32377281)
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).

Re:Monad Confusion and the Blurry Line Between Data and Comp... by hither_shores on Saturday August 06, 2022 @04:31PM (#32371350)
> 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.

Re:Monad Confusion and the Blurry Line Between Data and Comp... by spion on Sunday August 07, 2022 @08:57AM (#32376125)
I have no idea what you mean.
Re:Monad Confusion and the Blurry Line Between Data and Comp... by yccs27 on Sunday August 07, 2022 @06:52AM (#32375481)
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