= Solution
The equivalence holds for every lawful <computational monad> with the semantic equations above. In particular, effects in $e_1$ are neither discarded nor evaluated twice. Fix an initial <semantic environment> $\rho$, and write
$$
E=\operatorname{eval}(e_1)\,\rho,\qquad
\rho_v=\operatorname{extend}(\rho,[(x,v)]),\qquad
F(v)=\operatorname{eval}(e_2)\,\rho_v.
$$
Expanding `Let` and `Val` gives
$$
\begin{aligned}
\operatorname{eval}(\mathsf{let\ val}\ x=e_1\ \mathsf{in}\ e_2)\,\rho
&=\bigl(E\triangleright(\lambda v.\,\operatorname{result}(\rho_v))\bigr)
\triangleright(\lambda\rho'.\,\operatorname{eval}(e_2)\,\rho')\\
&=E\triangleright\bigl(\lambda v.\,
\operatorname{result}(\rho_v)\triangleright(\lambda\rho'.\,\operatorname{eval}(e_2)\,\rho')\bigr)\\
&=E\triangleright F.
\end{aligned}
$$
The two steps use <associativity> and left identity from the <monad laws>.
For the application, evaluating the <lambda abstraction> yields `result c`, where the <programming closure> $c$ satisfies $\operatorname{apply}(c,[v])=F(v)$. The singleton argument evaluator reduces to
$$
\begin{aligned}
\operatorname{evalArgs}([e_1])\,\rho
&=E\triangleright\bigl(\lambda v.\,
\operatorname{result}([])\triangleright(\lambda vs.\,\operatorname{result}(v:vs))\bigr)\\
&=E\triangleright(\lambda v.\,\operatorname{result}([v])).
\end{aligned}
$$
Use left identity to remove the initial `result c`, then <associativity> and left identity again:
$$
\begin{aligned}
\operatorname{eval}((\mathsf{lambda}(x)\ e_2)\ e_1)\,\rho
&=\bigl(E\triangleright(\lambda v.\,\operatorname{result}([v]))\bigr)
\triangleright(\lambda vs.\,\operatorname{apply}(c,vs))\\
&=E\triangleright\bigl(\lambda v.\,
\operatorname{result}([v])\triangleright(\lambda vs.\,\operatorname{apply}(c,vs))\bigr)\\
&=E\triangleright F.
\end{aligned}
$$
Consequently,
$$
\boxed{\operatorname{eval}(\mathsf{let\ val}\ x=e_1\ \mathsf{in}\ e_2)\,\rho
=\operatorname{eval}((\mathsf{lambda}(x)\ e_2)\ e_1)\,\rho
\quad\text{for every lawful }M.}
$$
The argument relies on the <lambda abstraction> itself being effect-free, as specified in part (a), and on using the same <semantic environment> for $e_1$ on each side. No commutativity of effects is assumed. In particular, the proof applies to <state monads>, exceptions and <continuation monads>, not merely to the <identity monad>.
Back to article page
