Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
started monad (in computer science)
(also added it as one line to the big table at computational trinitarianism)
I’ve never heard of a field called “programming theory”. Perhaps computer science would be what you want? Or if you want to specifically refer to the formal study of programming languages within computer science, I think people call that something more like “programming language theory”, although I’m not sure if I’ve seen it written out that way rather than just “PL theory”.
Yes, I googled around a bit before I created that entry, and noticed that. But I wanted the entry to be called this, so that it fits into saying
Because the alternative
looks really bad. ;-)
But, okay, I admit that I am being whimsical. I’ll be following suggestions for how to make up for this sin.
My suggestion is to rename the page to monad (in computer science) and delete the page programming theory.
All right. Done.
(By the way, I have changed it also in this thread here. Just as a note to future readers, who may wonder what we are talking about…)
For a reference, I’m betting that Dan Piponi has lots of good stuff at his blog, although programming theory or whatever-you-call-it isn’t my domain.
Yes, I saw an exposition by Dan Piponi on monads in computer science.
Hi Todd,
now that I have more of a spare minute, I guess you were referring to my request in the entry “somebody please add a good reference”.
So, yes, Piponi gives somehwhere a basic non-technical and pedagogical exposition of the example of how to encode functions with side effects in a functional language. I suppose that’s a good reference for those looking for this kind of thing, but what I would like to see is not this kind of exposition.
I am longing to find a reference that gets to the point right away, with precision and clearly. I know what a monad is. I know what a type system is. I have trouble reading Haskell code though. So I would like to see an authorative reference that goes like this:
“A monad in a typed functional programming language is” and then bang-bang-bang the definition. Like: “is an endomorphism of the type universe such that…”. Well, that’s roughly what I put into the entry. I just would like to point to some technical paper that actually says this.
That reminds me; I was wondering if I could point out the Wikipedia entry Monad (functional programming) as an illustrative example for how not to write Wiki entries:
first paragraph of the Idea-section: means nothing to somebody who doesn’t already know what the entry is about, and I think not useful even if one does
second paragraph of the Idea section: we hear what the topic of the entry is good for, but we still don’t know what the topic is.
third paragraph of the Idea section: that paragraph is actually where the definition is hidden! This is the single most useful paragraph of the whole entry. Trouble is, on first reading I had given up on the Idea section at this point already, so I didn’t even see this. Also I didn’t expect the Definition to be hidden there.
next comes a paragraph on history. The reader (who didn’t make it to the last part of the intro) still has no idea what the topic of the entry is, but now he learns many names of people who invented it.
then “Background and notational conventions” provides neither background nor notational conventions. Nor would this seem to be what the reader needs now.
Now motivating examples. That might of course be a good way to introduce a complicated subject – only that the subject is not actually complicated, its abstract definition is simpler than any of its examples. On first reading of the entry, this whole motivating example was entirely Chinese to me. (Now that I understand what’s going on, I can read it.)
same for the next motivating example
so we are now one third into a long entry and first time I arrived here I had still no idea what the entry was trying to tell me. But now at least the announcement: “formal definiton”. So I expect Definitions: X is Y such that Z. It’s roughly like that, but still not really focused. Is the first sentence there even sensible: “A monad is a construction that, given an underlying type system, embeds a corresponding type system (called the monadic type system) into it”?
Next comes lots of Haskell code… and so I give up.
It was after such experiences that I thought: please, somebody point me to a sober, concise technical definition.
A monad in a typed functional programming language is
Well, it’s funny, because earlier I thought I had read somewhere on Piponi’s blog exactly the type of crisp thing you are looking for, and now I can’t find it! But the idea was, roughly as I remember it, to cast the Kleisli category construction into typed functional programming language.
You might try asking on MO or something, if you can’t get satisfactory answers here.
Ah, I see. So I have checked again: what I had seen before on Dan Piponi’s blog is this here:
Now I see that there is also a link to:
Is that maybe what you are thinking of? (I still need to look through it.)
No, I don’t recognize what I saw in either of those.
It may have been the more succinct formulation (that I think I saw, involving two term-formation rules) was still embedded in the middle of fluff, but my memory is that you might have liked it. Sorry I’m not being more helpful.
Sorry I’m not being more helpful.
No that is helpful, thanks. This way I know what to look for. I just need to finish something else first, so I’ll continue this quest here a little later.
(Well, I guess Mike could write an account to all our heart’s content. But there must exist a good account somewhere already, right? :- )
Yeah, there must, mustn’t there? I look forward to hearing about one when you find it.
I touched the page briefly, linking to strong monad. Also is a comonad, not a monad, right? It’s and that are the monads.
I’ve edited the Idea section a bit, trying to make it a bit more intuitive. See what you think.
I can’t think of an introduction to monads in programming that’s suited to mathematicians rather than programmers; I suspect we may have to write our own. The original reference would be Moggi’s thesis, I’ll try and find the exact reference and maybe a link.
Thanks Finn!
By the way, we have syntactic category. I made it a hyperlink in your text.
I like what you added, but now the entry takes quite a bit before it starts saying anything about what a monad in a programming language actually is. I would like the very first sentence of the entry to be such that the reader already gets an idea where the journey is actually going. Can you think of something very brief to put before what you just added. We need a sentence brief but accurate and genuinely, informative. Maybe:
A monad in a programming language is a map then sends every type to a new type equipped with a function and a coherent rule to compose a function with a function to a function .
Something like this. And then we can explain all the relation to category theory etc. pp. I would suggest all that about props as types etc. pp should really go in a separate subsection. It should come after the main idea has already been stated.
What do you think?
(I’ll leave it at that now, have to call it quits.)
I have expanded and restructured the entry further. Check it out: monad (in computer science) .
I tried to disentangle the idea in CS from the interpretation in CT, tried to have a brief crisp Intro-paragraph that already says it all, with the remaing comments on that split into two further subsections. In one I try to expand on the example of side-effects. Check if I did that decently. Feel free to edit further.
There are still lots of grey links which make the entry look ugly. To remove at least one of them, I created a stub for programming language.
Looks good! I have corrected a couple of typos, expanded on the example, and added a reference to Moggi’s original article.
Under Examples I have made the following simple one explicit:
A program with input of type , output of type and mutable state is a function of type . Under the (Cartesian product internal hom)-adjunction this is equivalently given by its adjunct, which is a function of type . Here the operation is the monad induced by the above adjunction and this latter function is naturally regarded as a morphism in the Kleisli category of this monad.
Is that what is called the “state monad”?
(The entry has been pointing to state monad all along, but the link is dead. When I google for “state monad” I get Haskell code, which I am not in the mood of decyphering right now. )
Yes.
Thanks. So I copied my little paragraph to a standalone entry state monad. Cross-linked also with internal hom.
Somebody should write something at maybe monad. (What is the maybe monad, category-theoretically? Something like ?)
Would the exponential monad be a monad to list as an example of “monads in computer science”? Is it used in genuine computer science? (I’d expect it is, just checking.)
Do you mean the monad ? That’s called the continuation monad.
I really meant the exponential modality. But thanks for the continuation monad, I’ll add that, too. (Why “continuation”?)
I dare say the boundaries of “genuine computer science” are disputed :). Taking a generous view, how about Linearity and nonlinearity in distributed computation?
By the way, do tell us what’s going on at “Philosophy of Mechanics: Mathematical Foundations”.
I dare say the boundaries of “genuine computer science” are disputed
I know, I meant if those people who think that a monad is something about Haskell (those who think that computer science has to do with electronic computers ;-) use anything like linear logic’s exponential modality. If they do, they probably have some cute name for it. That’s what I was after.
By the way, do tell us what’s going on at “Philosophy of Mechanics: Mathematical Foundations”.
Unfortunetaly I will only be able to make a lighning appearance there from the conference Dinner on Thrusday night on to after the morning session on Friday. Tomorrow I also have to be at Higher Structures, Lower Rhine. Then from there right into the Thalys to Paris
Re #24: I think it’s in reference to continuation-passing style, which is a style of computer programming.
Well, Haskell is a nonlinear language, so I don’t think the exponential modality would be visible to it.
The maybe monad is indeed .
@Todd, yes thanks, I had figured meanwhile and had put that into continuation monad.
@Mike, thanks for confirming the maybe monad. Haskell or not (maybe somebody wrote a linear variant?), any programming language where people consider the exonential monad?
okay, I have created a minimum maybe monad.
Possibly there should be a comment that it has the maybe-interpretation only when the ambient category is extensive, or similar?
Hm, so the maybe monad actually appears prominently in other entries.
its algebras are pointed objects;
its underlying functor is the one use initial algebras are natural number objects.
Is this just something that so happens, or is there some story here to be told involving the words “maybe”, “pointed object” and “natural number object”?
I actually deleted programming theory (really moved it to programming theory > history) as suggested above (#4–6) and put its text in an appropriate spot in the introduction to computer science.
1 to 31 of 31