<p>The law <code>bind m (f ∘ g) = f (bind m g)</code> does not hold.</p>
<p>The types of functions are: <code>m : M a</code>, <code>f : M b -&gt; M c</code>, <code>g : a -&gt; M b</code>.</p>
<p>The law would hold if <code>f</code> were a function of the form <code>fmap h</code> with some <code>h : b -&gt; c</code>. Then the law would hold due to the naturality law of <code>bind</code>.</p>
<pre><code> bind m (fmap h ∘ g) = fmap h (bind m g)
</code></pre>
<p>A function <code>f</code> of the form <code>f = fmap h</code> may not modify any effects in <code>M</code>; it may only modify the wrapped values. But a general function <code>f : M b -&gt; M c</code> may modify effects. The law would essentially say that the composition of effects in <code>m</code> with the effect in <code>f(g)</code> should be the same as <code>f</code> applied to the composition of effects in <code>m</code> and <code>g</code>. But that is not necessarily true, because <code>f</code> may transform effects arbitrarily.</p>
<p>As a counterexample, take <code>M = Maybe</code>, choose all types to be just <code>Int</code>, and let <code>f</code> transform <code>Maybe</code>'s effects in some way:</p>
<pre><code> f :: Maybe Int -&gt; Maybe Int
 f _ = Just 123
</code></pre>
<p>Choose <code>m = Nothing</code> (and <code>g</code> can be any function). Then <code>bind m (f ∘ g)</code> is also <code>Nothing</code>. However, <code>f (bind m g)</code> is <code>Just 123</code> because <code>f</code> always returns that value. So, <code>bind m (f ∘ g)</code> is not equal to <code>f (bind m g)</code>. The law fails to hold.</p>

CC BY-SA 4.0
2024-04-25T10:03:49.050Z
2024-04-25T12:00:25.317Z
2024-04-25T12:00:25.317Z
winitzki
<p>This law about bind and function composition type checks:</p>
<pre><code>bind m (f o g) = f (bind m g)
</code></pre>
<p>but it is not clear whether it is true and how can it be proved.</p>
<p>How could I prove this? References are welcome.</p>

CC BY-SA 4.0
2024-04-25T07:32:43.420Z
I think this law does not hold. It would hold (via `bind`'s naturality law) only if `f = fmap h` where `fmap` is for the type constructor of the monad.
winitzki
<functional-programming><monad>
A monad law about bind and function composition
Gergely
# A monad law about bind and function composition

(Asked by: username_0 on 2024-04-24)

This law about bind and function composition type checks:
bind m (f o g) = f (bind m g)

but it is not clear whether it is true and how can it be proved.
How could I prove this? References are welcome.

**Tags:** functional-programming, monad
> **Comments:**
> **username_1**: I think this law does not hold. It would hold (via `bind`'s naturality law) only if `f = fmap h` where `fmap` is for the type constructor of the monad.  

---

## 1 answers

### Answer by username_1 on 2024-04-25. Score: 5 | Accepted answer

The law bind m (f ∘ g) = f (bind m g) does not hold.
The types of functions are: m : M a, f : M b -> M c, g : a -> M b.
The law would hold if f were a function of the form fmap h with some h : b -> c. Then the law would hold due to the naturality law of bind.
 bind m (fmap h ∘ g) = fmap h (bind m g)

A function f of the form f = fmap h may not modify any effects in M; it may only modify the wrapped values. But a general function f : M b -> M c may modify effects. The law would essentially say that the composition of effects in m with the effect in f(g) should be the same as f applied to the composition of effects in m and g. But that is not necessarily true, because f may transform effects arbitrarily.
As a counterexample, take M = Maybe, choose all types to be just Int, and let f transform Maybe's effects in some way:
 f :: Maybe Int -> Maybe Int
 f _ = Just 123

Choose m = Nothing (and g can be any function). Then bind m (f ∘ g) is also Nothing. However, f (bind m g) is Just 123 because f always returns that value. So, bind m (f ∘ g) is not equal to f (bind m g). The law fails to hold.


---

