= Solution
Use the three <monad laws> of the base <computational monad>. For left identity, at an arbitrary <program state> $s$,
$$
\begin{aligned}
(\operatorname{result}(x)\triangleright f)\,s
&=r_m(x,s)\triangleright_m\bigl(\lambda(y,t).\,f(y)\,t\bigr)\\
&=f(x)\,s.
\end{aligned}
$$
The last step is the base left identity law. For right identity,
$$
\begin{aligned}
(p\triangleright\operatorname{result})\,s
&=(p\,s)\triangleright_m\bigl(\lambda(x,t).\,\operatorname{result}(x)\,t\bigr)\\
&=(p\,s)\triangleright_m\bigl(\lambda(x,t).\,r_m(x,t)\bigr)\\
&=(p\,s)\triangleright_m r_m=p\,s.
\end{aligned}
$$
The penultimate equality identifies the pair-destructuring <function> with $r_m$; the last uses the base right identity law.
For <associativity>, expand the two successive uses of sequencing and apply base <associativity>:
$$
\begin{aligned}
((p\triangleright f)\triangleright g)\,s
&=\bigl((p\,s)\triangleright_m(\lambda(x,t).\,f(x)\,t)\bigr)
\triangleright_m(\lambda(y,u).\,g(y)\,u)\\
&=(p\,s)\triangleright_m\bigl(\lambda(x,t).\,
(f(x)\,t)\triangleright_m(\lambda(y,u).\,g(y)\,u)\bigr)\\
&=(p\,s)\triangleright_m\bigl(\lambda(x,t).\,(f(x)\triangleright g)\,t\bigr)\\
&=\bigl(p\triangleright(\lambda x.\,f(x)\triangleright g)\bigr)\,s.
\end{aligned}
$$
No <program state> is duplicated or reset during these rearrangements: both sides pass $s$ to $p$, its output $t$ to $f$, and the output $u$ of $f$ to $g$. By <function extensionality>,
$$
\boxed{\operatorname{result}(x)\triangleright f=f(x),\quad
p\triangleright\operatorname{result}=p,\quad
(p\triangleright f)\triangleright g=p\triangleright(\lambda x.\,f(x)\triangleright g).}
$$
Back to article page
