I’ve been asked a few times now for the history behind graded modalities (graded monads and graded comonads). So I decided to just type up the history real fast so I can easily send it to others. I’ll break this down into a chronological list of papers for graded monads (graded effects) and graded comonads (graded coeffects or graded resource tracking). This is not a complete bibliography, but a list of papers that could be considered milestone papers.
Additions and clarifications welcome!
Graded Monads
- 2003: The marriage of effects and monads by Wadler and Thiemann
- 2007: New approach to Arakelov geometry by Nikolai Durov
- 2007: Graded monads and rings of polynomials by A. L. Smirnov
- 2008: Graded monads and rings of polynomials by A. L. Smirnov
- 2014: Parametric Effect Monads and Semantics of Effect Systems Shin-ya Katsumata
- 2014: The semantic marriage of monads and effects by Dominic Orchard, Tomas Petricek, Alan Mycroft
- 2016: Towards a Formal Theory of Graded Monads by Soichiro Fujii, Shin-ya Katsumata, Paul-André Melliès
- 2016: Combining effects and coeffects via grading by Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, Tarmo Uustalu
- 2020: Unifying graded and parameterised monads by Dominic Orchard, Philip Wadler, Harley Eades III
Graded Comonads
- 1970: Grades of Modality by L. F. Goble
- 1972: In so many possible worlds by Kit Fine
- 1973: Counterfactuals by David K. Lewis
- 1992: Bounded linear logic: a modular approach to polynomial-time computability by Jean-Yves Girardm Andre Scedrov, Philip J. Scott
- 2013: Coeffects: Unified static analysis of context-dependence by Petricek, Orchard, and Mycroft
- 2014: Coeffects: A calculus of context-dependent computation by Petricek, Orchard, and Mycroft
- 2014: A Core Quantitative Coeffect Calculus by Aloïs BrunelMarco GaboardiDamiano MazzaSteve Zdancewic
- 2014: Bounded linear types in a resource semiring by Dan R. GhicaAlex I. Smith
- 2016: Combining effects and coeffects via grading by Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, Tarmo Uustalu
- 2016: I Got Plenty o’ Nuttin’ by Conor McBride
- 2017: The Syntax and Semantics of Quantitative Type Theory by Robert Atkey
- 2017: Linear Haskell: Practical Linearity in a Higher-order Polymorphic Language by Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack
- 2018: A Double Category Theoretic Analysis of Graded Linear Exponential Comonads by Shin-ya Katsumata
- 2019: Quantitative program reasoning with graded modal types by Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III
- 2020: A unified view of modalities in type systems by Andreas Abel, Jean Philippe Bernardy
- 2021: A graded dependent type system with a usage-aware semantics by Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, Stephanie Weirich