Try a new syntax for operation cases.

code/unix2.links

@@ -0,0 +1,189 @@
+# Tiny UNIX revision 2.
+
+sig str : ((a, [Char])) ~> (a, String)
+fun str((x, cs)) { (x, implode(cs)) }
+
+##
+## Basic i/o
+##
+typename File = [Char];
+typename FileDescr = Int;
+
+sig stdout : FileDescr
+var stdout = 1;
+
+sig basicIO : (Comp(a, {Putc:(FileDescr,Char) -> () |e})) {Putc{_} |e}~> (a, File)
+fun basicIO(m) {
+  handle(m()) {
+    case Return(res) -> (res, [])
+    case Putc(_, c, resume) ->
+      var (res, file) = resume(());
+      (res, c :: file)
+  }
+}
+
+sig echo : (String) {Putc:(FileDescr,Char) -> () |_}~> ()
+fun echo(cs) { iter(fun(c) { do Putc(stdout, c) }, explode(cs)) }
+
+fun example0() {
+  str(basicIO(fun() {
+        echo("Hello"); echo("World")
+  }))
+}
+
+##
+## Exceptions: non-local exits
+##
+sig exit : (Int) {Exit:(Int) -> Zero |_}-> a
+fun exit(n) { switch(do Exit(n)) {} }
+
+sig status : (Comp(a, {Exit:(Int) -> Zero |e})) {Exit{_} |e}~> Int
+fun status(m) {
+  handle(m()) {
+    case Return(_) -> 0
+    case Exit(n, _) -> n
+  }
+}
+
+fun example1() {
+  str(basicIO(fun() {
+        status(fun() {
+          echo("dead"); exit(1); echo("code")
+        })
+  }))
+}
+
+##
+## Dynamic binding: user-specific environments.
+##
+typename User = [|Alice|Bob|Root|];
+
+sig whoami : () {Ask:String |_}-> String
+fun whoami() { do Ask }
+
+sig env : (User, Comp(a, {Ask:String |e})) {Ask{_} |e}~> a
+fun env(user, m) {
+  handle(m()) {
+    case Return(x) -> x
+    case Ask(resume) ->
+      switch (user) {
+        case Alice -> resume("alice")
+        case Bob   -> resume("bob")
+        case Root  -> resume("root")
+      }
+  }
+}
+
+fun example2() {
+  env(Root, whoami)
+}
+
+###
+### Session management.
+###
+sig su : (User) {Su:(User) -> () |_}-> ()
+fun su(user) { do Su(user) }
+
+sig sessionmgr : (User, Comp(a, {Ask:String,Su:(User) -> () |e})) {Ask{_},Su{_} |e}~> a
+fun sessionmgr(user, m) {
+  env(user, fun() {
+     handle(m()) {
+       case Return(x) -> x
+       case Su(user', resume) ->
+         env(user', fun() { resume(()) })
+     }
+  })
+}
+
+fun example3() {
+  str(basicIO(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            su(Alice); echo(whoami()); echo(" ");
+            su(Bob);   echo(whoami()); echo(" ");
+            su(Root);  echo(whoami())
+          })
+        })
+  }))
+}
+
+##
+## Nondeterminism: time sharing.
+##
+sig fork : () {Fork:Bool |_}-> Bool
+fun fork() { do Fork }
+
+sig nondet : (Comp(a, {Fork:Bool |e})) {Fork{_} |e}~> [a]
+fun nondet(m) {
+  handle(m()) {
+    case Return(res) -> [res]
+    case Fork(resume) -> resume(true) ++ resume(false)
+  }
+}
+
+sig interrupt : () {Interrupt:() |_}-> ()
+fun interrupt() { do Interrupt }
+
+typename Pstate(a,e::Eff) = forall q::Presence.
+                            [|Done:a
+                             |Paused:() {Interrupt{q} |e}~> Pstate(a, { |e})|];
+
+sig slice : (Comp(a, {Interrupt:() |e})) {Interrupt{_} |e}~> Pstate(a, { |e})
+fun slice(m) {
+  handle(m()) {
+    case Return(res) -> Done(res)
+    case Interrupt(resume) -> Paused(fun() { resume(()) })
+  }
+}
+
+sig runNext : ([Pstate(a, { Fork:Bool |e})]) {Fork{_},Interrupt{_} |e}~> [a]
+fun runNext(ps) {
+  sig run : (Pstate (a, { Fork:() {}-> Bool|e })) {Fork{_},Interrupt{_} |e}~> [a]
+  fun run(p) {
+    switch(p) {
+      case Done(res) -> [res]
+      case Paused(resume) -> runNext(nondet(resume))
+    }
+  }
+  concatMap(run, ps)
+}
+
+sig timeshare : (Comp(a, {Fork:Bool,Interrupt:() |e})) {Fork{_},Interrupt{_} |e}~> [a]
+fun timeshare(m) {
+  var p = Paused(fun() { slice(m) });
+  runNext([p])
+}
+
+fun example4() {
+  str(basicIO(fun() {
+        timeshare(fun() {
+          sessionmgr(Root, fun() {
+            status(fun() {
+              var parent = fork();
+              (if (parent) su(Alice) else su(Bob));
+              echo(whoami() ^^ "> Hello ");
+              interrupt();
+              echo(whoami() ^^ "> Bye ");
+              interrupt();
+              if (parent) exit(0)
+              else {
+                var parent = fork();
+                interrupt();
+                (if (parent) su(Root)
+                 else {
+                  echo(whoami() ^^ "> oops ");
+                  exit(1)
+                });
+                echo(whoami() ^^ "> !! ")
+              }
+            })
+          })
+        })
+      }))
+}
+
+##
+## State: file i/o
+##
+
+# TODO.

macros.tex

@@ -1,3 +1,20 @@
+%%
+%% Defined-as equality
+%%
+\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
+\newcommand{\defnas}[0]{\mathrel{:=}}
+\newcommand{\simdefas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{\simeq}}}
+
+%%
+%% Partiality
+%%
+\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}}
+
+%%
+%% Operation arrows
+%%
+\newcommand{\opto}[0]{\ensuremath{\twoheadrightarrow}}
+
 %%
 %% Calculi names.
 %%
@@ -33,6 +50,10 @@
 \newcommand{\Else}{\keyw{else}}
 \newcommand{\Absurd}{\keyw{absurd}}
 \newcommand{\Record}[1]{\ensuremath{\langle #1 \rangle}}
+\newcommand{\Op}[1]{\ensuremath{\langle\!\!\langle #1 \rangle\!\!\rangle}}
+%\newcommand{\Op}[1]{\ensuremath{\{#1\}}}
+\newcommand{\OpCase}[3]{\Op{#1~#2 \opto #3}}
+\newcommand{\ExnCase}[2]{\Op{#1~#2}}
 \newcommand{\Unit}{\Record{}}
 \newcommand{\Inl}{\keyw{inl}}
 \newcommand{\Inr}{\keyw{inr}}
@@ -178,23 +199,6 @@
 
 \newenvironment{smathpar}{\vspace{-3ex}\small\begin{mathpar}}{\end{mathpar}\normalsize\ignorespacesafterend}
 
-%%
-%% Defined-as equality
-%%
-\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
-\newcommand{\defnas}[0]{\mathrel{:=}}
-\newcommand{\simdefas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{\simeq}}}
-
-%%
-%% Partiality
-%%
-\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}}
-
-%%
-%% Operation arrows
-%%
-\newcommand{\opto}[0]{\ensuremath{\twoheadrightarrow}}
-
 %%
 %% Lists
 %%
@@ -354,3 +358,21 @@
 \newcommand{\Su}{\dec{Su}}
 \newcommand{\su}{\dec{su}}
 \newcommand{\sessionmgr}{\dec{sessionmgr}}
+\newcommand{\echo}{\dec{echo}}
+\newcommand{\strlit}[1]{\texttt{"#1"}}
+\newcommand{\nondet}{\dec{nondet}}
+\newcommand{\Fork}{\dec{Fork}}
+\newcommand{\fork}{\dec{fork}}
+\newcommand{\Interrupt}{\dec{Interrupt}}
+\newcommand{\interrupt}{\dec{interrupt}}
+\newcommand{\Pstate}{\dec{Pstate}}
+\newcommand{\Done}{\dec{Done}}
+\newcommand{\Suspended}{\dec{Paused}}
+\newcommand{\slice}{\dec{slice}}
+\newcommand{\timeshare}{\dec{timeshare}}
+\newcommand{\runNext}{\dec{runNext}}
+\newcommand{\concatMap}{\dec{concatMap}}
+\newcommand{\State}{\dec{State}}
+\newcommand{\runState}{\dec{runState}}
+\newcommand{\Uget}{\dec{get}}
+\newcommand{\Uput}{\dec{put}}

thesis.tex

@@ -22,6 +22,7 @@
 \DeclareCaptionFormat{underlinedfigure}{#1#2#3\hrulefill}
 \captionsetup[figure]{format=underlinedfigure}
 \usepackage[T1]{fontenc}      % Fixes issues with accented characters
+\usepackage[scaled=0.85]{beramono}
 %\usepackage{libertine}
 %\usepackage{lmodern}
 %\usepackage{palatino}
@@ -958,7 +959,7 @@ computation to syntactically \emph{appear in tail position}.
       position, then both $M$ and $N$ appear in tail positions.
     \item If $\Let\;\Record{\ell = x; y} = V \;\In\;N$ appears in tail
       position, then $N$ is in tail position.
-    \item If $\Let\;x \revto M\;\In\;N$ appear in tail position, then
+    \item If $\Let\;x \revto M\;\In\;N$ appears in tail position, then
       $N$ appear in tail position.
     \item Nothing else appears in tail position.
   \end{itemize}
@@ -1708,20 +1709,23 @@ no predefined dynamic semantics. The introduction form for effectful
 operations is a computation term.
 %
 \begin{syntax}
-  &M,N \in \CompCat &::=& \cdots \mid~ \tikzmarkin{do1} (\Do \; \ell~V)^E \tikzmarkend{do1}
+  \slab{Value types}             &A,B \in \ValTypeCat   &::=& \cdots \mid~ \tikzmarkin{optype} A \opto B \tikzmarkend{optype}\\
+  \slab{Computations}      &M,N \in \CompCat      &::=& \cdots \mid~ \tikzmarkin{do1} (\Do \; \ell~V)^E \tikzmarkend{do1}
 \end{syntax}
 %
+\dhil{Describe the operation arrow.}
+%
 Informally, the intended behaviour of the new computation term
 $(\Do\; \ell~V)^E$ is that it performs some operation $\ell$ with
 value argument $V$. Thus the $\Do$-construct is similar to the typical
 exception-signalling $\keyw{throw}$ or $\keyw{raise}$ constructs found
 in programming languages with support for exceptions. The term is
 annotated with an effect row $E$, providing a handle to obtain the
-current effect context. We make use of this effect row during typing:
+current effect context. We make use of this effect row during typing.
 %
 \begin{mathpar}
   \inferrule*[Lab=\tylab{Do}]
-    { E = \{\ell : A \to B; R\} \\
+    { E = \{\ell : A \opto B; R\} \\
       \typ{\Delta}{E} \\
       \typ{\Delta;\Gamma}{V : A}
     }
@@ -1780,7 +1784,7 @@ syntactic category of handler definitions.
 \begin{syntax}
 \slab{Computations} &M,N \in \CompCat    &::=& \cdots \mid~ \tikzmarkin{deephandlers1} \Handle \; M \; \With \; H\tikzmarkend{deephandlers1}\\[1ex]
 \slab{Handlers}     &H   \in \HandlerCat &::=&  \{ \Return \; x \mapsto M \}
-                                           \mid \{ \ell \; p \; r \mapsto N \} \uplus H\\
+                                           \mid \{ \OpCase{\ell}{p}{r} \mapsto N \} \uplus H\\
 \slab{Terms}        &t \in \TermCat      &::=& \cdots \mid~ \tikzmarkin{handlerdefs} H \tikzmarkend{handlerdefs}
 \end{syntax}
 %
@@ -1788,14 +1792,14 @@ The handle construct $(\Handle \; M \; \With \; H)$ is the counterpart
 to $\Do$. It runs computation $M$ using handler $H$. A handler $H$
 consists of a return clause $\{\Return \; x \mapsto M\}$ and a
 possibly empty set of operation clauses
-$\{\ell \; p_\ell \; r_\ell \mapsto N_\ell\}_{\ell \in \mathcal{L}}$.
+$\{\OpCase{\ell}{p_\ell}{r_\ell} \mapsto N_\ell\}_{\ell \in \mathcal{L}}$.
 %
 The return clause $\{\Return \; x \mapsto M\}$ defines how to
 interpret the final return value of a handled computation. The
 variable $x$ is bound to the final return value in the body $M$.
 %
 Each operation clause
-$\{\ell \; p_\ell \; r_\ell \mapsto N_\ell\}_{\ell \in \mathcal{L}}$
+$\{\OpCase{\ell}{p_\ell}{r_\ell} \mapsto N_\ell\}_{\ell \in \mathcal{L}}$
 defines how to interpret an invocation of a particular operation
 $\ell$. The variables $p_\ell$ and $r_\ell$ are bound in the body
 $N_\ell$: $p_\ell$ binds the argument carried by the operation and
@@ -1806,7 +1810,7 @@ particular operation or the return clause; for these purposes we
 define two convenient projections on handlers in the metalanguage.
 \[
   \ba{@{~}r@{~}c@{~}l@{~}l}
-    \hell &\defas& \{\ell\; p\; r \mapsto N \}, &\quad \text{where } \{\ell\; p\; r \mapsto N \} \in H\\
+    \hell &\defas& \{\OpCase{\ell}{p}{r} \mapsto N \}, &\quad \text{where } \{\OpCase{\ell}{p}{r} \mapsto N \} \in H\\
     \hret &\defas& \{\Return\; x \mapsto N \}, &\quad \text{where } \{\Return\; x \mapsto N \} \in H\\
   \ea
 \]
@@ -1821,7 +1825,7 @@ labels it handles, i.e.
 \begin{equations}
   \dom &:& \HandlerCat \to \LabelCat\\
   \dom(\{\Return\;x \mapsto M\})  &\defas& \emptyset\\
-  \dom(\{\ell\; p\;r \mapsto M\} \uplus H) &\defas& \{\ell\} \cup \dom(H)
+  \dom(\{\OpCase{\ell}{p}{r} \mapsto M\} \uplus H) &\defas& \{\ell\} \cup \dom(H)
 \end{equations}
 
 \subsection{Static semantics}
@@ -1841,9 +1845,9 @@ typing of the $\Do$-construct.
 %\mprset{flushleft}
   \inferrule*[Lab=\tylab{Handler}]
     {{\bl
-       C = A \eff \{(\ell_i : A_i \to B_i)_i; R\} \\
+       C = A \eff \{(\ell_i : A_i \opto B_i)_i; R\} \\
        D = B \eff \{(\ell_i : P_i)_i;           R\}\\
-       H = \{\Return\;x \mapsto M\} \uplus \{ \ell_i\;p_i\;r_i \mapsto N_i \}_i
+       H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i
        \el}\\\\
        \typ{\Delta;\Gamma, x : A}{M : D}\\\\
        [\typ{\Delta;\Gamma,p_i : A_i, r_i : B_i \to D}{N_i : D}]_i
@@ -1878,7 +1882,7 @@ for handling return values and another for handling operations.
     &\reducesto& N[V/p, \lambda y . \, \Handle \; \EC[\Return \; y] \; \With \; H/r], \\
 \multicolumn{4}{@{}r@{}}{
        \hfill\ba[t]{@{~}r@{~}l}
-                   \text{where}& \hell = \{ \ell \; p \; r \mapsto N \}\\
+                   \text{where}& \hell = \{ \OpCase{\ell}{p}{r} \mapsto N \}\\
                    \text{and}  & \ell \notin \BL(\EC)
               \ea
 }
@@ -1911,8 +1915,8 @@ $\ell$.
 \[
   \bl
     \ba{@{~}r@{~}c@{~}l}
-        H_{\mathsf{inner}}   &\defas& \{\ell\;p\;r \mapsto r~42; \Return\;x \mapsto \Return~x\}\\
-        H_{\mathsf{outer}} &\defas& \{\ell\;p\;r \mapsto r~0;\Return\;x \mapsto \Return~x \}
+        H_{\mathsf{inner}}   &\defas& \{\OpCase{\ell}{p}{r} \mapsto r~42; \Return\;x \mapsto \Return~x\}\\
+        H_{\mathsf{outer}} &\defas& \{\OpCase{\ell}{p}{r} \mapsto r~0;\Return\;x \mapsto \Return~x \}
     \ea\medskip\\
       \Handle \;
         \left(\Handle\; \Do\;\ell~\Record{}\;\With\; H_{\mathsf{inner}}\right)\;
@@ -2044,7 +2048,7 @@ Section~\ref{sec:tiny-unix-io}.
 Much like UNIX we shall model a file as a list of characters, that is
 $\UFile \defas \List~\Char$. For convenience we will use the same
 model for strings, $\String \defas \List~\Char$, such that we can use
-string literal notation to denote the $\texttt{"contents of a file"}$.
+string literal notation to denote the $\strlit{contents of a file}$.
 %
 The signature of the basic file system will consist of a single
 operation $\Putc$ for writing a single character to the file.
@@ -2069,7 +2073,7 @@ Let us define a suitable handler for this operation.
          \Handle\;m\,\Unit\;\With\\
            ~\ba{@{~}l@{~}c@{~}l}
               \Return\;res &\mapsto& \Record{res;\nil}\\
-              \Putc~\Record{\_;c}~resume &\mapsto&
+              \OpCase{\Putc}{\Record{\_;c}}{resume} &\mapsto&
                   \Let\; \Record{res;file} = resume\,\Unit\;\In\;
                   \Record{res; c \cons file}
            \ea
@@ -2087,7 +2091,7 @@ The $\Return$-case pairs the result $res$ with the empty file $\nil$
 which models the scenario where the computation $m$ performed no
 $\Putc$-operations, e.g.
 $\basicIO\,(\lambda\Unit.\Unit) \reducesto^+
-\Record{\Unit;\texttt{""}}$.
+\Record{\Unit;\strlit{}}$.
 %
 The $\Putc$-case extends the file by first invoking the resumption,
 whose return type is the same as the handler's return type, thus it
@@ -2101,20 +2105,20 @@ file.
 %
 \[
   \bl
-    \fwrite : \Record{\UFD;\String} \to \UnitType \eff \{\Putc : \Record{\UFD;\Char} \opto \UnitType\}\\
-    \fwrite~\Record{fd;cs} \defas \iter\,(\lambda c.\Do\;\Putc\,\Record{fd;c})\,cs
+    \echo : \String \to \UnitType \eff \{\Putc : \Record{\UFD;\Char} \opto \UnitType\}\\
+    \echo~cs \defas \iter\,(\lambda c.\Do\;\Putc\,\Record{\stdout;c})\,cs
   \el
 \]
 %
-The function $\fwrite$ invokes the operation $\Putc$ point-wise on the
+The function $\echo$ invokes the operation $\Putc$ point-wise on the
 list of characters $cs$ by using the list iteration function $\iter$.
 %
 We can now write some contents to the file and observe the effects.
 %
 \[
   \ba{@{~}l@{~}l}
-                &\basicIO\,(\lambda\Unit. \fwrite\,\Record{\stdout;\texttt{"Hello"}}; \fwrite\,\Record{\stdout;\texttt{"World"}})\\
-    \reducesto^+& \Record{\Unit;\texttt{"HelloWorld"}} : \Record{\UnitType;\UFile}
+                &\basicIO\,(\lambda\Unit. \echo~\strlit{Hello}; \echo~\strlit{World})\\
+    \reducesto^+& \Record{\Unit;\strlit{HelloWorld}} : \Record{\UnitType;\UFile}
   \ea
 \]
 
@@ -2140,7 +2144,7 @@ We can now write some contents to the file and observe the effects.
          \Handle\;m\,\Unit\;\With\\
            ~\ba{@{~}l@{~}c@{~}l}
               \Return\;\_ &\mapsto& 0\\
-              \Exit~n~\_ &\mapsto& n
+              \ExnCase{\Exit}{n} &\mapsto& n
            \ea
        \ea
   \el
@@ -2151,9 +2155,9 @@ We can now write some contents to the file and observe the effects.
     &\bl
       \basicIO\,(\lambda\Unit.
          \status\,(\lambda\Unit.
-            \fwrite\,\Record{\stdout;\texttt{"dead"}};\exit~1;\fwrite\,\Record{\stdout;\texttt{"code"}}))
+            \echo~\strlit{dead};\exit~1;\echo~\strlit{code}))
      \el\\
-    \reducesto^+& \Record{1;\texttt{"dead"}} : \Record{\Int;\UFile}
+    \reducesto^+& \Record{1;\strlit{dead}} : \Record{\Int;\UFile}
   \ea
 \]
 
@@ -2212,13 +2216,13 @@ The following handler implements the environment.
          \Handle\;m\,\Unit\;\With\\
            ~\ba{@{~}l@{~}c@{~}l}
               \Return\;res &\mapsto& res\\
-              \Ask~\Unit~resume &\mapsto&
+              \OpCase{\Ask}{\Unit}{resume} &\mapsto&
                 \bl
                   \Case\;user\,\{
                   \ba[t]{@{}l@{~}c@{~}l}
-                    \Alice &\mapsto& resume~\texttt{"alice"}\\
-                    \Bob   &\mapsto& resume~\texttt{"bob"}\\
-                    \Root  &\mapsto& resume~\texttt{"root"}\}
+                    \Alice &\mapsto& resume~\strlit{alice}\\
+                    \Bob   &\mapsto& resume~\strlit{bob}\\
+                    \Root  &\mapsto& resume~\strlit{root}\}
                    \ea
                 \el
            \ea
@@ -2233,7 +2237,7 @@ string representation of the user. With this implementation we can
 interpret an application of $\whoami$.
 %
 \[
-  \environment~\Record{\Root;\whoami} \reducesto^+ \texttt{"root"} : \String
+  \environment~\Record{\Root;\whoami} \reducesto^+ \strlit{root} : \String
 \]
 %
 It is not difficult to extend this basic environment model to support
@@ -2266,7 +2270,7 @@ string.
            \Handle\;m\,\Unit\;\With\\
              ~\ba{@{~}l@{~}c@{~}l}
                 \Return\;res &\mapsto& res\\
-                \Su~user'~resume &\mapsto& \environment\,\Record{user';resume})\rangle
+                \OpCase{\Su}{user'}{resume} &\mapsto& \environment\,\Record{user';resume})\rangle
               \ea
          \ea
   \el
@@ -2279,20 +2283,124 @@ string.
          \qquad\sessionmgr\,\Record{\Root;\lambda\Unit.\\
            \qquad\qquad\status\,(\lambda\Unit.
             \ba[t]{@{}l@{~}l}
-              \su~\Alice;&\fwrite\,\Record{\stdout;\whoami\,\Unit};~\fwrite\,\Record{\stdout;\texttt{" "}};\\
-              \su~\Bob;&\fwrite\,\Record{\stdout;\whoami\,\Unit};~\fwrite\,\Record{\stdout;\texttt{" "}};\\
-              \su~\Root;&\fwrite\,\Record{\stdout;\whoami\,\Unit})})
+              \su~\Alice;&\echo\,(\whoami\,\Unit);~\echo~\strlit{ };\\
+              \su~\Bob;  &\echo\,(\whoami\,\Unit);~\echo~\strlit{ };\\
+              \su~\Root; &\echo\,(\whoami\,\Unit))})
             \ea
      \el \smallskip\\
-   \reducesto^+& \Record{0;\texttt{"alice bob root"}} : \Record{\Int;\UFile}
+   \reducesto^+& \Record{0;\strlit{alice bob root}} : \Record{\Int;\UFile}
  \ea
 \]
 \subsection{Nondeterminism: time sharing}
 \label{sec:tiny-unix-time}
 
