notes.tex

\documentclass{article}

\usepackage[T1]{fontenc}
\usepackage[margin=1in]{geometry}
\usepackage{palatino}
\usepackage{amsthm,amsmath,amssymb}
\usepackage{xcolor}
\usepackage[utf8]{inputenc}
\usepackage[colorlinks=true,urlcolor=blue]{hyperref}
\usepackage{listings}
\newcommand{\task}{\par\noindent\emph{Task:}\ }

\definecolor{darkblue}{rgb}{0,0,0.5}
\definecolor{lightgray}{gray}{0.75}

\lstset{basicstyle=\ttfamily\small, numbers=left,
  xleftmargin=3em,extendedchars=true,
  numberstyle=\tiny\color{lightgray}, keywordstyle=\color{darkblue}, morekeywords={and,
    as, begin, check, do, done, downto, else, end, effect, external, finally,
    for, fun, function, handle, handler, if, in, match, let, new, of, operation,
    perform, rec, val, while, to, type, then, with},
literate=%
    {→}{{$\rightarrow$}}1%
    {×}{{$\times$}}1%
    {←}{{$\leftarrow$}}1%
    {↦}{{$\mapsto$}}1%
    {↝}{{$\leadsto$}}1%
    {…}{{$\ldots$}}1%
    {⇒}{{$\Rightarrow$}}1%
    {∈}{{$\in$}}1%
    {≡}{{$\equiv$}}1%
    {λ}{{$\lambda$}}1%
    {⊢}{{$\vdash$}}1%
    {κ}{{$\kappa$}}1%
    {Σ}{{$\Sigma$}}1%
    {Δ}{{$\Delta$}}1%
    {Γ}{{$\Gamma$}}1%
    {Θ}{{$\Theta$}}1%
    {₀}{{${}_0$}}1%
    {₁}{{${}_1$}}1%
    {₂}{{${}_2$}}1%
    {ᵢ}{{${}_\mathtt{i}$}}1%
    {ⱼ}{{${}_\mathtt{j}$}}1%
}

{\theoremstyle{definition}
\newtheorem{problem}{Problem}[section]}


\begin{document}
\title{Algebraic effects and handlers\\(OPLSS 2018 lecture notes)}
\author{Andrej Bauer\\University of Ljubljana}
\date{July 2018}

\maketitle

These are the notes and materials for the lectures on algebraic effects and
handlers at the
\href{https://www.cs.uoregon.edu/research/summerschool/summer18/index.php}{Oregon
  programming languages summer school 2018 (OPLSS)}. The notes were originally
written in Markdown and converted to {\LaTeX} semi-automatically, please excuse
strange formatting. You can find all the resources at
\href{https://github.com/OPLSS/introduction-to-algebraic-effects-and-handlers}{the
  accompanying GitHub repository}.

The lectures were recorded on video that are available at the summer school web
site.

\hypertarget{general-resources-reading-material}{%
\subsubsection*{General resources \& reading
material}\label{general-resources-reading-material}}

\begin{itemize}
\item
  \href{https://github.com/yallop/effects-bibliography}{Effects
  bibliography}
\item
  \href{https://github.com/effect-handlers/effects-rosetta-stone}{Effects
  Rosetta Stone}
