-1
$\begingroup$

I have been studying some category theory only to understand the "why" behind the various categorical constructs we use ("borrow") in the world of functional programming.

One of the oft cited maxims is this:

A monad is just a monoid in the category of endofunctors

Can we structure all programs to be a composition of pure and monadic functions and nothing else? If so, would the resultant "compositional structure" be monoidal?

Is it fair to infer such a "monoidal property" to exist for all programs (i.e., computable functions) ?

It seems that this should be intuitively true, but I'm not sure where (if at all) is a flaw in this inference? What may I be missing?

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ It is not clear what you are asking, at least not to me. What are some precise examples of "monoidal structure" that you speak of? Are you just talking about monads and the fact that the Kleisli category of a monad captures (in some cases) a notion of effectful computation? $\endgroup$
    – Andrej Bauer
    Jul 24, 2020 at 12:49
  • 1
    $\begingroup$ I too think that the question is unclear. First of all, you probably mean monadic rather than "monoidal", as you seem to be talking about monads whereas the latter adjective usually has a different meaning in category theory. And the fact that a monad is a monoid in the the category of endofunctors is not a "maxim", it's a mathematical fact/definition. Also, if you say that your programming language is represented by a category $C$, then of course you can't go outside of $C$ if you don't go outside of your programming language. $\endgroup$
    – Damiano Mazza
    Jul 25, 2020 at 5:59
  • 1
    $\begingroup$ And no, cartesian closure has nothing to do with mixing pure and impure functions: it simply means that you may "curry/uncurry" your functions to freely go back and forth between $(A\times B)\to C$ and $A\to B\to C$. What does your "chain" $C\to C\to C\to\cdots$ refer to? Are you composing monads? Do you know that monads do not compose in general? What in the world is a "meta-reason" and what "loop" are you closing? It is difficult to tell weather a reasoning is flawed or not when the reasoning itself is so confusing... $\endgroup$
    – Damiano Mazza
    Jul 25, 2020 at 6:01
  • 2
    $\begingroup$ Nope, still unclear. You are asking a question about a very well-developed area of PL research which abounds in precise concepts. You should strive to ask your question without using any derision quotes. Words like "monoidal" have a few meanings, all of them precise. If there is some unclarity about how monads are used to model computation, perhaps you should ask a more basic question about that (and judge apprpriately whether the question belongs here or on CS SE). As it stands, your question is not clear, at least not to me. $\endgroup$
    – Andrej Bauer
    Jul 28, 2020 at 8:03
  • 2
    $\begingroup$ Here's another problem. When you say "all programs are X" that is almost never going to make sense, unless you carefully delimit what you mean by "program". Words like "computation" and "program" are open-ended concepts that develop through time. If you are asking a mathematical question (about things being monadic or monoidal) then you should refer to precise concepts. Fix a programming language and ask a question about it, then at lest we'll have some context. (And we'll discover what many books explain, namely that monads give compositional structure to effectful computation.) $\endgroup$
    – Andrej Bauer
    Jul 28, 2020 at 8:06

1 Answer 1

Reset to default
1
$\begingroup$

I am going to answer the question from your title in a slightly facetious way:

Computable maps are closed under composition, and the identity map is computable, therefore the collection of all computable maps $\mathbb{N} \to \mathbb{N}$ forms a monoid with respect to composition.

Perhaps you meant to aks whether there was a monad involved, in which case:

The category of sets and partial maps is equivalent to the Kleisly category for the lifting monad. The equivalence specializes to a computable setting, such as PER model or more generally a realizability topos. Therefore, the computable partial maps can be seen as effectful maps, where the effect is that of non-termination, as captured by the lifting monad.

I do not think this is what you asked, but perhaps seeing the answer will make it clearer to you that the audience is having trouble understanding your question.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I appreciate you taking a stab at answering the question. You're right that it doesn't answer my question per se, but provides me food for thought to help my hash out the missing pieces in my understanding. For context, this question was an off-shoot of this one on CS.se: cs.stackexchange.com/questions/128627/… $\endgroup$
    – PhD
    Jul 30, 2020 at 17:05

Not the answer you're looking for? Browse other questions tagged or ask your own question.