Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorAntel
   • CommentTimeNov 15th 2021
   • PermaLink
   Author: Antel
   Format: MarkdownItexIn computer science, a [Monad](https://ncatlab.org/nlab/show/monad+%28in+computer+science%29) is always an [Applicative Functor](https://ncatlab.org/nlab/show/applicative+functor). It's regarded as intermediate structure between functors and monads. And it is the programming equivalent of [lax monoidal functors](https://ncatlab.org/nlab/show/monoidal+functor) with [tensorial strength](https://ncatlab.org/nlab/show/tensorial+strength) in category theory. So a Monad in programming is always a lax monoidal functor with tensorial strength. Exactly how is this possible? What I know about Monad in programming is that they are equivalent to a monad on a 'type category' which has 'data types' as objects and 'pure functions' as morphisms. Since data types can always be seen as a set of values, the type category is like a subcategory of Set. Actually an arbitrary subcategory because languages can support any types as they want. I got to know that every monad in Set are [strong monad](https://ncatlab.org/nlab/show/strong+monad), which has tensorial strength by definition. I tried to prove that they eventually form a monoidal functor, but I failed. I could make two different possible candidate for coherence maps from given tensorial strength and costrength, but couldn't prove that they satisfy the commutation condition for the coherence maps. The only thing I could find was that strong monads are [monoidal monad](https://ncatlab.org/nlab/show/monoidal+monad) (and thus monoidal functor) if they are [commutative](https://ncatlab.org/nlab/show/commutative+monad). However, monads are not commmutative in general even in Set. There are many monad which are not commutative in Set, including free monoid monad. (I think they are equivalent to List in programming.) Just proving that every monad in Set are monoidal functor may not be that hard. I rather want to know more fundamental, or generalizable reason behind that (If exist). If I'm not wrong, it seems that every monad in Set are indeed monoidal functor even when they are not commutative. What makes this behavior? What makes every monad or strong monad in certain category be always monoidal functor, even when they are not commutative? I am not a math major and still new to this area. I just got curious about some fundamental things behind tools I have used. I apologize if I said something stupid here.

   In computer science, a Monad is always an Applicative Functor. It’s regarded as intermediate structure between functors and monads.

   And it is the programming equivalent of lax monoidal functors with tensorial strength in category theory. So a Monad in programming is always a lax monoidal functor with tensorial strength.

   Exactly how is this possible? What I know about Monad in programming is that they are equivalent to a monad on a ’type category’ which has ’data types’ as objects and ’pure functions’ as morphisms. Since data types can always be seen as a set of values, the type category is like a subcategory of Set. Actually an arbitrary subcategory because languages can support any types as they want.

   I got to know that every monad in Set are strong monad, which has tensorial strength by definition. I tried to prove that they eventually form a monoidal functor, but I failed. I could make two different possible candidate for coherence maps from given tensorial strength and costrength, but couldn’t prove that they satisfy the commutation condition for the coherence maps.

   The only thing I could find was that strong monads are monoidal monad (and thus monoidal functor) if they are commutative. However, monads are not commmutative in general even in Set. There are many monad which are not commutative in Set, including free monoid monad. (I think they are equivalent to List in programming.)

   Just proving that every monad in Set are monoidal functor may not be that hard. I rather want to know more fundamental, or generalizable reason behind that (If exist).

   If I’m not wrong, it seems that every monad in Set are indeed monoidal functor even when they are not commutative. What makes this behavior? What makes every monad or strong monad in certain category be always monoidal functor, even when they are not commutative?

   I am not a math major and still new to this area. I just got curious about some fundamental things behind tools I have used. I apologize if I said something stupid here.

2. • CommentRowNumber2.
   • CommentAuthorGuest
   • CommentTimeNov 15th 2021
   • PermaLink
   Author: Guest
   Format: MarkdownItexLeaving aside the question [whether the types and functions of a languages actually form a category or not](http://math.andrej.com/2016/08/06/hask-is-not-a-category/) and the morality of fast and loose reasoning, [[strong monad#strong_monads_are_enriched_monads|strong functors $V\to V$ are equivalently $V$-enriched functors]], every (ordinary) functor is uniquely Set-[[enriched functor|enriched]], and to get a lax monoidal structure on a monad $T$ on Set you can just mimic §2 and §7 of [[applicative functor#references|McBride–Paterson (2008)]], but in Set: define $\mathrm{ap}\colon T(X\to Y)\to (T(X)\to T(Y))$ by $\mathrm{ap}(f)(x)=\mu_Y(T(g\mapsto (Tg)(x))(f))$, and then $\_\star\_\colon T(A)\times T(B)\to T(A\times B)$ given by $a\star b\coloneqq\mathrm{ap}(x\mapsto(y\mapsto(x,y)))(a)(b)$ and the component $\eta_1$ of the unit $\eta$ of $T$ make up a [[monoidal functor|lax monoidal structure] on $T$. So I guess it boils down to the fact that $T$ is enriched over the closed monoidal category Set. Note that a [[monoidal monad]] is not just a monad whose underlying functor is lax monoidal: the unit and multiplication have to be [[monoidal natural transformations]], too.

   Leaving aside the question whether the types and functions of a languages actually form a category or not and the morality of fast and loose reasoning, strong functors $V\to V$ are equivalently $V$-enriched functors, every (ordinary) functor is uniquely Set-enriched, and to get a lax monoidal structure on a monad $T$ on Set you can just mimic §2 and §7 of McBride–Paterson (2008), but in Set: define $\mathrm{ap}\colon T(X\to Y)\to (T(X)\to T(Y))$ by $\mathrm{ap}(f)(x)=\mu_Y(T(g\mapsto (Tg)(x))(f))$, and then $\_\star\_\colon T(A)\times T(B)\to T(A\times B)$ given by $a\star b\coloneqq\mathrm{ap}(x\mapsto(y\mapsto(x,y)))(a)(b)$ and the component $\eta_1$ of the unit $\eta$ of $T$ make up a [[monoidal functor|lax monoidal structure] on $T$. So I guess it boils down to the fact that $T$ is enriched over the closed monoidal category Set.

   Note that a monoidal monad is not just a monad whose underlying functor is lax monoidal: the unit and multiplication have to be monoidal natural transformations, too.

3. • CommentRowNumber3.
   • CommentAuthorAntel
   • CommentTimeNov 15th 2021
   • PermaLink
   Author: Antel
   Format: MarkdownItexThank you for the fast answer! I can't say that I understood all of the things you said, but I'll try.

   Thank you for the fast answer! I can’t say that I understood all of the things you said, but I’ll try.

4. • CommentRowNumber4.
   • CommentAuthorGuest
   • CommentTimeNov 15th 2021
   • PermaLink
   Author: Guest
   Format: MarkdownItexI’m sorry if I made it sound overly complicated! I just wanted to say you can take inspiration from Haskell’s usual Applicative instance on Monads (which I guessed/hoped you would be familiar with) to write out the structure maps in terms of the morphism part $g\mapsto T(g)$ and monad structure of $T$ and the closed monoidal structure on Set — I don’t know if there’s anything more general going on than that.

   I’m sorry if I made it sound overly complicated! I just wanted to say you can take inspiration from Haskell’s usual Applicative instance on Monads (which I guessed/hoped you would be familiar with) to write out the structure maps in terms of the morphism part $g\mapsto T(g)$ and monad structure of $T$ and the closed monoidal structure on Set — I don’t know if there’s anything more general going on than that.

5. • CommentRowNumber5.
   • CommentAuthorAntel
   • CommentTimeNov 16th 2021
   • (edited Nov 16th 2021)
   • PermaLink
   Author: Antel
   Format: MarkdownItexThank you. By the way, I got [this](https://math.stackexchange.com/questions/4306514/what-makes-every-strong-monad-on-a-certain-category-be-a-monoidal-functor) answer at mathematics stack exchange. It seems that any strength and costrength of symmetric bistrong monad form coherence maps, thus monoidal functor.

   Thank you. By the way, I got this answer at mathematics stack exchange. It seems that any strength and costrength of symmetric bistrong monad form coherence maps, thus monoidal functor.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeNov 16th 2021
   • PermaLink
   Author: Urs
   Format: MarkdownItexOnce you have sorted this out, it would be great if you could record the insight as a Lemma in an appropriate $n$Lab page!

   Once you have sorted this out, it would be great if you could record the insight as a Lemma in an appropriate $n$Lab page!

7. • CommentRowNumber7.
   • CommentAuthorAntel
   • CommentTimeNov 17th 2021
   • (edited Nov 17th 2021)
   • PermaLink
   Author: Antel
   Format: MarkdownItexAs I said, I am not a math major and new to this area. My ability to express complex things in English is bad and my ability to do in with mathematically plausible way is worse. I'm a bit scared to participate in writing any nLab page. What makes it harder for me is that the strong concepts seem to be related with [enriched](https://ncatlab.org/nlab/show/enriched+category+theory) concepts which I'm not very familiar with. I don't know what did you mean by *the insight*, but please let me explain what made me to have interest on this subject. It all started from my personal project to create a [lecture on monad](https://www.youtube.com/watch?v=gD7U8sfwsuU&list=PLZQAYIhEkMXHPq0bZekOp8oeGZPkqnNWi) for programmers which does not assume for readers to know anything about functional programming other than it uses pure functions, but answers every questions they may have on monad, from every *how* and *what* to every *why*. One of the questions I had to deal with was about monad-specific syntax in some languages (i.e. [do-notation](https://en.wikibooks.org/wiki/Haskell/do_notation) in Haskell, for-comprehension in Scala) and confusing nested lambda patterns they supposed to mean. What's the point of these? Why they are used so much in monad programming? I used a lot of tactics to explain this. At section [1.2](https://youtu.be/vrhiOzXcbC0&t=298) (The audio is in Korean, but the main presentation is in English so one may can understand it just by seeing the presentation), before the concept of monad is introduced, I showed that such thing can also be done for functors. I also introduced an analogy with multi-variable integration at [6:47](https://youtu.be/vrhiOzXcbC0&t=442). Later, this analogy is stretched further to the extent I introduce a concept of integral-specific syntax at section [1.5](https://youtu.be/HFT0QI6XDY8?t=433). All of these efforts helped me a lot to understand monad in programming further. The usual explanation on why monad is so useful in programming, which explains it using the fact that monad form a Kleisli category, is *incomplete*. The full reason behind why monad is so useful is that it can extend not only single-variable functions, but also multi-variable functions in Kleisli way. Working with the second chapter, I wanted to re-explain things I found mathematically. It must be easy and intuitive, like this. 1. Multi-variable functions are used a lot in programming, whether if they are in actual multi-variable form or in equivalent one-variable form. One may want $ X_1 \rightarrow TY_1 $, $ X_2 \rightarrow TY_2 $ and $ (Y_1, Y_2) \rightarrow TZ $ can be composed just like $ X_1 \rightarrow Y_1 $, $ X_2 \rightarrow Y_2 $ and $ (Y_1, Y_2) \rightarrow Z $. 2. Multi-variable functions can be expressed two way in a (closed monoidal) type category. $ Y_1 \otimes Y_2 \rightarrow Z $ or $ Y_1 \rightarrow [Y_2, Z] $. Therefore, one may want for them to be lifted nicely into $ FY_1 \otimes FY_2 \rightarrow FZ $ and $ FY_1 \rightarrow [FY_2, FZ] $ for each by a functor $ F $, and the transformations preserve 2-variable composition just as functors preserve 1-variable composition. It never happens. They just become $ F(Y_1 \otimes Y_2) \rightarrow FZ $ and $ FY_1 \rightarrow F[Y_2, Z] $ for each. 3. Thankfully, we have saviors named bistrength (strength and costrength commuting each other) for type categories. They makes the type category to be monoidal, i. e, give natural transformations $ FY_1 \otimes FY_2 \rightarrow F(Y_1 \otimes Y_2) $ and $ F[Y_2, Z] \rightarrow [FY_2, FZ] $ which we want. One can now define 2-variable (and eventually, multi-variable) lift for 2-variable functions by composing $ F(f) $ with these transformations, and this transformation turns out to preserve 2-variable compositions just like functors for 1-variable compositions. The problem was that I couldn't prove that every bistrong monad are (lax) monoidal functor. It was too complex for me to prove by myself. That's why I asked about that here and there. Now I got Dan Doel's [answer](https://math.stackexchange.com/questions/4306514/what-makes-every-strong-monad-on-a-certain-category-be-a-monoidal-functor). I think his answer is correct. This is full story of me. I don't know if there is any mathmatically meaningful here except the final proof I got from Dan Doel. Most of these are just about some new methodology to teach/explain monad in programming, anyway.

   As I said, I am not a math major and new to this area. My ability to express complex things in English is bad and my ability to do in with mathematically plausible way is worse. I’m a bit scared to participate in writing any nLab page. What makes it harder for me is that the strong concepts seem to be related with enriched concepts which I’m not very familiar with.

   I don’t know what did you mean by the insight, but please let me explain what made me to have interest on this subject.

   It all started from my personal project to create a lecture on monad for programmers which does not assume for readers to know anything about functional programming other than it uses pure functions, but answers every questions they may have on monad, from every how and what to every why.

   One of the questions I had to deal with was about monad-specific syntax in some languages (i.e. do-notation in Haskell, for-comprehension in Scala) and confusing nested lambda patterns they supposed to mean. What’s the point of these? Why they are used so much in monad programming?

   I used a lot of tactics to explain this. At section 1.2 (The audio is in Korean, but the main presentation is in English so one may can understand it just by seeing the presentation), before the concept of monad is introduced, I showed that such thing can also be done for functors. I also introduced an analogy with multi-variable integration at 6:47. Later, this analogy is stretched further to the extent I introduce a concept of integral-specific syntax at section 1.5.

   All of these efforts helped me a lot to understand monad in programming further. The usual explanation on why monad is so useful in programming, which explains it using the fact that monad form a Kleisli category, is incomplete. The full reason behind why monad is so useful is that it can extend not only single-variable functions, but also multi-variable functions in Kleisli way.

   Working with the second chapter, I wanted to re-explain things I found mathematically. It must be easy and intuitive, like this.

   1. Multi-variable functions are used a lot in programming, whether if they are in actual multi-variable form or in equivalent one-variable form. One may want $X_1 \rightarrow TY_1$, $X_2 \rightarrow TY_2$ and $(Y_1, Y_2) \rightarrow TZ$ can be composed just like $X_1 \rightarrow Y_1$, $X_2 \rightarrow Y_2$ and $(Y_1, Y_2) \rightarrow Z$.

   2. Multi-variable functions can be expressed two way in a (closed monoidal) type category. $Y_1 \otimes Y_2 \rightarrow Z$ or $Y_1 \rightarrow [Y_2, Z]$. Therefore, one may want for them to be lifted nicely into $FY_1 \otimes FY_2 \rightarrow FZ$ and $FY_1 \rightarrow [FY_2, FZ]$ for each by a functor $F$, and the transformations preserve 2-variable composition just as functors preserve 1-variable composition. It never happens. They just become $F(Y_1 \otimes Y_2) \rightarrow FZ$ and $FY_1 \rightarrow F[Y_2, Z]$ for each.

   3. Thankfully, we have saviors named bistrength (strength and costrength commuting each other) for type categories. They makes the type category to be monoidal, i. e, give natural transformations $FY_1 \otimes FY_2 \rightarrow F(Y_1 \otimes Y_2)$ and $F[Y_2, Z] \rightarrow [FY_2, FZ]$ which we want. One can now define 2-variable (and eventually, multi-variable) lift for 2-variable functions by composing $F(f)$ with these transformations, and this transformation turns out to preserve 2-variable compositions just like functors for 1-variable compositions.

   The problem was that I couldn’t prove that every bistrong monad are (lax) monoidal functor. It was too complex for me to prove by myself. That’s why I asked about that here and there. Now I got Dan Doel’s answer. I think his answer is correct.

   This is full story of me. I don’t know if there is any mathmatically meaningful here except the final proof I got from Dan Doel. Most of these are just about some new methodology to teach/explain monad in programming, anyway.