= Solution
Expand the two <type synonyms> to see what survives an exception:
$$
\begin{aligned}
\operatorname{ExT}(\operatorname{MemT}\ m)\ A
&=\operatorname{Mem}\to m(\operatorname{Maybe}\ A,\operatorname{Mem}),\\
\operatorname{MemT}(\operatorname{ExT}\ m)\ A
&=\operatorname{Mem}\to m(\operatorname{Maybe}(A,\operatorname{Mem})).
\end{aligned}
$$
In the first order, a failed computation can still produce `(Nothing,s')`. The exception handler therefore runs with $s'$, including writes made before failure. In the second order, failure produces `Nothing`, with no returned <computer memory>. A handler defined by applying the underlying `orelse` pointwise runs its alternative from the original input <computer memory> $s$. This gives rollback of this explicit <program state> for the failed branch.
For example, start with a <memory location> holding $0$, write $1$, fail, and handle the failure by reading that <memory location>. The first order returns $1$; the second returns $0$. This rollback concerns the explicit <computer memory> only: arbitrary effects in the base <computational monad> are not thereby reversed.
$$
\boxed{\begin{aligned}
\operatorname{ExT}(\operatorname{MemT}\ m)&:\text{ writes survive failure};\\
\operatorname{MemT}(\operatorname{ExT}\ m)&:\text{ failed memory updates roll back}.
\end{aligned}}
$$
A conventional <programming language> normally retains writes made before an exception is caught. Its mutable <computer memory> and <exception handling> therefore correspond more closely to $\operatorname{ExT}(\operatorname{MemT}\ m)$.
Back to article page
