<p>There have been a number of developments with regards to the use of monads in the theory of computation since Eugenio Moggi's work. I am not able to give a comprehensive account, but here are some points that I am familiar with, others can chime in with their answers.</p>

<h3>Specific examples of monads</h3>

<p>You do not have to study super-general theory all the time. There are examples of monads that are very interesting and sufficiently complicated to fill an entire undergraduate thesis.</p>

<p>I like very much <a href="http://blog.sigfpe.com">Dan Piponi's blog</a> where he gives amazing examples of how monads can be used to mix functional programming and mathematics. Search for his work on knots and braid through monads, for example.</p>

<p>Another specific example of mondas worth studying was given by Martin Escardo and Paulo Oliva in the context of selection functionals, see their <a href="http://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf">Selection Functions, Bar Recursion, and Backward Induction</a>, or perhaps to get interested first read <a href="http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/Escardo-Oliva-MSFP2010-corrected.pdf">What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common</a> (associated Haskell and Agda files <a href="http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/">here</a>).</p>

<h3>Mathematical background</h3>

<p>Monads come from category theory and are much older than Eugenio Moggi. You could study the background theory if you are mathematically inclined. For instance, you could attack <a href="https://en.wikipedia.org/wiki/Beck%27s_monadicity_theorem">Beck's monadicity theorem</a>. A theoretical computer scientist can never know too much math.</p>

<h3>Variations on a theme</h3>

<p>You could look at something that is not strictly monads.</p>

<p>For instance, Connor McBride and Ross Paterson's <a href="http://staff.city.ac.uk/~ross/papers/Applicative.html">Idioms: applicative programming with effects</a> shows how one can generalize monads to something that is practically relevant and insightful.</p>

<p>Or you could look at how comonads are used to model computational effects. Someone should suggest some references for this topic, but a good start might be <a href="http://www.slideshare.net/davidoverton/comonad">David Overtone's slides</a>.</p>

<h3>Modal type theory</h3>

<p>In homotopy type theory, as well as in type theory in general, monads appear in the shape of <a href="http://ncatlab.org/nlab/show/modal+type+theory">modal type theory</a>. Recently modal type theory has been considered in homotopy type theory because the truncation operators are examples of modal operators. And then there is <a href="http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a> in which modal operators (which are monads) play an essential role.</p>

<h3>Algebraic effects and handlers</h3>

<p>[Disclaimer: partially blowing my own horn here.]</p>

<p>A while ago Gordon Plotkin and John Power obserrved that many computational effects are not just any monads, but special monads arising from algebraic theories. This lead to a whole new treatment of computational effects known as <em>algebraic effects</em>. Later Gordon Plotkin and Matija Pretnar introduced <em>handlers</em> and together with algebraic effects they form a very nice theory of computational effects. One advantage of this approach is that algebraic theories can be easily combined while monads cannot.</p>

<p>You could study how exactly algebraic effects relate to monads. You could look at how people implemented algebraic effects and handlers, say in the <a href="http://www.eff-lang.org">Eff language</a> or in <a href="https://hackage.haskell.org/package/effect-handlers">Haskell as a library</a>. This is more or less current research.</p>