\item
  \href{http://www.eff-lang.org}{Programming language Eff}
\end{itemize}

\hypertarget{what-is-algebraic-about-algebraic-effects-and-handlers}{%
\section{What is algebraic about algebraic effects and
handlers?}\label{what-is-algebraic-about-algebraic-effects-and-handlers}}

The purpose of the first two lectures is to review algebraic theories and
related concepts, and connect them with computational effects. We shall start on
the mathematical side of things and gradually derive from it a programming
language.

\hypertarget{outline}{%
\subsubsection*{Outline}\label{outline}}

Pretty much everything that will be said in the first two lectures is written
up in \href{https://arxiv.org/abs/1807.05923}{``What is algebraic about
algebraic effects and handlers?''}, which still a bit rough around the
edges, so if you see a typo please
\href{https://github.com/andrejbauer/what-is-algebraic-about-algebraic-effects}{let
me know}.

Contents of the first two lectures:
%
\begin{itemize}
\item
  signatures, terms, and algebraic theories
\item
  models of an algebraic theory
\item
  free models of an algebraic theory
\item
  generalization to parameterized operations with arbitrary arities
\item
  sequencing and generic operations
\item
  handlers
\item
  comodels and tensoring of comodels and models
\end{itemize}

\hypertarget{problems}{%
\subsection{Problems}\label{problems}}

Each section contains a list of problems, which are ordered roughly in the order
of difficulty, either in terms of trickiness, the amount of work, or
prerequisites. I recommend that you discuss the problems in groups, and pick
whichever problems you find interesting.

\begin{problem}[The theory of an associative unital operation]
Consider the theory $T$ of an associative operation with a unit.
It has a constant $\epsilon$ and a binary operation $\cdot$
satisfying equations
%
\begin{align*}
(x \cdot y) \cdot z &= x \cdot (y \cdot z) \\
\epsilon \cdot x &= x \\
x \cdot \epsilon &= x
\end{align*}
%
Give a useful description of the free model of $T$ generated by a
set $X$. You can either guess an explicit construction of free
models and show that it has the required universal property, or you can
analyze the free model construction (equivalence classes of well-founded
trees) and provide a simple description of it.
\end{problem}

\begin{problem}[The theory of apocalypse]
We formulate an algebraic theory $\mathsf{Time}$ in it is possible to
explicitly record passage of time. The theory has a single unary
operation $\mathsf{tick}$ and no equations. Each application of
$\mathsf{tick}$ records the passage of one time step.

\task Give a useful description of the free model of the
theory, generated by a set $X$.

\task Let a given fixed natural number $n$ be given.
Describe a theory $\mathsf{Apocalypse}$ which extends the theory
$\mathsf{Time}$ so that a computation crashes (aborts, necessarily
terminates) if it performs more than $n$ of ticks. Give a useful
description of its free models.

Advice: do \emph{not} concern yourself with any sort of operational
semantics which somehow ``aborts'' after $n$ ticks. Instead, use
equations and postulate that certain computations are equal to an
aborted one.
\end{problem}

\begin{problem}[The theory of partial maps]

The models of the empty theory are precisely sets and functions. Is
there a theory whose models form (a category equivalent to) the category
of sets and \emph{partial} functions?

Recall that a partial function $f : A \hookrightarrow B$ is an ordinary
function $f : S \to B$ defined on a subset $S \subseteq A$.
(How do we define composition of partial functions?)
\end{problem}

\begin{problem}[Models in the category of models]

In \href{https://arxiv.org/abs/1807.05923}{Example 1.27 of the reading
material} it is calculated that a model of the theory $\mathsf{Group}$ in
the category $\mathsf{Mod}(\textsf{Group})$ is an abelian group. We may generalize
this idea and ask about models of theory $T_1$ in the category of
models $\mathsf{Mod}(T_2)$ of theory $T_2$.

The \textbf{tensor product $T_1 \otimes T_2$} of algebraic theories
$T_1$ and $T_2$ is a theory such that the category of models
of $T_1$ in the category $\mathsf{Mod}(T_2)$ is equivalent to the
category of models of $T_1 \otimes T_2$.

Hint: start by outlining what data is needed to have a $T_1$-model
in $\mathsf{Mod}(T_2)$ is, and pay attention to the fact that the
operations of $T_1$ must be interpreted as
$T_2$-homomorphisms. That will tell you what the ingredients of
$T_1 \otimes T_2$ should be.
\end{problem}

\subsubsection{Problem: Morita equivalence}

It may happen that two theories $T_1$ and $T_2$ have
equivalent categories of models, i.e.,
%
\begin{equation*}
\mathsf{Mod}(T_1) \simeq \mathsf{Mod}(T_2)
\end{equation*}
%
In such a case we say that $T_1$ and $T_2$ are
\textbf{Morita equivalent}.

Let $T$ be an algebraic theory and $t$ a term in context
$x_1, \ldots, x_i$. Define a \textbf{definitional extension
$T + (\mathsf{op} {{:}{=}} t)$} to be the theory $T$ extended with an
additional operation $\mathsf{op}$ and equation
%
\begin{equation*}
x_1, \ldots, x_i \mid \mathsf{op}(x_1, \ldots, x_i) = t
\end{equation*}
%
We say that $\mathsf{op}$ is a \textbf{defined operation}.
%
\task Confirm the intuitive feeling that
$T + (\mathsf{op} {{:}{=}} t)$ by proving that $T$ and
$T + (\mathsf{op} {{:}{=}} t)$ are Morita equivalent.

\task Formulate the idea of a definitional extension so that
we allow an arbitrary set of defined operations, and show that we still
have Morita equivalence.

\begin{problem}[The theory of a given set]
Given any set $A$, define the \textbf{theory $T(A)$ of the set $A$} as follows:
%
\begin{itemize}
\item
  for every $n$ and every map $f : A^n \to A$,
  $\mathsf{op}(f)$ is an $n$-ary operation
\item
  for all $f : A^i \to A$, $g : A^j \to A$ and
  $h_1, \ldots, h_i : A^j \to A$, if
  %
  \begin{equation*}
    f \circ (h_1, \ldots, h_i) = g
  \end{equation*}
  %
  then we have an equation
  %
  \begin{equation*}
    x_1, \ldots, x_j \mid \mathsf{op}(f)(\mathsf{op}(h_1)(x_1,\ldots,x_j), \ldots, h_i(x_1,\ldots,x_j)) = g(x_1, \ldots, x_j)
  \end{equation*}
\end{itemize}

\task Is $T(\{0,1\})$ Morita equivalent to another, well-known algebraic theory?
\end{problem}

\begin{problem}[A comodel for non-determinism]
  In \href{https://arxiv.org/abs/1807.05923}{Example 4.6 of the reading
    material} it is shown that there is no comodel of non-determinism in the
  category of sets. Can you suggest a category in which we get a reasonable
  comodel of non-determinism?
\end{problem}

\begin{problem}[Formalization of algebraic theories]

If you prefer avoiding doing Real Math, you can formalize algebraic
theories and their comodels in your favorite proof assistant. A possible
starting point is
\href{https://gist.github.com/andrejbauer/3cc438ab38646516e5e9278fdb22022c}{this
gist}, and a good goal is the construction of the free model of a theory
generated by a set (or a type).

Because the free model requires quotienting, you should think ahead on
how you are going to do that. Some possibilities are:
%
\begin{itemize}
\item
  use homotopy type theory and make sure that the types involved are
  h-Sets
\item
  use setoids
\item
  suggest your own solution
\end{itemize}
%
It may be wiser to first show as a warm-up exercise that theories
without equations have initial models, as that only requires the
construction of well-founded trees (which are inductive types).
\end{problem}

\section{Designing a programming language}

Having worked out algebraic theories in previous lectures, let us turn the
equational theories into a small programming language.

What we have to do:
%
\begin{enumerate}
\item Change mathematical terminology to one that is familiar to programmers.
\item Reuse existing concepts (generators, operations, trees) to set up the overall
   structure of the language.
\item Add missing features, such as primitive types and recursion, and generally
   rearrange things a bit to make everything look nicer.
\item Provide operational semantics.
\item Provide typing rules.
\end{enumerate}

\subsection{Reading material}

There are many possible ways and choices of designing a programming language
around algebraic operations and handlers, but we shall mostly rely on Matija
Pretnar's tutorial \href{http://www.eff-lang.org/handlers-tutorial.pdf}{An
  Introduction to Algebraic Effects and Handlers. Invited tutorial paper}. A
