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

---

## 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`.


---

