Thought. State handler [rdn-0001]
Thought. State handler [rdn-0001]
Inference of computation \(\mathtt {plus1}\) using \(\mathtt {state}\) handler. Definition from An Introduction to Algebraic Effects and Handlers. Invited tutorial paper.
Definition of \(\mathtt {state}\).
\[ \begin {align*} \mathtt {state} \stackrel {\mathbf {def}}{=} \mathbf {handler}\,\{ & \mathtt {get}(\_;k) \mapsto {} \mathbf {fun}\; s\mapsto {}(k\;s )\;s \\ & \mathtt {set}(s;k) \mapsto {} \mathbf {fun}\;\_\mapsto {}(k\;())\;s \\ & \mathbf {return}\;x \mapsto {} \mathbf {fun}\;\_\mapsto {}\mathbf {return}\;x \} \end {align*} \]Definition of \(\mathtt {plus1}\).
\[ \begin {align*} \mathtt {plus1} \stackrel {\mathbf {def}}{=} \mathbf {fun}\;() \mapsto {} & \mathbf {do}\; n \gets \mathtt {get} \;()\; \mathbf {in} \\ & \mathtt {set}\;n + 1 \end {align*} \]Usage.
\[ (\mathbf {with}\;\mathtt {state}\;\mathbf {handle}\;\mathtt {plus1})\;41 \]Expansion.
...
Reduce.
\[ \begin {align*} (\mathbf {fun}\;s\mapsto {} (\mathbf {fun}\;\_\mapsto {} & (\mathbf {fun}\;\_\mapsto {} \mathbf {return}\;x)\; (s + 1 ))\; s )\;41 \\ (\mathbf {fun}\;\_\mapsto {} & (\mathbf {fun}\;\_\mapsto {} \mathbf {return}\;x)\; (41 + 1))\; 41 \\ & (\mathbf {fun}\;\_\mapsto {} \mathbf {return}\;x)\; (41 + 1) \\ & (41 + 1) \\ & 42 \end {align*} \]