more advanced treatment is available in
\href{https://arxiv.org/abs/1306.6316}{An effect system for algebraic effects
  and handlers}.

\subsection{Change of terminology}

\begin{itemize}
\item The elements of $\mathsf{Free}_\Sigma(V)$ are  are \textbf{computations} (instead of trees).
\item The elements of $V$ are \textbf{values} (instead of generators).
\item We speak of \textbf{value types} (instead of sets of generators).
\item We speak of \textbf{computation type} (instead of free models).
\end{itemize}

Henceforth we ignore equations.

\subsection{Abstract syntax}

We add only one primitive type, namely $\mathsf{bool}$. Other constructs
(integers, products, sums) are left as exercises.

\noindent
Value:
%
\begin{lstlisting}
v ::= x              (variable)
    | false          (boolean constants)
    | true
    | h              (handler)
    | λ x . c        (function)
\end{lstlisting}
%
Handler:
%
\begin{lstlisting}
h ::= handler { return x ↦ c_ret, ... opᵢ(x, κ) ↦ cᵢ, ... }
\end{lstlisting}
%
Computation:
%
\begin{lstlisting}
c ::= return v               (pure computation)
    | if v then c₁ else c₂   (conditional)
    | v₁ v₂                  (application)
    | with v handle c        (handling)
    | do x ← c₁ in c₂        (sequencing)
    | op (v, λ x . c)        (operation call)
    | fix x . c              (fixed point)
