It is folklore knowledge that a pair of adjoint functors induces a monad and a comonad. Due to my recent work, I had to load relevant information into my brain cache. However, it turned out to be hard for me to find all the pieces of information I need in one place. Therefore, I am going to summarise here what I know and need, hoping it will be helpful for someone like me.
I started to take an interest in reasoning and derivation of monadic programs around 2016-17. Several years having passed, I collaborated with many nice people, managed to get some results published, failed to publish some stuffs I personally like, and am still working on some interesting tiny problems. This post summaries what was done, and what remains to be done.
Shin-Cheng Mu and José Nuno Oliveira. Programming from Galois connections. In the Journal of Logic and Algebraic Programming , Vol 81(6), pages 680–704, August 2012.
[PDF]
One is often amazed that, once two functions are identified as a Galois connection, a long list of nice and often useful properties follow from one concise, elegant defining equation. But how does one construct a program from a specification given as a Galois connection?
Shin-Cheng Mu and José Nuno Oliveira. Programming from Galois connections — principles and applications. Technical Report TR-IIS-10-009, Academia Sinica, December 2010.
[PDF]
Shin-Cheng Mu and José Nuno Oliveira. Programming from Galois connections. In the 12th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS #12), LNCS 6663, pages 294-313. May 30 – June 3, 2011.
[PDF]
In the recent work of Sharon and me on maximally dense segments we needed quite a number of functions to be monotonic, idempotent, etc. It only occurred to me after submitting the paper: could they be defined as Galois connections?