[Haskell-cafe] What to call Occult Effects

[Olaf Klinke]

> 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