\end{lstlisting}
%
We introduce \textbf{generic operations} as syntactic abbreviation and let
$\mathsf{op}\;v$ stand for $\mathsf{op}(v, \lambda x . \mathsf{return}\; x)$.

\subsection{Operational semantics}

We provide small-step semantics, but big step semantics can also be given (see
reading material). In the rules below \lstinline{h} stands for
%
\begin{lstlisting}
handler { return x ↦ c_ret, ... opᵢ(x,y) ↦ cᵢ, ... }
\end{lstlisting}
%
We write \lstinline{e₁[e₂/x]} for \lstinline{e₁} with \lstinline{e₂} substituted
for \lstinline{x}. The operational rules are:
%
\begin{lstlisting}
________________________________
(if true then c₁ else c₂)  ↦  c₁

_________________________________
(if false then c₁ else c₂)  ↦  c₂

______________________
(λ x . c) v  ↦  c[v/x]

_____________________________________
with h handle return v  ↦  c_ret[v/x]

_____________________________________________________________
with h handle opᵢ(v,κ)  ↦  cᵢ[v/x, (λ x . with h handle κ x)/y]

_________________________________
do x ← return v in c₂  ↦  c₂[v/x]

_______________________________________________________
do x ← op(v, κ) in c₂  ↦  op(v, λ y . do x ← κ y in c₂)

______________________________
fix x . c  ↦  c[(fix x . c)/x]
\end{lstlisting}

\subsection{Effect system}

\subsubsection{Value and computation types}

Value type:
%
\begin{lstlisting}
A, B := bool | A → C | C ⇒ D
\end{lstlisting}
%
Computation type:
%
\begin{lstlisting}
C, D := A!Δ
\end{lstlisting}
%
Dirt:
%
\begin{lstlisting}
Δ ::= {op₁, …, opⱼ}
\end{lstlisting}
%
The idea is that a computation which returns values of type \lstinline{A} and
\emph{may} perform operations \lstinline{op₁, …, opⱼ} has the computation type
\lstinline|A!{op₁, …, opⱼ}|.

\subsubsection{Signature}

We presume that some way of declaring operations is given, i.e., that we have a
signature \lstinline{Σ} which lists operations with their parameters and
arities:
%
\begin{lstlisting}
Σ = { …, opᵢ : Aᵢ ↝ Bᵢ, … }
\end{lstlisting}
%
Note that the the parameter and the arity types \lstinline{Aᵢ} and
\lstinline{Bᵢ} are both value types.

\subsubsection{Typing rules}