CC BY-SA 3.0
2015-11-13T22:57:26.477Z
Hi, thanks for that answer! I clicked on your website about Eff, and it seems like the link to [An Introduction to Algebraic Effects and Handlers](http://www.eff-lang.org/handlers-tutorial.pdf) is outdated, i.e. the file `eff-lang.org/handlers-tutorial.pdf` is missing.
k.stm
CC BY-SA 3.0
2015-11-13T23:00:47.333Z
I asked Matija to fix the link, in the meantime you could look at http://arxiv.org/abs/1203.1539.
Andrej Bauer
CC BY-SA 3.0
2015-11-13T23:09:55.170Z
I already am. Can you, by the way, give some short overview of the background theory I need to study in order to understand your paper? I know some category theory, untyped lambda calculus and some elementary theory of computation and elementary theory of programming (I know what denotational semantics are), but not much more so far. I can for example already tell from section 3 of your paper that I need to look into typing rules (so maybe into typed lambda calculus). Sorry if I’m being pushy here.
k.stm
CC BY-SA 3.0
2015-11-14T14:25:50.940Z
You should know a bit about universal algebra and/or Lavwere's theory of algebraic theories. If you are not familiar with typing rules then you could study a general textbook on programming languages, such as Benjamin Pierce's [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/) or Bob Harper's  [Practical foundations of programming languages](https://existentialtype.wordpress.com/2012/12/03/pfpl-is-out/).
Andrej Bauer
CC BY-SA 3.0
2015-11-13T22:16:22.673Z
2015-11-13T22:22:43.923Z
2015-11-13T22:22:43.923Z
Andrej Bauer
<p>This <a href="http://okmij.org/ftp/Haskell/extensible/more.pdf" rel="nofollow">paper</a> gives some important recent work using monads.</p>

CC BY-SA 3.0
2015-11-13T21:28:29.167Z
Hi, thanks for your answer. I would appreciate a little context, that is if you can spare the time to give some details. (Actually the paper has nice introduction about its contents, but I would still like to see some context for its surroundings, like if there’s related work and such.)
k.stm
CC BY-SA 3.0
2015-11-13T21:06:24.103Z
2015-11-13T21:06:24.103Z
NietzscheanAI
<p><em>Background</em>. I am a bachelor student who is interested in research related to category theory, monads and Haskell, and I want to find a topic for my bachelor’s thesis in that area.</p>

<p>I have looked at the paper </p>

<ul>
<li><a href="http://www.disi.unige.it/person/MoggiE/" rel="noreferrer">Eugenio Moggi</a>, “<a href="http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf" rel="noreferrer">Notions of Computations and Monads</a>”, 1991,</li>
</ul>

<p>and I do not understand much of it yet. I will probably need quite some time to fully understand it. 
But before spending more time on studying it, I want to get a better understanding of the field and its research potential.
I recently talked to a professor of mine about it and he told me that monads were in fashion in the research community back in the 90s, but nowadays they are out of fashion. </p>

<p><em>Therefore</em>, I am now looking for recent work related to monads, and am wondering:</p>

<ul>
<li>In what areas of theoretical computer science is nowadays research done  that is related to category theory and monads?</li>
<li>What sort of research has been built up or proposed on E. Moggi’s work on monads in the theory of programming? Has there been any follow up or on going research related to his paper?</li>
</ul>

CC BY-SA 3.0
2015-11-13T08:07:31.580Z
Before we answer this question: it is not research-level is it? It may be better suited for cs.stackexchange.com.
Andrej Bauer
CC BY-SA 3.0
2015-11-13T09:11:09.937Z
@AndrejBauer My bachelor thesis will not be research level, but my question addresses current research or at least research made in the last decade.
k.stm
CC BY-SA 3.0
2015-11-13T12:32:39.967Z
@AndrejBauer I disagree. The sister site is mostly for homework questions, whereas here an expert opinion is needed.
Yuval Filmus
CC BY-SA 3.0
2015-11-14T17:46:40.867Z
@Kaveh That was quite the drastic edit you just made. You improved some points, but now it’s not really the question I was asking anymore. When I have time tomorrow, I will rollback some of your changes. For example, it’s important to me to have the background in there. Please tell me what changes you think were necessary and why so I know what not to rollback.
k.stm
CC BY-SA 3.0
2015-11-14T18:13:27.740Z
@Yuval, I think lots of people on [cs.se] would strongly disagree with your comment that it is mainly for homeworks and that experts are not present on [cs.se]. In this case Andrej has answered over 100 questions on [cs.se].
Kaveh
CC BY-SA 3.0
2015-11-14T20:39:03.397Z
@Kaveh I think disagreements are positive. We are all allowed to have our different opinions.
Yuval Filmus
CC BY-SA 3.0
2015-11-14T23:03:08.187Z
@Kaveh Ah, yeah. I see your points. I think the question may interest others as well – even when phrased as a question from a bachelor student’s point of view. (It does have some upvotes and stars). Giving background is also important to give context, so I’m going to put back some of it. In any case, I really like much of your wording and I will keep it for the actual questions.
k.stm
<reference-request><pl.programming-languages><big-picture><ct.category-theory><monad>
Status quo of category theory and monads in theoretical computer science research?
k.stm
# Status quo of category theory and monads in theoretical computer science research?

(Asked by: username_0 on 2015-11-13)

*Background*. I am a bachelor student who is interested in research related to category theory, monads and Haskell, and I want to find a topic for my bachelor’s thesis in that area.

I have looked at the paper

* [Eugenio Moggi](http://www.disi.unige.it/person/MoggiE/), “[Notions of Computations and Monads](http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf)”, 1991,

and I do not understand much of it yet. I will probably need quite some time to fully understand it.
But before spending more time on studying it, I want to get a better understanding of the field and its research potential.
I recently talked to a professor of mine about it and he told me that monads were in fashion in the research community back in the 90s, but nowadays they are out of fashion.

*Therefore*, I am now looking for recent work related to monads, and am wondering:

* In what areas of theoretical computer science is nowadays research done that is related to category theory and monads?
* What sort of research has been built up or proposed on E. Moggi’s work on monads in the theory of programming? Has there been any follow up or on going research related to his paper?

**Tags:** reference-request, pl.programming-languages, big-picture, ct.category-theory, monad
> **Comments:**
> **username_1**: Before we answer this question: it is not research-level is it? It may be better suited for cs.stackexchange.com.  
> **username_0**: @AndrejBauer My bachelor thesis will not be research level, but my question addresses current research or at least research made in the last decade.  
> **username_2**: @AndrejBauer I disagree. The sister site is mostly for homework questions, whereas here an expert opinion is needed.  
> **username_0**: @Kaveh That was quite the drastic edit you just made. You improved some points, but now it’s not really the question I was asking anymore. When I have time tomorrow, I will rollback some of your changes. For example, it’s important to me to have the background in there. Please tell me what changes you think were necessary and why so I know what not to rollback.  
> **username_3**: @Yuval, I think lots of people on [cs.se] would strongly disagree with your comment that it is mainly for homeworks and that experts are not present on [cs.se]. In this case Andrej has answered over 100 questions on [cs.se].  
> **username_2**: @Kaveh I think disagreements are positive. We are all allowed to have our different opinions.  
> **username_0**: @Kaveh Ah, yeah. I see your points. I think the question may interest others as well – even when phrased as a question from a bachelor student’s point of view. (It does have some upvotes and stars). Giving background is also important to give context, so I’m going to put back some of it. In any case, I really like much of your wording and I will keep it for the actual questions.  

---

## 2 answers

### Answer by username_1 on 2015-11-13. Score: 17

There have been a number of developments with regards to the use of monads in the theory of computation since Eugenio Moggi's work. I am not able to give a comprehensive account, but here are some points that I am familiar with, others can chime in with their answers.

### Specific examples of monads

You do not have to study super-general theory all the time. There are examples of monads that are very interesting and sufficiently complicated to fill an entire undergraduate thesis.

I like very much [Dan Piponi's blog](http://blog.sigfpe.com) where he gives amazing examples of how monads can be used to mix functional programming and mathematics. Search for his work on knots and braid through monads, for example.

Another specific example of mondas worth studying was given by Martin Escardo and Paulo Oliva in the context of selection functionals, see their [Selection Functions, Bar Recursion, and Backward Induction](http://www.cs.bham.ac.uk/~mhe/papers/selection-escardo-oliva.pdf), or perhaps to get interested first read [What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common](http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/Escardo-Oliva-MSFP2010-corrected.pdf) (associated Haskell and Agda files [here](http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/)).

### Mathematical background

Monads come from category theory and are much older than Eugenio Moggi. You could study the background theory if you are mathematically inclined. For instance, you could attack [Beck's monadicity theorem](https://en.wikipedia.org/wiki/Beck%27s_monadicity_theorem). A theoretical computer scientist can never know too much math.

### Variations on a theme

You could look at something that is not strictly monads.

For instance, Connor McBride and Ross Paterson's [Idioms: applicative programming with effects](http://staff.city.ac.uk/~ross/papers/Applicative.html) shows how one can generalize monads to something that is practically relevant and insightful.

Or you could look at how comonads are used to model computational effects. Someone should suggest some references for this topic, but a good start might be [David Overtone's slides](http://www.slideshare.net/davidoverton/comonad).

### Modal type theory

In homotopy type theory, as well as in type theory in general, monads appear in the shape of [modal type theory](http://ncatlab.org/nlab/show/modal+type+theory). Recently modal type theory has been considered in homotopy type theory because the truncation operators are examples of modal operators. And then there is [cohesive homotopy type theory](http://ncatlab.org/nlab/show/cohesive+homotopy+type+theory) in which modal operators (which are monads) play an essential role.

### Algebraic effects and handlers

[Disclaimer: partially blowing my own horn here.]

A while ago Gordon Plotkin and John Power obserrved that many computational effects are not just any monads, but special monads arising from algebraic theories. This lead to a whole new treatment of computational effects known as *algebraic effects*. Later Gordon Plotkin and Matija Pretnar introduced *handlers* and together with algebraic effects they form a very nice theory of computational effects. One advantage of this approach is that algebraic theories can be easily combined while monads cannot.

You could study how exactly algebraic effects relate to monads. You could look at how people implemented algebraic effects and handlers, say in the [Eff language](http://www.eff-lang.org) or in [Haskell as a library](https://hackage.haskell.org/package/effect-handlers). This is more or less current research.

> **Comments:**
> **username_0**: Hi, thanks for that answer! I clicked on your website about Eff, and it seems like the link to [An Introduction to Algebraic Effects and Handlers](http://www.eff-lang.org/handlers-tutorial.pdf) is outdated, i.e. the file `eff-lang.org/handlers-tutorial.pdf` is missing.  
> **username_1**: I asked Matija to fix the link, in the meantime you could look at http://arxiv.org/abs/1203.1539.  
> **username_0**: I already am. Can you, by the way, give some short overview of the background theory I need to study in order to understand your paper? I know some category theory, untyped lambda calculus and some elementary theory of computation and elementary theory of programming (I know what denotational semantics are), but not much more so far. I can for example already tell from section 3 of your paper that I need to look into typing rules (so maybe into typed lambda calculus). Sorry if I’m being pushy here.  
> **username_1**: You should know a bit about universal algebra and/or Lavwere's theory of algebraic theories. If you are not familiar with typing rules then you could study a general textbook on programming languages, such as Benjamin Pierce's [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/) or Bob Harper's  [Practical foundations of programming languages](https://existentialtype.wordpress.com/2012/12/03/pfpl-is-out/).  

---

### Answer by username_4 on 2015-11-13. Score: 1

This [paper](http://okmij.org/ftp/Haskell/extensible/more.pdf) gives some important recent work using monads.

> **Comments:**
> **username_0**: Hi, thanks for your answer. I would appreciate a little context, that is if you can spare the time to give some details. (Actually the paper has nice introduction about its contents, but I would still like to see some context for its surroundings, like if there’s related work and such.)  

---