+\[
+  \bl
+    \fork : \UnitType \to \Bool \eff \{\Fork : \UnitType \opto \Bool\}\\
+    \fork~\Unit \defas \Do\;\Fork~\Unit
+  \el
+\]
+
+\[
+  \bl
+    \nondet : (\UnitType \to \alpha \eff \{\Fork:\UnitType \opto \Bool\}) \to \List~\alpha\\
+    \nondet~m \defas
+         \ba[t]{@{}l}
+           \Handle\;m\,\Unit\;\With\\
+             ~\ba{@{~}l@{~}c@{~}l}
+                \Return\;res &\mapsto& [res]\\
+                \OpCase{\Fork}{\Unit}{resume} &\mapsto& resume~\True \concat resume~\False
+              \ea
+         \ea
+  \el
+\]
+
+\[
+  \bl
+    \interrupt : \UnitType \to \UnitType \eff \{\Interrupt : \UnitType \opto \UnitType\}\\
+    \interrupt~\Unit \defas \Do\;\Interrupt~\Unit
+  \el
+\]
+
+\[
+  \Pstate~\alpha~\varepsilon \defas \forall \theta.
+     \ba[t]{@{}l@{}l}
+       [&\Done:\alpha;\\
+        &\Suspended:\UnitType \to \Pstate~\alpha~\varepsilon \eff \{\Interrupt:\theta';\varepsilon\} ]
+     \ea
+\]
+
+\[
+  \bl
+    \slice : (\UnitType \to \alpha \eff \{\Interrupt:\UnitType \opto \UnitType;\varepsilon\}) \to \Pstate~\alpha~\varepsilon\\
+    \slice~m \defas
+         \ba[t]{@{}l}
+           \Handle\;m\,\Unit\;\With\\
+             ~\ba{@{~}l@{~}c@{~}l}
+                \Return\;res &\mapsto& \Done~res\\
+                \OpCase{\Interrupt}{\Unit}{resume} &\mapsto& \Suspended~resume
+              \ea
+         \ea
+  \el
+\]
+
+\[
+  \bl
+    \runNext : \List~(\Pstate~\alpha~\{\Fork:\Bool;\varepsilon\}) \to \List~\alpha \eff \varepsilon\\
+    \runNext~ps \defas
+        \concatMap\,(\lambda p.
+               \ba[t]{@{}l}
+                  \Case\;p\;\{
+                    \ba[t]{@{}l@{~}c@{~}l}
+                       \Done~res         &\mapsto& [res]\\
+                       \Suspended~m &\mapsto& \runNext\,(\nondet~m) \})\,ps
+                    \ea
+                \ea
+  \el
+\]
+
+\[
+  \bl
+     \timeshare : (\UnitType \to \alpha \eff \{\Fork:\UnitType \opto \Bool;\Interrupt:\UnitType \opto \UnitType;\epsilon\}) \to (\List~\alpha) \eff \epsilon\\
+     \timeshare~m \defas \runNext\,[\Suspended\,(\lambda\Unit.\slice~m)]
+  \el
+\]
+
 \subsection{State: file i/o}
 \label{sec:tiny-unix-io}
 
+\[
+  \State~\alpha \defas \{\Get:\UnitType \opto \alpha;\Put:\alpha \opto \UnitType\}
+\]
+
+\[
+  \bl
+    \Uget : \UnitType \to \alpha \eff \{\Get:\UnitType \opto \alpha\}\\
+    \Uget~\Unit \defas \Do\;\Get~\Unit \medskip\\
+
+    \Uput : \UnitType \to \alpha \eff \{\Put:\alpha \opto \Unit\}\\
+    \Uput~st \defas \Do\;\Put~st
+  \el
+\]
+
+\[
+  \bl
+    \runState : \Record{\beta;\UnitType \to \alpha \eff \State~\beta} \to \Record{\alpha;\beta}\\
+    \runState~\Record{st_0;m} \defas
+        \ba[t]{@{}l}
+           \Let\;f \revto
+              \ba[t]{@{}l}
+                \Handle\;m\,\Unit\;\With\\
+                 ~\ba{@{~}l@{~}c@{~}l}
+                   \Return\;res      &\mapsto& \lambda st.\Record{res;st}\\
+                   \OpCase{\Get}{\Unit}{resume} &\mapsto& \lambda st.resume~st~st\\
+                   \OpCase{\Put}{st'}{resume}   &\mapsto& \lambda st.resume~\Unit~st'
+                  \ea
+              \ea\\
+           \In\; f\,st_0
+        \ea
+  \el
+\]
 
 % The existing literature already contain an extensive amount of
 % introductory examples of programming with (deep) effect