Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: free monad as initial algebra

Asad Saeeduddin (Sep 20 2021 at 00:46):

in programming contexts, i usually see the "free monad" formulated as the initial algebra of the endofunctor $\mathbf{1} + F \otimes -$ on the category of endofunctors on typed functions (where $+$ and $\otimes$ denote functor coproduct and composition respectively).

is there somewhere i can see a proof of this construction producing the "free monad monad" on the category of endofunctors? the reason i'm a bit confused is that it seems elsewhere online, the use of the $\mu ( \mathbf{1} + F \otimes - )$ "formula" to calculate the free monoid seems to rely on a distributive relationship $X \otimes (Y + Z) \cong (X \otimes Y) + (X \otimes Z)$ between $\otimes$ and $+$, and in general we can't witness this for arbitrary endofunctors in a programming context. for example, there's no way to purely reveal the result of a side-effectful computation, as would be implied by distribute :: IO (F a + G a) -> IO (F a) + IO (G a)

to give an example of sources that refer to distributivity between monoidal structures: https://ncatlab.org/nlab/show/free+monoid (which doesn't include a proof) says: image.png

and Bartosz Milewski's excellent blog post:

image.png

Mike Shulman (Sep 20 2021 at 01:01):

In the absence of distributivity, you need a different construction of the free monad on an endofunctor, but the free monad still exists (assuming niceness hypotheses). See for instance https://ncatlab.org/nlab/show/transfinite+construction+of+free+algebras.

Asad Saeeduddin (Sep 20 2021 at 01:03):

@Mike Shulman i see. does the solution still take roughly the same form (perhaps we still use $\mu (\mathbf{1} + F \otimes -)$, but restrict ourselves in $F$?) or do we need something totally different?

Mike Shulman (Sep 20 2021 at 01:06):

I don't know what you mean by $\mu(\mathbf{1}+F\otimes -)$.

Mike Shulman (Sep 20 2021 at 01:07):

To me, $\mu$ in this context denotes a least fixed point, which is a characterization of something by a property, not a construction of it.

Mike Shulman (Sep 20 2021 at 01:07):

And what is $\mathbf{1}$?

Mike Shulman (Sep 20 2021 at 01:10):

I'm guessing that by $\mathbf{1}$ you mean the identity endofunctor, and $\otimes$ means the tensor product in the monoidal category of endofunctors, so that $\mu(\mathbf{1}+F\otimes -)$ denotes the left $F$-module freely generated by the unit object in that monoidal category.

Mike Shulman (Sep 20 2021 at 01:11):

So maybe your question is whether, in the general case, the free monad generated by an endofunctor $F$ is also the free left $F$-module generated by the unit?

Mike Shulman (Sep 20 2021 at 01:17):

I don't have time to work out the details right now, but I think that should probably follow from the fact that the free monad is in fact algebraically-free.

Asad Saeeduddin (Sep 20 2021 at 01:24):

@Mike Shulman ah, sorry for being unclear. you've inferred most of what i was trying to say from my confused writing, but i'll try to spell it out anyway:

i am indeed assuming the existence of an (equivalence class of) object characterized by a property. specifically, by $(\mathbf{1} + F \otimes -) : [[\mathcal{C}, \mathcal{C}], [\mathcal{C}, \mathcal{C}]]$ i'm referring to an endofunctor on a category of endofunctors. and by $\mu (\mathbf{1} + F \otimes -) : [\mathcal{C}, \mathcal{C}]$, i'm referring to an object that i assume exists: the carrier of the initial object in the category of F-algebras of $(\mathbf{1} + F \otimes -)$.

and yes, $1$ is the identity functor, $+$ is functor coproduct (we assume that $\mathcal{C}$ is suitable so that this exists), and $\otimes$ is the functor composition monoidal structure on the endofunctor-category $[\mathcal{C}, \mathcal{C}]$.

i'll look through the resources you gave me and hopefully try to muddle through, thank you

Nathanael Arkor (Sep 20 2021 at 10:28):

I think the paper List Objects with Algebraic Structure of Fiore and Saville might also be a helpful place to look, as it has related discussion.