Dear Olaf and everyone, the law do {_ <- b; a} = a is equivalent to do {_ <- b; return ()} = return (), for, assuming the latter, do {_ <- b; a} = do {_ <- do {_ <- b; return ()}; a} = do {_ <- return (); a} = a and it does actually have some history. It was dubbed 'discardability' by Thielecke [1] and explored by Führmann in [2] together with some other important properties of effects, such as 'centrality' and 'commutativity'. Combinations of these properties and examples are explored in the conventional Haskell-like style in [3] (where 'discardability' is called 'side-effect freeness' though). Cheers, Sergey [1] H. Thielecke, Categorical structure of continuation passing style, Ph.D. Thesis, University of Edinburgh, 1997. [2] C. Führmann, Varieties of effects, in: M. Nielsen, U. Engberg (Eds.), Foundations of Software Science and Computation Structures, FOSSACS 2002, in: Lect. Notes Comput. Sci., vol. 2303, Springer, 2002, pp. 144–158. [3] L. Schröder, T. Mossakowski, Monad-independent dynamic logic in HasCasl, J. Logic Comput. 14 (2004) 571–619