Dear Olaf,
[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?
Well, these two questions are closely related, as you actually indicate further below. In [1] the main monad is the continuation monad, and equational laws are used as means to classify classes of computations with important properties, but nothing prevents one from using them for classifying monads entirely satisfying such laws.
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
Yes, it is again just the same law: isomorphism of M () and () is a yet more concise way to state this property, neat!
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.
I think [3] and [4] are related (and somewhat contrast [1] and [2]) in that, the laws like discardability are meant to identify those computations (or (sub-)monad), which can in a way play a role of logical assertions. So, the slogan is: assertions are well-behaved computations. In that sense, from the perspective of [3], discardability is a desirable property, but not sufficient. For example, the 'copyability law' do {x <- p; y <- p; return (x, y)} = do {x <- p; return (x, x)} is not satisfied by the probability distribution monad, which is discardable, roughly, because when tossing a coin, getting tails twice in a row is 1/4, while the probability of getting tails after tossing it once is 1/2. So, if we regard sequential composition of programs as a kind of conjunction, then it would not be idempotent. From the perspective of [4], not having copyability is fine, because the underlying logic is meant to be more permissive, and admits non-idempotent conjunctions. Same goes for commutativity: even the conjunction of copyability and discardability does not entail commutativity -- [3] contains a counterexample to this effect (Example 37). Cheers, Sergey
Olaf
[4] https://hal.inria.fr/hal-01446033/file/418352_1_En_5_Chapter.pdf