A typing context assigns value types to free variables:
%
\begin{lstlisting}
Γ ::= x₁:A₁, …, xᵢ:Aᵢ
\end{lstlisting}
%
We think of \lstinline{Γ} as a map which takes variables to their types.

There are two forms of typing judgment:
%
\begin{enumerate}
\item \lstinline{Γ ⊢ v : A} -- value \lstinline{v} has value type \lstinline{A} in context \lstinline{Γ}
\item \lstinline{Γ ⊢ c : C} -- computation \lstinline{c} has computation type \lstinline{C} in context \lstinline{Γ}
\end{enumerate}

Rules for value typing:
%
\begin{lstlisting}
Γ(x) = A
_________
Γ ⊢ x : A

________________
Γ ⊢ false : bool

________________
Γ ⊢ true : bool

Γ, x : A ⊢ c_ret : B!Θ
Γ, x : Pᵢ, κ : Aᵢ → B!Θ ⊢ cᵢ : B!Θ  (for each opᵢ : Pᵢ ↝ Aᵢ in Δ)
_______________________________________________________________________
Γ ⊢ (handler { return x ↦ c_ret, ... opᵢ(x) κ ↦ cᵢ, ... }) : A!Δ ⇒ B!Θ

   Γ, x:A ⊢ c : C
_____________________
Γ ⊢ (λ x . c) : A → C
\end{lstlisting}
%
Rules for computation typing:
%
\begin{lstlisting}
    Γ ⊢ v : A
__________________
Γ ⊢ return v : A!Δ

Γ ⊢ v : bool    Γ ⊢ c₁ : C    Γ ⊢ c₂ : C
________________________________________
    Γ ⊢ (if v then c₁ else c₂) : C

Γ ⊢ v₁ : A → C    Γ ⊢ v₂ : A
____________________________
   Γ ⊢ v₁ v₂ : C

Γ ⊢ v : C ⇒ D     Γ ⊢ c : C
___________________________
 Γ ⊢ (with v handle c) : D

Γ ⊢ c₁ : A!Δ    Γ, x:A ⊢ c₂ : B!Δ
_________________________________
  Γ ⊢ (do x ← c₁ in c₂) : B!Δ

Γ ⊢ v : Aᵢ    opᵢ ∈ Δ    opᵢ : Aᵢ ↝ Bᵢ
___________________________________
        Γ ⊢ op v : Bᵢ!Δ

 Γ, x:A ⊢ c : A!Δ
_____________________
Γ ⊢ (fix x . c) : A!Δ
\end{lstlisting}

\subsection{Safety theorem}

If \lstinline{⊢ c : A!Δ} then:
%
\begin{enumerate}
\item \lstinline{c = return v} for some \lstinline{⊢ v : A} \emph{or}
\item \lstinline{c = op(v, κ)} for some \lstinline{op ∈ Δ} and some value \lstinline{v} and continuation \lstinline{κ}, \emph{or}
\item \lstinline{c ↦ c'} for some \lstinline{⊢ c' : A!Δ}.
\end{enumerate}
%
For a mechanized proof see \href{https://arxiv.org/abs/1306.6316}{An effect
  system for algebraic effects and handlers}.


\subsection{Other considerations}

The effect system suffers from the so-called \emph{poisoning}, which can be
resolved if we introduce \textbf{effect subtyping}. Recursion requires that we
use domain-theoretic denotational semantics. Such a semantics turns out to be
adequate (but not fully abstract for the same reasons that domain theory is not
fully abstract for PCF). See \href{https://arxiv.org/abs/1306.6316}{An effect
  system for algebraic effects and handlers} where the above points are treated
carefully.

\subsubsection{Problems}

\begin{problem}[Products]

Add simple products \lstinline{A × B} to the core language:
%
\begin{enumerate}
\item Extend the syntax of values with pairs.
\item Extend the syntax of computations with an elimination of pairs, e.g., \lstinline{do (x,y) ← c₁ in c₂}.
\item Extend the operational semantics.
\item Extend the typing rules.
\end{enumerate}
\end{problem}

