Monads, Not a Thing I Made Up

This post is a part of my blog paleontology series. I dug up and restored this post on 2025-08-11. I made corrections to a number of spelling mistakes.

In college I definitely tried to talk about monads with my friends far too many times. Amazing against all odds, we're still friends to this day.

I was reading about Curry–Howard Correspondence after encountering it again in an Article by Paul Callaghan (I believe I first encounter it in a talk by Simon Peyton Jones). When I reached the final paragraph of the first section I had a real a-ha moment and just had to read the paragraph a second time. The part the interested me was:

"Because of the possibility of writing non-terminating programs, Turing-complete models of computation (such as languages with arbitrary recursive functions) must be interpreted with care, as naive application of the correspondence leads to an inconsistent logic. The best way of dealing with arbitrary computation from a logical point of view is still an actively debated research question, but one popular approach is based on using monads to segregate provably terminating from potentially non-terminating code."

Its little connection like this that help me with understanding topics such as monads.

P.S. the title comes from the fact that my friends claim the word monad is something I made up (and certainly not a real thing).

~ Matt