<p>I would suggest a formulation in two steps:</p>
<ol>
<li>There must be a natural transformation <span class="math-container">$\mathrm{run} : \forall a.\, m\,a\to a$</span>.</li>
</ol>
<p>The function <code>run</code> is a designated &quot;runner&quot; that extracts a value out of a monad.</p>
<p>Note that <code>run</code> is <em>not</em> necessarily a monad morphism <span class="math-container">$m\to \mathrm{Id}$</span>, where <span class="math-container">$\mathrm{Id}$</span> is the identity monad (<span class="math-container">$\mathrm{Id} \, a = a$</span>). 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 <span class="math-container">$\forall a.\,m\,a\to a$</span>.</p>
<ol start="2">
<li>Then we define <code>ignoreEffect = return . run</code>.</li>
</ol>

CC BY-SA 4.0
2024-03-13T11:06:37.797Z
2024-03-22T10:24:57.393Z
2024-03-22T10:24:57.393Z
winitzki
<p>Is there a standardized notion of something that removes side effects for an element in a monad?</p>
<p>In the case of state monad:</p>
<p>An element <code>mx : m X</code> is effectively <code>mx : S -&gt; X×S</code> and I would like to turn it into <code>mx'</code>:</p>
<pre><code>def mx' : m X := fun (s : S) =&gt; (fst (mx s), s)
</code></pre>
<p>i.e. remove the effect of <code>mx</code> on the state.</p>
<p>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.</p>
<p>So I'm curious if this is a common notion or not.</p>
<hr />
<p>Edit: Also, what should be the abstract definition of such function? My current definition(in Lean 4) is:</p>
<pre><code>class IgnoreEffect (m : Type u → Type v) [Monad m]
  ignoreEffect {α} : m α → m α

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

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

CC BY-SA 4.0
2024-03-13T21:16:11.200Z
What are you trying to accomplish? Can you explain the background and motivation for what you'd like to do?
Andrej Bauer
CC BY-SA 4.0
2024-03-13T22:50:33.393Z
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.
tom
<monad>
Ignore side effect in monadic code
tom
# Ignore side effect in monadic code

(Asked by: username_0 on 2022-05-26)

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.

**Tags:** monad

> **Comments:**
> **username_1**: What are you trying to accomplish? Can you explain the background and motivation for what you'd like to do?  
> **username_0**: This question is almost two years old and I do not even remember what was the exact motivation. I wanted to do auusername_0atic 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.  

---

## 1 answers

### Answer by username_2 on 2024-03-13. Score: 0

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$.

2. Then we define `ignoreEffect = return . run`.


---