\begin{problem}[Sums]

Add simple sums \lstinline{A + B} to the core language:
%
\begin{enumerate}
\item Extend the syntax of values with injections.
\item Extend the syntax of computations with an elimination of sums (a suitable \lstinline{match} statement).
\item Extend the operational semantics.
\item Extend the typing rules.
\end{enumerate}
\end{problem}

\begin{problem}[\lstinline{empty} and \lstinline{unit} types]
Add the \lstinline{empty} and \lstinline{unit} types to the core language. Follow the same steps as
in the previous exercises.
\end{problem}

\begin{problem}[Non-terminating program]
Define a program which prints infinitely many booleans. You may assume that the
\lstinline{print : bool → unit} operation is handled appropriately by the runtime
environment. For extra credit, make it "funny".
\end{problem}

\begin{problem}[Implementation]
Implement the core language from Matija Pretnar's
\href{http://www.eff-lang.org/handlers-tutorial.pdf}{tutorial}. To make it
interesting, augment it with recursive function definitions, integers, and
product types. Consider implementing the language as part of the \href{http://plzoo.andrej.com}{Programming
Languages Zoo}.
\end{problem}


\hypertarget{programming-with-algebraic-effects-and-handlers}{%
\section{Programming with algebraic effects and
handlers}\label{programming-with-algebraic-effects-and-handlers}}

In the last lecture we shall explore how algebraic operations and
handlers can be used in programming.

\hypertarget{eff}{%
\subsection{Eff}\label{eff}}

There are several languages that support algebraic effects and handlers.
The ones most faithful to the theory of algebraic effects are
\href{http://www.eff-lang.org}{Eff} and the
\href{https://github.com/ocamllabs/ocaml-multicore}{multicore OCaml}.
They have very similar syntax, and we could use either, but let us use
Eff, just because it was the first language with algebraic effects and
handlers.

You can \href{http://www.eff-lang.org/try/}{run Eff in your browser} or
\href{https://github.com/matijapretnar/eff/\#installation--usage}{install
it} locally. The page also has a quick overview of the syntax of Eff,
which mimics the syntax of OCaml.

\hypertarget{reading-material-1}{%
\subsection{Reading material}\label{reading-material-1}}

We shall draw on examples from
\href{http://www.eff-lang.org/handlers-tutorial.pdf}{An introduction to
algebraic effects and handlers} and
\href{https://arxiv.org/abs/1203.1539}{Programming with algebraic
effects and handlers}. Some examples can be seen also at the
\href{https://github.com/effect-handlers/effects-rosetta-stone}{Effects
Rosetta Stone}.

Other examples, such as I/O and redirection can be seen at the
\href{http://www.eff-lang.org/try/}{try Eff} page.

\hypertarget{basic-examples}{%
\subsection{Basic examples}\label{basic-examples}}

\subsubsection*{Exceptions}
\label{sec:exceptions}

\lstinputlisting{./eff-examples/exception.eff}

\subsubsection*{State}
\label{sec:state}

\lstinputlisting{./eff-examples/state.eff}

\hypertarget{multi-shot-handlers}{%
\subsection{Multi-shot handlers}\label{multi-shot-handlers}}

A handler has access to the continuation, and it may do with it whatever
it likes. We may distinguish handlers according to how many times the
continuation is invoked:

\begin{itemize}
\item
  an \textbf{exception-like} handler does not invoke the continuation
\item
  a \textbf{single-shot} handler invokes the continuation exactly once
\item
  a \textbf{multi-shot} handler invokes the continuation more than once
\end{itemize}

Of course, combinations of these are possible, and there are handlers
where it's difficult to ``count'' the number of invocations of the
continuation, such as multi-threading below.

An exception-like handler is, well, like an exception handler.

A single-shot handler appears to the programmer as a form of
dynamic-dispatch callbacks: performing the operation is like calling the
callback, where the callback is determined dynamically by the enclosing
handlers.

The most interesting (and confusing!) are multi-shot handlers. Let us
have a look at one such handler.

\hypertarget{ambivalent-choice}{%
\subsubsection{Ambivalent choice}\label{ambivalent-choice}}

Ambivalent choice is a computational effect which works as follows. There is an
exception $\mathsf{Fail} : \mathsf{unit} \to \mathsf{empty}$ which signifies
failure to compute successfully, and an operation
$\mathsf{Select} : \alpha\; \mathsf{list} \to \alpha$, which returns one of the
elements of the list. It has to do return an element such that the subsequent
computation does \emph{not} fail (if possible).

With ambivalent choice, we may solve the $n$-queens problem (of
placing $n$ queens on an $n \times n$ chess board so they do
not attack each other):

\lstinputlisting{./eff-examples/queens.eff}

\hypertarget{cooperative-multi-threading}{%
\subsection{Cooperative
multi-threading}\label{cooperative-multi-threading}}

Operations and handlers have explicit access to continuations. A handler
need not invoke a continue, it may instead store it somewhere and run
\emph{another} (previously stored) continuation. This way we get
\emph{threads}.

\lstinputlisting{./eff-examples/thread.eff}

\hypertarget{tree-representation-of-a-functional}{%
\subsection{Tree representation of a
functional}\label{tree-representation-of-a-functional}}

Suppose we have a \textbf{functional}
%
\begin{equation*}
  h : (\mathsf{int} \to \mathsf{bool}) \to \mathsf{bool}
\end{equation*}

When we apply it to a function $f : \mathsf{int} \to \mathsf{bool}$, we feel
that $h \; f$ will proceed as follows: $h$ will \emph{ask} $f$ about the value
$f \; x_0$ for some integer $x_0$. Depending on the result it gets, it will then
ask some further question $f \; x_1$, and so on, until it provides an
\emph{answer}~$a$.

We may therefore represent such a functional $h$ as a \textbf{tree}:
%
\begin{itemize}
\item
  the leaves are the answers
\item
  a node is labeled by a question, which has two subtrees representing
  the two possible continuations (depending on the answer)
\end{itemize}
%
We may encode this as the datatype:
%
\begin{verbatim}
type tree =
  | Answer of bool
  | Question of int * tree * tree
\end{verbatim}
%
Given such a tree, we can recreate the functional $h$:
%
\begin{verbatim}
let rec tree2fun t f =
  match t with
  | Answer y -> y
  | Question (x, t1, t2) -> tree2fun (if f x then t1 else t2) f
\end{verbatim}
%
Can we go backwards? Given $h$, how do we get the tree? It turns out this is not
possible in a purely functional setting in general (but is possible for out
specific case because $\mathsf{int} \to \mathsf{bool}$ is \emph{compact},
Google ``impossible functionals''), but it is with computational effects. 

\lstinputlisting{./eff-examples/fun_tree.eff}

\hypertarget{problems-1}{%
\subsection{Problems}\label{problems-1}}

\begin{problem}[Breadth-first search]
  Implement the \emph{breadth-first search} strategy for ambivalent choice.
\end{problem}

\begin{problem}[Monte Carlo sampling]
%
The \href{http://www.eff-lang.org/try/}{online Eff} page has an example
showing a handler which modifies a probabilistic computation (one that
uses randomness) to one that computes the \emph{distribution} of
results. The handler computes the distribution in an exhaustive way that
quickly leads to inefficiency.

Improve it by implement a
\href{https://en.wikipedia.org/wiki/Monte_Carlo_method}{Monte Carlo}
handler for estimating distributions of probabilistic computations.
\end{problem}

\begin{problem}[Recursive cows]
  Contemplate the
  \href{https://github.com/effect-handlers/effects-rosetta-stone/tree/master/examples/recursive-cow}{recursive
    cows}.
\end{problem}

\end{document}

%%% Local Variables:
%%% coding: utf-8
%%% mode: latex
%%% TeX-master: t
%%% End: