= Solution
The <continuation> receives both the computed value and the current <computer memory>. Therefore return invokes it with unchanged <computer memory>, while sequencing installs a <continuation> that passes the produced value and updated <computer memory> to the next computation:
``
result :: a -> M a
result x k s = k x s
bind :: M a -> (a -> M b) -> M b
bind p f k s = p (\x s' -> f x k s') s
``
For left identity, expand the two definitions:
$$
(\operatorname{result}(x)\triangleright f)\,k\,s
=(\lambda y\,t.\,f(y)\,k\,t)\,x\,s=f(x)\,k\,s.
$$
For right identity,
$$
(p\triangleright\operatorname{result})\,k\,s
=p(\lambda x\,t.\,\operatorname{result}(x)\,k\,t)\,s
=p(\lambda x\,t.\,k\,x\,t)\,s=p\,k\,s.
$$
For <associativity>, both groupings reduce to the same expression:
$$
\begin{aligned}
((p\triangleright f)\triangleright g)\,k\,s
&=p\bigl(\lambda x\,t.\,f(x)(\lambda y\,u.\,g(y)\,k\,u)\,t\bigr)\,s,\\
\bigl(p\triangleright(\lambda x.\,f(x)\triangleright g)\bigr)\,k\,s
&=p\bigl(\lambda x\,t.\,f(x)(\lambda y\,u.\,g(y)\,k\,u)\,t\bigr)\,s.
\end{aligned}
$$
By <function extensionality>, these establish all three <monad laws>:
$$
\boxed{\operatorname{result}(x)\triangleright f=f(x),\qquad
p\triangleright\operatorname{result}=p,\qquad
(p\triangleright f)\triangleright g=p\triangleright(\lambda x.\,f(x)\triangleright g).}
$$
Back to article page
