Programs cause various side effects during their execution, and the static analysis of side effects of programs is one of the important topics in program analysis. Effect systems are a type-theoretic approach to statically estimate side effects caused by programs. In a typical effect system, the estimation is done by constructing abstract representations of a program’s side effects along typing derivations. These representations are often called “effects”.

In a seminal paper [1], Wadler integrated monadic types and effects into the effect-annotated monadic type T(e)(t). Wadler then raises a question of which semantic structure corresponds to the effect-annotated monadic type. In response to this question, I used a structure called graded monad to interpret the effect-annotated monadic type [2]. In this talk, I will introduce graded monads with examples and an application to the semantics of effect systems. I will also talk about algebraic operations of graded monads, the decomposition of graded monads by an adjunction and a twist [3], and the graded TT-lifting of ordinary monads.

[1] Philip Wadler. The Marriage of Effects and Monads. ICFP 1998: 63-74

[2] Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. POPL 2014: 633-646

[3] Soichiro Fujii, Shin-ya Katsumata, Paul-André Melliès. Towards a Formal Theory of Graded Monads. FoSSaCS 2016: 513-530