# Status quo of category theory and monads in theoretical computer science research?

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

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?
• Before we answer this question: it is not research-level is it? It may be better suited for cs.stackexchange.com. – Andrej Bauer Nov 13 '15 at 8:07
• @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 Nov 13 '15 at 9:11
• @AndrejBauer I disagree. The sister site is mostly for homework questions, whereas here an expert opinion is needed. – Yuval Filmus Nov 13 '15 at 12:32
• @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 Nov 14 '15 at 17:46
• @Yuval, I think lots of people on Computer Science would strongly disagree with your comment that it is mainly for homeworks and that experts are not present on Computer Science. In this case Andrej has answered over 100 questions on Computer Science. – Kaveh Nov 14 '15 at 18:13

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.

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 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, or perhaps to get interested first read What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common (associated Haskell and Agda files here).

### 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. 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 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.

### Modal type theory

In homotopy type theory, as well as in type theory in general, monads appear in the shape of 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 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 or in Haskell as a library. This is more or less current research.

• 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 is outdated, i.e. the file eff-lang.org/handlers-tutorial.pdf is missing. – k.stm Nov 13 '15 at 22:57
• I asked Matija to fix the link, in the meantime you could look at arxiv.org/abs/1203.1539. – Andrej Bauer Nov 13 '15 at 23:00
• 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 Nov 13 '15 at 23:09
• 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 or Bob Harper's Practical foundations of programming languages. – Andrej Bauer Nov 14 '15 at 14:25

This paper gives some important recent work using monads.

• 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 Nov 13 '15 at 21:28