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
I've got the impression that all three of the above works look at a problem dual to the OP in a certain sense: At least [1] and [2] ask: For a given monad M, what is the subset of computations b with b >> a = a for all a? In contrast, I understood Kim-Ee's question as: What are the monads M where all computations b belong to this class? Assuming this property, the monoid M () is isomorphic to (). Indeed, the monoid M () inherits the property a <> b = b for all a, b :: M () and the only monoid with this property is the one- element monoid. In category theory a monad M with M 1 being isomorphic to the terminal object 1 is called 'affine'. Bart Jacobs in [4] gives a diagram (10) that amounts to return.const = fmap.const and shows that this is equivalent to being affine. Hence we might also use 'affine' for monads with Kim-Ee's property. Bart Jacobs' proof first reduces the general identity return.const = fmap.const :: a -> m b -> m a to the case b = () just as Sergey did above. Then = fmap (const a) = fmap (const a) . (id :: m () -> m ()) = fmap (const a) . return . const () by assumption = return . const a . const () by naturality of return = return . const a property of const I also learned that the school of 'effects' tries to avoid monads (this going back to John Power), so the terms 'discardable' and 'affine' might just be names for the same thing in different communities. Further there is a categorical construction (see [4]) to compute the greatest affine sub-monad of a monad. Interestingly, the affine part of the state monad is the reader monad, that is, functions s -> (a,s) that may use s but not change it. Olaf [4] https://hal.inria.fr/hal-01446033/file/418352_1_En_5_Chapter.pdf