3
$\begingroup$

Is there a standardized notion of something that removes side effects for an element in a monad?

In the case of state monad:

An element mx : m X is effectively mx : S -> X×S and I would like to turn it into mx':

def mx' : m X := fun (s : S) => (fst (mx s), s)

i.e. remove the effect of mx on the state.

This of course does not make sense for every monad, maybe it makes sense only for state monad. But I can imagine you could use it to suppress writing to a file for example.

So I'm curious if this is a common notion or not.


Edit: Also, what should be the abstract definition of such function? My current definition(in Lean 4) is:

class IgnoreEffect (m : Type u → Type v) [Monad m]
  ignoreEffect {α} : m α → m α

  bind_ignore_effect {α β} (ma : m α) (mb : m β) : 
    (bind (ignoreEffect ma) λ a => mb) = mb

I have a gut feeling there should be an additional law for the case when the value a is actually used. I'm unsure how to formulate it.

$\endgroup$
2
  • $\begingroup$ What are you trying to accomplish? Can you explain the background and motivation for what you'd like to do? $\endgroup$ Commented Mar 13 at 21:16
  • $\begingroup$ This question is almost two years old and I do not even remember what was the exact motivation. I wanted to do automatic differentiation(AD) of monadic code and for that I needed to define what a differentiable monad is. I remember this was part of it but it was dead end. Fortunately, now I have a good definition of differentiable monad and I can successfully run AD on monadic code. $\endgroup$
    – tom
    Commented Mar 13 at 22:50

1 Answer 1

0
$\begingroup$

I would suggest a formulation in two steps:

  1. There must be a natural transformation $\mathrm{run} : \forall a.\, m\,a\to a$.

The function run is a designated "runner" that extracts a value out of a monad.

Note that run is not necessarily a monad morphism $m\to \mathrm{Id}$, where $\mathrm{Id}$ is the identity monad ($\mathrm{Id} \, a = a$). For instance, the State monad does not have such a monad morphism. Some monads do have a monad morphism of that sort; for example, extracting the first element of a non-empty list. Other monads (for example, the continuation monads) cannot even have a natural transformation of type $\forall a.\,m\,a\to a$.

  1. Then we define ignoreEffect = return . run.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.