# On Reinforcement Learning, Effect Handlers, and the State Monad

Ugo Dal Lago  Francesco Gavazzo  Alexis Ghyselen

###### Abstract

We study the algebraic effects and handlers as a way to support decision-
making abstractions in functional programs, whereas a user can ask a learning
algorithm to resolve choices without implementing the underlying selection
mechanism, and give a feedback by way of rewards. Differently from some
recently proposed approach to the problem based on the selection monad [2], we
express the underlying intelligence as a reinforcement learning algorithm
implemented as a set of handlers for some of these algebraic operations,
including those for choices and rewards. We show how we can in practice use
algebraic operations and handlers — as available in the programming language
EFF — to clearly separate the learning algorithm from its environment, thus
allowing for a good level of modularity. We then show how the host language
can be taken as a $\lambda$-calculus with handlers, this way showing what the
essential linguistic features are. We conclude by hinting at how type and
effect systems could ensure safety properties, at the same time pointing at
some directions for further work.

##  1 Introduction

Machine learning is having, and will likely have more and more, a tremendous
impact on the way _computational_ problems (e.g. classification or clustering)
are solved. Learning techniques, however, turn out to be very fruitful when
solving _control_ problems, too. There, in fact, an agent’s goal is to learn
how to maximize its reward while interacting with the environment rather than
while computing a mere function. From this point of view, the so-called
_reinforcement learning_ techniques [34] are proving to be particularly
appropriate in many contexts where exploration and optimization have to be
interleaved.

Prompted by that, in the past decade there has been an incredible effort to
develop programming languages and programming language techniques oriented to
the design of machine learning systems. The outcome of such an effort is well-
known and gave birth to new programming language paradigms, such as Bayesian
[18, 39] and differentiable programming [1, 25, 33], as well as to the
flourishing field of programming languages for inference.111See, e.g., the
dedicated POPL Workshop LAFI https://popl21.sigplan.org/home/lafi-2021.
Despite the incredible strides made, machine learning support from programming
languages is still in its infancy and its deliverables mostly consist of a set
of general-purpose programming language libraries (such as Theano [7],
TensorFlow [3], and Edward [36, 37], just to mention but a few) and domain-
specific languages (such as Anglican [35], Pyro [9], and Stan [11], just to
mention but a few).

In this work, we deal with a further programming language paradigm oriented to
machine learning: _choice-based programming_. The latter moves from the
observation that many machine learning systems — especially those pertaining
the realm of reinforcement learning — can be described in terms of _choices_ ,
_costs_ , and _rewards_. Prompted by that, choice-based programming
languages222 Such as SmartChoice [10].  extend traditional programming
languages with high-level _decision-making_ abstractions that allow for the
modular design of programs in terms of choices and rewards. While in a
probabilistic language programs are structured in terms of sampling and
observing — leaving the actual inference process to the interpreter — in a
choice-based language the code is structured by specifying where a choice
should be made and what its associated cost (or, dually, its reward) is,
leaving the actual decision-making process to the interpreter.

All of that considerably changes the way one writes and thinks about software,
at the same time raising new — and challenging — questions both from the point
of view of programming language theory and of machine learning. In the former
case, in fact, we have to deal with the introduction of decision-making
abstractions, their implementation, and their semantics. In the latter case,
instead, we have just began to realise how to tackle modularity of machine
learning systems using programming language-based techniques.

The latter point is the main topic of this paper. We move from the recent work
by Abadi and Plotkin [2], where a _monadic_ [22] approach to choice-based
programming is developed. There, the authors show how the so-called _selection
monad_ [14, 16, 15] can be used to model (and to give semantics to) programs
written in a choice-based language as _effectful_ programs, and how it is
possible to manage choices as _algebraic operations_ [27, 26, 28], delegating
the task of solving these choices to those who implement the selection
mechanism. In this work, we are concerned with further developing this idea,
although in a different direction. In fact, even if we still deal with monadic
and algebraic approaches to choice-based programming, we explore the use of
the _state_ — rather than _selection_ — _monad_ in the framework of
reinforcement learning systems. In particular, we show how the use of the
state monad allows for a high level of modularity in the construction of
systems based on reinforcement learning.

The reader, at this point, may wonder _why_ one should consider a further kind
of monadic programming — viz. one based on the state monad — when dealing with
reinforcement learning systems . The next two sections are dedicated to answer
this question. There, we will study a simple example coming from the
reinforcement learning literature, highlighting some drawbacks of the
selection monad, on the one hand, and the strengths of our state-based
approach, on the other hand. That will also allow us to illustrate the
practical advantages of functional programming techniques in reinforcement
learning modelling.

For the moment, we simply remark that at the very heart of our approach lies a
clear separation between the part of the program dealing with the learning
algorithm and the one that handles the interaction with the environment. Such
a separation can be naturally structured in the form of a state monad with
choice and reward operations acting as algebraic operations. However — and
here comes the main difference between our approach and the one based on the
selection monad — the action of such operations is _not_ determined by the
monad (as _de facto_ happens when working with the selection monad), but it is
ultimately given by the reinforcement learning algorithm used. As a
consequence, one can model reinforcement learning systems modularly as
monadic, state-based programs written using choice and reward operations, and
then view reinforcement learning algorithms as algebraic interpretations of
such operations. Concretely, that means that we can view (and implement)
reinforcement learning algorithms as _handlers_ [29, 5, 31] giving
interpretations to choice and reward operations. Different learning algorithms
then give different handlers — and thus different interpretations of choices
and rewards — so that it is possible to instantiate the very same program with
different learning algorithms by simply changing the way its algebraic
operations are handled.

Summing up, the main contributions of this paper are the following:

  * •

The development of a modular approach to reinforcement learning systems
throughout functional programming language techniques. Among such techniques,
the main role is played by the _state monad_ and its associated _algebraic
operations_ for performing choices and rewards. Crucially, the use of the
state monad (as opposed to the selection monad) allows us to consider
different interpretations of choices and rewards, such interpretations
ultimately _being_ the reinforcement learning algorithm used. We make use of
_handlers_ to implement these interpretations in a modular fashion.

  * •

The analysis of our approach in a core $\lambda$-calculus with handlers and
algebraic operations. This allows us to isolate the exact features a language
needs to have in order to support our functional approach to reinforcement
learning systems.

  * •

A preliminary study of how to use semantic-based techniques (notably
polymorphic and graded type systems) to ensure correct behaviours of
reinforcement learning systems when implemented in a functional way.

##  2 Structuring Reinforcement Learning Applications Through Functional
Programming

To begin with, we are going to illustrate our approach on a simple running
example, common in the reinforcement learning literature [34], namely the so
called _multi-armed bandit_ problem, denoted MAB. In this setting, a gambler
faces a row of $k$ slot machines, each of which distributes rewards in the
form of winnings according to a probabilistic model unknown to the gambler.
The gambler, it goes without saying, wants to maximize its gains over a fixed
number of rounds. At each round, the gambler chooses a machine and obtains a
reward depending on its reward distribution. On the one hand, then, the
gambler wants to maximize her gains, but on the other she knows nothing about
the inner working of the machines. This example, indeed, expresses the need of
a trade-off between _exploration_ and _optimization_ : the gambler wants to
play on the best machine as much as possible, but in order to find this best
machine, she needs to try _every_ machine. Moreover, since rewards are random,
playing once on each machine, then playing only on the one with the best
observed reward, may not be optimal in the long run. Reinforcement learning
indeed focuses in offering techniques which explores this trade-off in a
meaningful way.

What we are interested in doing here is deriving a strategy for the agent in
the aformentioned problem _using_ reinforcement learning techniques, and _with
the help_ of functional programming. We are _not_ interested at devising new
algorithms, but rather at showing that functional programming can help in
_giving structure_ to programs which comprise both the proper learning
algorithm, but also the interaction with the environment.

Conceptually, it is natural to see a program solving MAB by way of
reinforcement learning as structured into three parts:

  * •

The first one, the environment, serves as an interface with the outside world,
making it visible to the program. Here, this part comprises the $k$ slot
machines, possibly through a system of sensors and functions querying those
sensors.

  * •

The second one, the learner, which provides generic reinforcement learning
algorithms, possibly through libraries. There are many algorithms the
literature offers, for example gradient learning, Q-learning, expected Sarsa
or other TD-methods [34].

  * •

The user, namely some code letting the environment and the learner exchange
information, thus acting as a bridge between the two. Here, the user is
supposed to turn events and data coming from the environment into a form which
can be understood by the learner.

One of the key ingredients of our proposal consists in structuring these three
parts and their interaction by stipulating that the user proceeds by invoking
some algebraic operations provided by both the environment and the learner.
This is schematized in Figure 1.

Environment  User $O_{E}$ : Observations $A_{E}$ : Actions User $O_{E}$ :
Observations $A_{E}$ : Actions Learner $O_{\mathit{RL}}$ : Abstract
Observations $A_{\mathit{RL}}$ : Abstract Actions
$\mathtt{observe}$$\mathtt{do}$$\mathtt{choice}$$\mathtt{reward}$Abstract
Interface

Figure 1: Our approach

The main algebraic operations are the four mentioned in the figure, two of
them provided by the environment and two provided by the learner. The two
algebraic operations provided by the environment are $\mathtt{observe}$ and
$\mathtt{do}$. The former, having type $1\rightsquigarrow O_{E}$ allows the
user to retrieve some data from the environment. In our multi-armed bandit
example, it corresponds to observing the gain on the current slot machine. The
operation $\mathtt{do}:A_{E}\rightsquigarrow 1$ executes an action in the
environment. In our running example, an action would be the choice of one of
the $k$ slot machines. Those operations depend the set of possible
observations and the set of possible actions in the environment, those sets
being represented by two types $O_{E}$ and $A_{E}$ in the user code. In our
example, the observations are the gains, thus we can give the type
$O_{E}=\mathtt{Real}$. As for actions, they stand for choices of a slot
machine, and thus $A_{E}=\\{1,\dots,k\\}$.

Then, there are two other operations for the learner, namely $\mathtt{choice}$
and $\mathtt{reward}$. The operation $\mathtt{choice}:1\rightsquigarrow A_{E}$
asks the learner to take an action for us. In our setting it means that a call
to $\mathtt{choice}$ returns an integer between $1$ and $k$ designing the slot
machine the user should play on. The
$\mathtt{reward}:\mathtt{Real}\rightsquigarrow 1$ operation allows the user to
give a feedback to the learner depending on its previous choice. In our
example, the typical reward would be the gain obtained from the slot machine
chosen by the learner. There is also an additional bridge between the user and
the learner, that we call the _abstract interface_ : the learner may need more
information than the feedback given by $\mathtt{reward}$, and this information
will be transmitted using the abstract interface by way of some additional
algebraic operations invoked by the learner but handled by the user.

One advantage of the just described approach is to show that this learner part
of the program, i.e., the handler for the operations $\mathtt{choice}$ and
$\mathtt{reward}$, can be implemented _independently_ from the details of the
environment, once and for all. One could even conceive to have a library of
handlers, where each set of handlers corresponds to a reinforcement learning
algorithm, in such a way that the user could choose one of these handlers for
each of the environments he has access to, implementing the abstract interface
but without delving into the details of the underlying algorithms. Similarly,
implementing any new RL algorithm would boil down to just write a new set of
handlers for $\mathtt{choice}$ and $\mathtt{reward}$.

In which _order_ should the user invoke the various algebraic operations? A
typical sequence of interactions would be
$\mathtt{choice}\rightarrow\mathtt{do}\rightarrow\mathtt{observe}\rightarrow\mathtt{reward}$,
meaning intuitively that it asks for a choice, and then does explicitly this
action in the environment, observes the results of this action, and finally
produces a reward. As we will soon see, it is preferable that the user indeed
respects this order, e.g., when handling the $\mathtt{reward}$ operation, the
learner may need to observe the environment (abstracted by the interface)
since a valuation function typically depends on the state reached after an
action.

In order to have a learner independent from the environment, it must not make
explicit reference to the types $A_{E}$ and $O_{E}$, as we saw on MAB. Thus,
we introduce two _finite_ sets $O_{\mathit{RL}}$ and $A_{\mathit{RL}}$
corresponding to the abstract sets of observations and actions, respectively.
Except for their sizes, those finite sets must be totally independent form the
environment. It means that in practice, the learner only has access to some
elements of those sets, and should make choices in $A_{\mathit{RL}}$ depending
only on the abstract observations from $O_{\mathit{RL}}$ it receives from the
user. Typically, both the policy to choose actions and the learning part are
built by constructing and updating a _value function_ mapping pairs in
$O_{\mathit{RL}}\times A_{\mathit{RL}}$ to a reward estimation, for example an
element of $\mathtt{Real}$.

###  2.1 A Naive RL Algorithm in EFF

We present our approach practically with a very basic algorithm for
reinforcement learning, which works by only remembering an evaluation function
keeping track of _the expectation_ of the immediate rewards it receives for
any of the actions, and chooses an action by way of a so-called
$\varepsilon$-greedy policy [34]: with probability $(1-\varepsilon)$, it makes
the best possible choice based on the _current_ valuation, and with
probability $\varepsilon$ it explores by choosing an action uniformly at
random. To implement this algorithm, we use the language EFF [31], an OCAML-
based language for effects and handlers. The syntax of EFF should be
understandable to anyone with some basic knowledge on OCAML, effects and
handlers. We use lists for the sake of simplicity, although other kinds of
data structures would enable better performances. The source code as well as
other examples can be found in [13].

##### Declaring The Abstract Interface.

The first step towards implementing the RL algorithm consists in declaring the
sets $O_{\mathit{RL}}$ and $A_{\mathit{RL}}$ together with the abstract
interface which will allow us to recover some information on the sets
$O_{\mathit{RL}}$ and $A_{\mathit{RL}}$:

⬇

type rl_act

type rl_obs

effect rl_observe : unit $\mapsto$ rl_obs

effect rl_getavailableact : rl_obs $\mapsto$ rl_act list

Here, the first effect allows the learner to observe the environment (after
the abstraction) and to get, for each observation, the list of available
actions it has to choose from. As we stated before, the learner does _not_
have access to the interpretation of those two effects nor to the actual
types, and only knows that those sets of abstract actions and observations are
finite, this being enough to implement the reinforcement learning algorithm.

##### Handling Choices and Rewards.

The handler makes essential use of the state monad, where the state represents
the memory of the learner. For the specific RL algorithm we are targeting now,
this memory consists of an element of this type:

⬇

type memory = ((rl_obs*((rl_act*int*float) list)) list)*int*int

The left type of the internal memory corresponds to a _value function_ , for
each pair of an observable and an action, we give an estimation of the
immediate reward we can obtain. It is computed as the _average_ reward, and in
order to do this average incrementally, it is common to also remember the
number of times a choice has been made. Then, the internal memory also
remembers the _last choice made_ using a pair of integers denoting indexes in
the evaluation function (we usually denote $na$ the index of an action and
$no$ the index of an observation). Then, we can implement the
$\varepsilon$-greedy policy of the learner (we only describe the important
functions and not the simple intermediate one).

⬇

(* This function takes as input a probability and a list of reward estimation

and returns the selected action and its index in the list *)

let greedypolicy ($\epsilon$,l) =

if ((randomfloat 1.) <= $\epsilon$) then

(* Uniform choice in this case *)

begin

let na = randomint (list_length l) in

(* Find the action with index na *)

let a = findact l na in

(na,a)

end

else

(* Select the action with the maximal estimated reward *)

argmax l

;;

And with this, and some other auxiliary functions, we can define the handler
for the basic RL algorithm. The only non-standard clause for the handler is
the last one, starting with $\mathtt{finally}$, in this setting with a state
monad, it should be understood as the initial state for a computation.

⬇

(*The first input is the probability of exploring,

the second is the initial estimation*)

let rl_naive $\epsilon$ v = handler

(*declare a state monad, with the type described above*)

| y $\mapsto$ (fun (_:memory) $\mapsto$ y)

| effect Choice k $\mapsto$ fun (l,_,_) $\mapsto$

(*use the interface to get an observation*)

let o = rl_observe () in

(* extract the index no for o, with its list of estimations q *)

let (l’,no,q) = getstateestimate l o v in

(* select the action a with the greedy policy *)

let (na,a) = greedypolicy ($\epsilon$,q) in

(*update the estimations*)

let l” = updatestate l’ no (fun ll $\mapsto$ updatechoice ll na) in

(*return action a, with the updated memory*)

(continue k a) (l”,no,na)

| effect (Reward r) k $\mapsto$ fun (l,no,na) $\mapsto$

(*update estimations for the previous choice (no,na) *)

let l’ = updatestate l no (fun q $\mapsto$ updatereward q na r) in

(*give the new memory to the continuation*)

(continue k ()) (l’,no,na)

(*initial memory*)

| finally f $\mapsto$ f ([],0,0)

;;

Note that we initialize the estimations lists only when we see an element of
$O_{\mathit{RL}}$ for the first time. This is standard in RL because there
could be an extremely large set of states, and it may well be that not all of
them are reached — it may be better to give an initial estimation to a state
only when we actually see this state (in this program, this is done by the
$\mathtt{geststateestimate}$ function). We do not give the code of the update
functions, which is anyway easy to write. The nice thing of this handler is
that it _does not depend_ on the environment, it can of course interact with
its environment (using $\mathtt{rl\\_observe}$) but it does so in a modular
way, so that this program can be used in _any environment_ in which we would
like to experiment this (admittedly naive) algorithm.

###  2.2 The Multi-Armed Bandit in EFF

We show how to make use of the RL algorithm described in the previous section
on the environment coming from MAB. The first step consists in declaring the
types for $O_{E}$ and $A_{E}$. Since rewards are earnings, and our actions are
nothing more than a choice of a specific machine, we can proceed as follows:

⬇

type env_obs = float

type env_act = int

##### Modeling the Environment

We model MAB as a program, where we take a very simple distribution of rewards
for the sake of the example. As stated before, the environment correspond to
the handling of $\mathtt{observe}$ and $\mathtt{do}$.

⬇

type env_state = float

(* The random reward of the machine a.

In a real case, this reward should be obtained

by observing the result of the slot machine *)

let getreward (a:act) = (float_of_int a) +. (randomfloat 10.) ;;

(*max corresponds to the number of slot machines *)

let MAB_handler max = handler

| y $\mapsto$ (fun (_:env_state) $\mapsto$ y)

| effect (Do a) k $\mapsto$ fun _ $\mapsto$

(* When seeing a valid action a, we compute the gain for the

slot machine a and store the result in the memory *)

if (a > 0) && (a <= max) then (continue k ()) (getreward a)

else raise "This action is not available! \n"

(*An observation corresponds to showing the stored result *)

| effect Observe k $\mapsto$ fun r $\mapsto$ (continue k r) r

(* Initial environment, no rewards observed *)

| finally f $\mapsto$ f 0.

;;

##### Implementing the Abstract Interface

The abstract interface is a handler that implements the types
$A_{\mathit{RL}}$ and $O_{\mathit{RL}}$, and handles the algebraic operations
declared by the learner:

⬇

(* Abstractions Types. The type unit for observations

means that the learner has no information on the environment *)

type rl_obs = unit ;;

type rl_act = int ;;

effect rl_observe : rl_obs

effect rl_getavailableact : rl_obs $\mapsto$ rl_act list

(*Transform a standard observation into an abstract one*)

let abstractobs (o : env_obs) :obs = () ;;

(*The handler describes:

- the abstraction of observations

- the actions available to the learner *)

let abs_MAB max =

let l = list_enumerate 1 (max + 1) in

handler

| effect rl_observe k $\mapsto$ let o = observe () in

continue k (abstractobs o)

| effect (rl_getavailableact o) k $\mapsto$ continue k l

;;

##### The Main Program

With this, we have everything we need to handle the four main operations. In
order to use the learner described above, we can just open the file in which
the RL algorithm is defined and use it as a handler, with the interface
described above. For example, we can write the main program:

⬇

#use "MAB_Environment.eff" ;;

#use "RL_Naive.eff";;

(*Multi-Armed Bandit with 6 machines *)

with (MAB_handler 6) handle

(*Provides the interface to the learner *)

with (abs_MAB 6) handle

(* Call the Basic RL algorithm described previously *)

with (rl_naive 0.05 10.) handle

(*Start writing your progam with algebraic operations

Here, we do 500 rounds *)

let rec run n r =

if n = 0 then r else

let a = choice () in (do a);

let r’ = observe () in

reward r’; run (n-1) (r +. r’)

in run 500 0.

;;

And the point is that if we want to use another learner we only have to load a
different handler for the learner, and this naive learner can be used in any
environment as long as the abstract interface is handled.

##  3 The Selection Monad, and Why it is Not an Answer

To gain a better understanding of the differences between our _state_ -based
approach and the _selection_ -based approach by Abadi and Plotkin [2], let us
illustrate some of the main drawbacks exhibited by the selection monad when
applied to MAB. To do so, let us first shortly recap the underlying mechanism
behind such a monad.

The selection monad is defined through the functor $S(X)=(X\rightarrow
R)\rightarrow X$, where $R$ is a (usually ordered) set of rewards.
Intuitively, a computation in $S(X)$ takes in input a reward function $f:X\to
R$ associating to each element in $X$ a reward in $R$ (we can think about
$f(x)$ as a measure of the goodness of $x$), and chooses an element in $X$
that, intuitively, is optimal for $f$. By its very definition, even if the set
$R$ of rewards is a parameter of the selection monad, the latter does not have
direct access to it: the only way to interact with rewards is through a reward
function, meaning that the selection monad, by itself, does not handle rewards
_directly_. Abadi and Plotkin [2] overcome this problem by combining the
selection monad with another monad $T$ giving direct access to rewards, this
way obtaining (a monad whose carrier is) the functor

$S_{T}(X)=(X\rightarrow R)\rightarrow T(X).$

Here, $T$ can for example be the $R$-based writer monad $T(X)=R\times X$ —
this way, rewards can be found in the first component of the result whenever a
choice is made. One can even go beyond that and take
$T(X)=D_{\mathit{fin}}(R\times X)$, where $D_{\mathit{fin}}$ is the finite
distribution monad, this way modeling stochastic rewards.

Using this strategy — i.e. working with $S_{T}$ rather than with $S$ alone —
we can indeed model (stochastic) rewards as prescribed by the multi-armed
bandit problem. For that, we just consider the monad
$(X\rightarrow\mathbb{R})\rightarrow D_{\mathit{fin}}(\mathbb{R}\times X)$.
The last ingredient needed to attempt a selection monad-based model to MAB is
to give _choice operations_ , which ultimately constitute the way to construct
selection computations. As the reader may guess, this is the most delicate
point.

The selection monad comes with a choice operation $\mathtt{choice}$ which
given two selection computations $a$ and $b$ in $S(X)$, returns a new
computation $\mathtt{choice}(a,b)$ belonging to $S(X)$ working as follow:
given a reward function $f:X\rightarrow R$, $\mathtt{choice}(a,b)$ passes $f$
to both $a$ and $b$, this way obtaining two candidate optimal elements $a(f)$
and $b(f)$, and then chooses between the latter on the basis of $f$. More
precisely, given $a(f)$ and $b(f)$, we can obtain a reward for each of them as
the elements $f(a(f))$ and $f(b(f))$ in $R$. Assuming $R$ to come with a
binary relation $\preceq$ ranking rewards, we then let
$\mathtt{choice}(a,b)(f)$ to return the best one between $a(f)$ and $b(f)$
according to $\preceq$.

At this point, we can already start perceiving the main issue behind choice
operations: to choose between two computations, we have to simulate _both_ of
them, and then take the optimal one. In any case, this concerns the selection
monad $S$ alone. What about the monad $S_{T}$, i.e. the combination of the
selection monad with a monad $T$ giving access to rewards? Here, the situation
is slightly more complicated, but the basic mechanism behind choice operations
is essentially the same one for $S$. Proceeding as for the latter, we obtain
elements $a(f)$ and $b(f)$ belonging to $T(X)$: this time, however, we cannot
directly apply the reward function $f$ on them. The solution proposed by Abadi
and Plotkin [2] is to require to have a $T$-algebra $\alpha:T(R)\to R$, so
that we can apply $T(f)$ — rather than $f$ — on $a(f)$ and $b(f)$, this way
obtaining monadic rewards $T(f)(a(f))$, $T(f)(b(f))$ in $T(R)$; map them into
$R$ using $\alpha$; and then choose the optimal one according to the order
$\preceq$ on $\mathbb{R}$. For instance, taking real numbers as rewards, we
can take, e.g., $\alpha:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ as real-
number by addition.

Notice that dealing with choice operations this way, we not only still have
the same problem seen for $S$ — namely that choosing between computations
require to simulate _all_ of them — but we also have to compute monadic
applications of $f$. That is, the application of $T(f)$ to an element $\phi\in
T(X)$ usually requires to compute the reward $f(x)$ for each element $x$ which
is, intuitively, part of $\phi$. For instance, if we think about $\phi$ as a
distribution, then computing $T(f)(\phi)$ requires to compute the reward of
each element in the support of $\phi$. All of that does not fit well with the
very essence of reinforcement learning, as we are going to see.

Let us now come to reinforcement learning systems and to the multi-armed
bandit example, highlighting the main problem behind the semantic mechanism of
choice operations. First, let us notice that the selection monad seems to
provide an adequate setting for reinforcement learning. In fact, taking the
monad $(X\rightarrow\mathbb{R})\rightarrow D_{\mathit{fin}}(\mathbb{R}\times
X)$, we obtain choices and (stochastic) rewards, and the former can in
principle depend on the latter. In such a setting, the choice operation is
defined parametrically with respect to an algebra
$\alpha:D_{\mathit{fin}}(\mathbb{R}\times\mathbb{R})\to\mathbb{R}$, which can
be naturally defined as follows: given a distribution $\phi$, we first apply
addition to all the elements in the support of $\phi$, and then compute the
resulting expectation. Given such an algebra $\alpha$, to perform a choice
operation $\mathtt{choose}$ between two computations $a$ and $b$ with a reward
function $f$, we first compute the probability distributions $a(f)$ and
$b(f)$, and then compute the expected reward associated to _each_ such a
distribution, which means first computing the reward of _each_ element in its
support.

The latter passage is not reasonable from reinforcement learning perspective.
In fact, when dealing with reinforcement learning systems, implementing
choices operations this way forces us to $(i)$ simulate _all_ actions; $(ii)$
to obtain a perfect knowledge of the environment; $(iii)$ and to make
(optimal) choices based on that. In MAB, that means $(i)$ simulating playing
on _each_ machine; $(ii)$ observing the _whole_ distributions associated to
each machine; $(iii)$ and then select the one with the best expectation, which
in turn requires to compute the rewards of _each_ element in the support of
the distribution of a machine. All of that is simply to strong to give a
reasonable model of reinforcement learning systems. Notice that all of that is
essentially independent of the choice of the algebra $\alpha$, meaning that
the problem lies at the very hearth of he selection monad (and its choice
operations) rather than on the concrete way one aggregates monadic rewards.

##  4 From Practice to Theory: Effects and Handlers

In this section, we try to inject the ideas we developed in Section 2 into a
paradigmatic programming language, so as to be able to isolate the features we
deem necessary.

###  4.1 A Core Language with Effects and Handlers

For the sake of simplicity, we take the core language described in [31] with
additional base types corresponding to observations and actions and a simple
type system without type effects. We will not talk about the details of the
underlying effect, such as randomness, I/O, or exceptions. Those effects are
obviously needed in practice, but adding them to the theory would be standard,
so for the sake of simplicity we ignore those, and when we write a type
$T\rightarrow T^{\prime}$, this function should be understood as a function
that can use those standard effects.

The grammar for terms and types is in Figure 2.

$\displaystyle\text{(Values) }V$
$\displaystyle::=x\;\mbox{\Large{$\mid$}}\;\lambda
x.C\;\mbox{\Large{$\mid$}}\;(V,V)\;\mbox{\Large{$\mid$}}\;()\;\mbox{\Large{$\mid$}}\;\underline{c}\;\mbox{\Large{$\mid$}}\;\underline{f}\;\mbox{\Large{$\mid$}}\;H$
$\displaystyle\text{(Handlers) }H$
$\displaystyle::=\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto
C,\mathtt{op}_{1}(x;k)\mapsto C,\dots,\mathtt{op}_{n}(x;k)\mapsto C\\}$
$\displaystyle\text{(Computations) }C$
$\displaystyle::=\mathbf{return}~{}V\;\mbox{\Large{$\mid$}}\;\pi_{i}(V)\;\mbox{\Large{$\mid$}}\;\mathtt{op}(V;x.C)\;\mbox{\Large{$\mid$}}\;\mathbf{let}~{}x=C~{}\mathbf{in}~{}C\;\mbox{\Large{$\mid$}}\;V~{}V\;\mbox{\Large{$\mid$}}\;\mathbf{with}~{}V~{}\mathbf{handle}~{}C$
$\displaystyle\text{(Types) }T$
$\displaystyle::=\mathtt{B}\;\mbox{\Large{$\mid$}}\;\mathtt{Unit}\;\mbox{\Large{$\mid$}}\;T\times
T\;\mbox{\Large{$\mid$}}\;T\rightarrow T\;\mbox{\Large{$\mid$}}\;T\Rightarrow
T$

Figure 2: Syntax and Types of Terms

In other words, we work with a $\lambda$-calculus with pairs base types
(ranged over by $\mathtt{B}$), constants and functions for those base types,
denoted by $\underline{c}$ and $\underline{f}$. Any symbol $c\in\mathcal{C}$
is associated to a base type $\mathtt{B}$, while any symbol $f\in\mathcal{F}$
comes equipped with a function type
$\mathtt{B}_{1}\times\cdots\times\mathtt{B}_{n}\rightarrow\mathtt{B}$.
Moreover, we have algebraic operations, each operation symbol $\mathtt{op}$
coming with a type $\mathtt{op}:T_{p}\rightsquigarrow T_{a}\in\Sigma$ where
$T_{p}$ is the type of parameters and $T_{a}$ is the arity. In a computation
$\mathtt{op}(V;x.C)$, the variable $x$ is bound in $C$. Those operations are
handled by handlers. An handler has the following form

$\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto
C_{r},\mathtt{op}_{1}(x;k)\mapsto C_{1},\dots,\mathtt{op}_{n}(x;k)\mapsto
C_{n}\\}$

Here, the computations $C_{1},\ldots,C_{n}$ are pieces of code meant to handle
the corresponding algebraic operation, while $C_{r}$ is meant to handle a
return clause. We use the arrow $\Rightarrow$ to denote handler types,
contrary to the function type that uses $\rightarrow$. When one wants to use
the aforementioned handler for the purpose of managing some algebraic
operations, we do by way of a term in the form

$\mathbf{with}~{}V~{}\mathbf{handle}~{}C$

in which $C$ is executed in a protected environment such that any algebraic
operations produced by $C$ is handled by the handler $V$, provided it is one
among those declared in it.

The typing rules for this language are given in Figure 3. In a computation
$\mathtt{op}(V;x.C)$, $C$ can be seen as a continuation for the computation,
with type $T_{a}\rightarrow T$, this is why in the typing of handler, the
second parameter $k$ has this type. The typing rule for the handler with
simple types looks like a function application, where the handler transforms a
computation of type $T_{2}$ to a computation of type $T_{1}$.

$\Gamma,x:T\vdash x:T$ $\Gamma,x:T_{1}\vdash C:T_{2}$ $\Gamma\vdash\lambda
x.C:T_{1}\rightarrow T_{2}$ $\Gamma\vdash V_{1}:T_{1}$ $\Gamma\vdash
V_{2}:T_{2}$ $\Gamma\vdash(V_{1},V_{2}):T_{1}\times T_{2}$
$\Gamma\vdash():\mathtt{Unit}$ $c:\mathtt{B}\in\mathcal{C}$
$\Gamma\vdash\underline{c}:\mathtt{B}$
$f:\mathtt{B}_{1}\times\cdots\mathtt{B}_{n}\rightarrow\mathtt{B}\in\mathcal{F}$
$\Gamma\vdash\underline{f}:\mathtt{B}_{1}\times\cdots\mathtt{B}_{n}\rightarrow\mathtt{B}$
$\\{(\mathtt{op}_{i}:T^{p}_{i}\rightsquigarrow
T^{a}_{i})\in\Sigma\qquad\Gamma,x:T_{i}^{p},k:T_{i}^{a}\rightarrow T_{c}\vdash
C_{i}:T_{c}\\}_{1\leq i\leq n}$ $\Gamma,x:T_{v}\vdash C_{r}:T_{c}$
$\Gamma\vdash\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto
C_{r},\mathtt{op}_{1}(x;k)\mapsto C_{1},\dots,\mathtt{op}_{n}(x;k)\mapsto
C_{n}\\}:T_{v}\Rightarrow T_{c}$ $\Gamma\vdash V:T$
$\Gamma\vdash\mathbf{return}~{}V:T$ $\Gamma\vdash V:T_{1}\times T_{2}$
$\Gamma\vdash\pi_{i}(V):T_{i}$ $(\mathtt{op}:T_{p}\rightsquigarrow
T_{a})\in\Sigma$ $\Gamma\vdash V:T_{p}$ $\Gamma,x:T_{a}\vdash C:T$
$\Gamma\vdash\mathtt{op}(V;x.C):T$ $\Gamma\vdash C_{1}:T_{1}$
$\Gamma,x:T_{1}\vdash C_{2}:T_{2}$
$\Gamma\vdash\mathbf{let}~{}x=C_{1}~{}\mathbf{in}~{}C_{2}:T_{2}$ $\Gamma\vdash
V_{1}:T_{2}\rightarrow T_{1}$ $\Gamma\vdash V_{2}:T_{2}$ $\Gamma\vdash
V_{1}~{}V_{2}:T_{1}$ $\Gamma\vdash V:T_{2}\Rightarrow T_{1}$ $\Gamma\vdash
C:T_{2}$ $\Gamma\vdash\mathbf{with}~{}V~{}\mathbf{handle}~{}C:T_{1}$

Figure 3: Typing Rules

Then, the dynamic semantics is given in Figure 4. Algebraic operations can
commute with the $\mathbf{let}~{}$ constructor and handlers for other
operations. As for handlers, the return computation is handled by the return
clause, and an algebraic operation is handled by the corresponding computation
in the handler, where the continuation $k$ is replaced by the actual
continuation $C$ with the same handler.

$\pi_{i}(V_{1},V_{2})\rightarrow V_{i}$ $C_{1}\rightarrow C_{1}^{\prime}$
$\mathbf{let}~{}x=C_{1}~{}\mathbf{in}~{}C_{2}\rightarrow\mathbf{let}~{}x=C_{1}^{\prime}~{}\mathbf{in}~{}C_{2}$
$\mathbf{let}~{}x=\mathtt{op}(V;y.C_{1})~{}\mathbf{in}~{}C_{2}\rightarrow\mathtt{op}(V;y.\mathbf{let}~{}x=C_{1}~{}\mathbf{in}~{}C_{2})$
$\mathbf{let}~{}x=\mathbf{return}~{}V~{}\mathbf{in}~{}C_{2}\rightarrow
C_{2}[V/x]$
$(\lambda x.C)~{}V\rightarrow C[V/x]$
$V=(\underline{c_{1}},\dots,\underline{c_{n}})$ $c=f(c_{1},\dots,c_{n})$
$\underline{f}~{}V\rightarrow\underline{c}$
For the following rules, we denote
$H=\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto
C_{r},\mathtt{op}_{1}(x;k)\mapsto C_{1},\dots,\mathtt{op}_{n}(x;k)\mapsto
C_{n}\\}$
$C\rightarrow C^{\prime}$
$\mathbf{with}~{}H~{}\mathbf{handle}~{}C\rightarrow\mathbf{with}~{}H~{}\mathbf{handle}~{}C^{\prime}$
$\mathtt{op}\notin\\{\mathtt{op}_{1},\dots,\mathtt{op}_{n}\\}$
$\mathbf{with}~{}H~{}\mathbf{handle}~{}\mathtt{op}(V;x.C)\rightarrow\mathtt{op}(V;x.\mathbf{with}~{}H~{}\mathbf{handle}~{}C)$
$\mathbf{with}~{}H~{}\mathbf{handle}~{}\mathbf{return}~{}V\rightarrow
C_{r}[V/x]$
$\mathbf{with}~{}H~{}\mathbf{handle}~{}\mathtt{op}_{i}(V;x.C)\rightarrow
C_{i}[V/x][\lambda x.\mathbf{with}~{}H~{}\mathbf{handle}~{}C/k]$

Figure 4: Semantics

With this, we have a complete description of a core language with effects,
handlers and base types. In practice, we also want other standard constructors
for booleans (if then else), lists or other data structures, but this can be
easily added to the core language without any theoretical difficulties. It is
then relatively standard to prove the subject reduction of this type system,
proving some simple kind of safety:

######  Theorem 1 (Subject Reduction).

If $\Gamma\vdash C:T$ and $C\rightarrow C^{\prime}$ then $\Gamma\vdash
C^{\prime}:T$

###### Proof.

The proof is standard. We start by proving a weakening lemma (if $\Gamma\vdash
C:T$ then $\Gamma,x:T^{\prime}\vdash C:T$) and a value substitution lemma (if
$\Gamma,x:T\vdash C:T^{\prime}$ and $\Gamma\vdash V:T$ then $\Gamma\vdash
C[V/x]:T^{\prime}$) by induction on judgment, and then we can prove subject
reduction by induction on the relation $C\rightarrow C^{\prime}$. The
weakening lemma is useful for the cases when an algebraic operation
$\mathtt{op}$ commute with a $\mathbf{let}~{}$or an $\mathbf{handle}$, and the
substitution lemma is useful for substitutions, which are always for values as
one can see in Figure 4. ∎

However, with those simple types it is not possible to prove that any typable
computation reduces to a computation of the shape $\mathbf{return}~{}V$,
because a non handled operation $\mathtt{op}$ cannot be reduced. To have those
kind of safety theorems, we need type effects, as we will see in the next
section.

###  4.2 Setting the Stage: Types and Algebraic Operations for RL

Let us now instantiate more clearly the set of base types and operations for
our approach. We consider that:

  * •

Base types should contain at least
$\mathtt{Bool},\mathtt{Real},A_{E},O_{E},A_{\mathit{RL}},O_{\mathit{RL}}$,
respectively the types for booleans, real number for rewards, _actions_ ,
_observations_ and their abstract counterparts.

  * •

Constants for booleans and real numbers are standard. For
$A_{E},A_{\mathit{RL}}$ and $O_{\mathit{RL}}$, we consider finite sets of
constants, and $A_{E},A_{\mathit{RL}}$ should have the same size. As for
$O_{E}$, the set of constants depends on the environment so we have no fixed
choice.

  * •

We have standard functions for booleans and real numbers, and equality for all
those base types. We may also have additional functions for $O_{E}$ depending
on the environment.

  * •

For the set of operations symbols, we suppose that we have at least the main
four operations described before

$\displaystyle\mathtt{choice}$ $\displaystyle:\mathtt{Unit}\rightsquigarrow
A_{E}$ $\displaystyle\mathtt{reward}$
$\displaystyle:\mathtt{Real}\rightsquigarrow\mathtt{Unit}$
$\displaystyle\mathtt{observe}$ $\displaystyle:\mathtt{Unit}\rightsquigarrow
O_{E}$ $\displaystyle\mathtt{do}$
$\displaystyle:A_{E}\rightsquigarrow\mathtt{Unit}$

And, in order to make the abstraction more formal, we also add

$\displaystyle\mathtt{choice_{\mathit{RL}}}$
$\displaystyle:\mathtt{Unit}\rightsquigarrow A_{\mathit{RL}}$
$\displaystyle\mathtt{reward_{\mathit{RL}}}$
$\displaystyle:\mathtt{Real}\rightsquigarrow\mathtt{Unit}$

Moreover, we also need to add effects corresponding to the abstract interface.
As this interface is not fixed, we chose for the sake of the example the one
we used on the naive algorithm. So we add those operations:

$\displaystyle\mathtt{observe_{\mathit{RL}}}$
$\displaystyle:\mathtt{Unit}\rightsquigarrow O_{\mathit{RL}}$
$\displaystyle\mathtt{getactions_{\mathit{RL}}}$
$\displaystyle:O_{\mathit{RL}}\rightsquigarrow
A_{\mathit{RL}}~{}\mathtt{List}$

This describes all we need in order to formalize our approach. However, in
practice, we do not want all the actors (environment, user and learner) to
have access to all those operations at all time. A typical example is that the
learner must not use $\mathtt{observe}$ or have access to $O_{E}$ as it would
break abstraction, and thus modularity. As a first approach, we define subsets
of this language, by defining subsets of base types, functions and algebraic
operation, so that we can define clearly which actor has access to which
constructors. In the next section on safety, we will formalize this with a
type system.

  * •

The whole language described above, with all base types and operations is
denoted $\lambda_{\mathit{eff}}^{I}$. This calculus will be used to define the
interface, as an interface should be able to see both the constructors for the
environment and for the learner in order to make the bridge.

  * •

We denote by $\lambda_{\mathit{eff}}^{E}$ the subset of this whole language
without types and operations related to the learner (all types and operations
with $\mathit{RL}$ in the name, such as $A_{\mathit{RL}}$,
$\mathtt{choice}_{\mathit{RL}}$, …). This language will be used for the main
program and the handler for $\mathtt{do}$ and $\mathtt{observe}$, as it is
basically the language with no concrete information about the learner.

  * •

Dually, we denote by $\lambda_{\mathit{eff}}^{\mathit{RL}}$ the language with
_only_ the operations related to the learner. Also, in
$\lambda_{\mathit{eff}}^{\mathit{RL}}$, we consider that we do not have any
functions nor constants for $O_{\mathit{RL}}$ and $A_{\mathit{RL}}$ except
equality and the operations in the abstract interface. Indeed, this language
will correspond to the learner, and as explained before, we want the learner
to be independent from its environment. An important point to make this
possible, is that the learner should be modular (or ideally, polymorphic) in
the types $O_{\mathit{RL}}$ and $A_{\mathit{RL}}$, and so having access to the
constants of those types would break this principle. In particular, with this
definition of $\lambda_{\mathit{eff}}^{\mathit{RL}}$, changing the size of the
finite sets $O_{\mathit{RL}}$ and $A_{\mathit{RL}}$ does not modify the
language, so whatever the size may be, the learner still uses the same
language.

###  4.3 RL Algorithms and Environments as Handlers

We start with the main program. As showed in the previous section, the main
program is just an usual functional program that has access to the types
$O_{E}$ and $A_{E}$ as well as the four main operations $\mathtt{choice}$,
$\mathtt{reward}$, $\mathtt{observe}$ and $\mathtt{do}$. Thus, it corresponds
to the language we denote $\lambda_{\mathit{eff}}^{E}$. This is the main focus
of our work, to make it possible to program within this language. In order to
do this we still need to handle those four operations, and for this we design
several handlers.

####  4.3.1 The Learner

The learner is a handler with the state monad for the operations
$\mathtt{choice}_{\mathit{RL}}$ and $\mathtt{reward}_{\mathit{RL}}$, written
in $\lambda_{\mathit{eff}}^{\mathit{RL}}$. So, formally, the learner is a
handler

$H_{\mathit{RL}}\equiv\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto\lambda
m.\mathbf{return}~{}(m,x),\mathtt{choice}_{\mathit{RL}}(k)\mapsto
C_{c},\mathtt{reward}_{\mathit{RL}}(r;k)\mapsto C_{r}\\}$

such that

$k:A_{\mathit{RL}}\rightarrow S_{M}(T)\vdash C_{c}:S_{M}(T)\qquad
r:\mathtt{Real},k:\mathtt{Unit}\rightarrow S_{M}(T)\vdash C_{r}:S_{M}(T)$

where $T$ is any type and $S_{M}(T)\equiv M\rightarrow(M\times T)$ is the type
for the state monad with state $M$, that represents the _memory_ of the
learner. With this, we obtain a handler $H_{\mathit{RL}}$ with type
$T\Rightarrow S_{M}(T)$ for any $T$.

In this handler, we can indeed encode a RL algorithm, as we did for the naive
algorithm for MAB, because, informally:

  * •

The memory $M$ can contain a value function, associating an heuristic to pairs
of states and actions ($O_{\mathit{RL}}\times A_{\mathit{RL}}$). It can also
be used to log information if needed, typically the previous choice, the
number of times choice was called …

  * •

The term for choice $C_{c}$ has a link with the _policy_ of the learner.
Indeed, a policy can be seen as a function of type $M\rightarrow
A_{\mathit{RL}}\times M$, where, from an internal memory of the learner, we
chose an action in $A_{\mathit{RL}}$ and we can also modify the memory if
needed, for example to log this choice. With this policy, it is easy to obtain
a computation $C_{c}$ with the type described above by composing with the
continuation $k$.

  * •

The term for $C_{r}$ has a link with the update of the value function after a
choice. Indeed, learner usually modify their value function after a choice (or
a sequence of choices). This can be seen as an update function of type
$\mathtt{Real}\times M\rightarrow M$, when we modify the memory (and thus the
value function) according to the reward. Here, using a log in the memory can
come in handy for most reinforcement learning algorithm to remember which
choice is being rewarded. It is then easy to see that, from this update
function, we can obtain a computation $C_{r}$ with the type described above by
composing with the continuation $k$.

However, the learner will also need additional information from the
environment, typically the current observable state or the list of available
actions for this state, that is why we can also use the operations of the
abstract interface in the computations $C_{c}$ and $C_{r}$.

####  4.3.2 Hiding the Memory of the Learner

The concept of this handler for the learner, which is typically a handler with
the state monad, is standard but it is not very practical. Indeed, in the type
$T\Rightarrow S_{M}(T)$ we can see that the handled computation needs an
initial memory, and the final memory is returned at the end of the
computation. However, this handled computation should be done in the main
program, and the user cannot provide an initial memory since it is not
supposed to know the actual type of memory. Similarly, there is no reason for
the user to have direct access to the memory of the learner, so this type $M$
should be hidden in the computation type. So, in practice, we want a handler
for the learner of type $T\Rightarrow T$ for any $T$. Fortunately, it is
possible to do this from the previous handler, and it is a standard way to
make the state invisible. Suppose that the learner provides an initial memory
$m_{i}$. Then, it can define the following handler (with the empty set of
handled operations):

$H_{\mathit{hide}}\equiv\mathbf{handler}~{}\\{\mathbf{return}~{}f\mapsto\mathbf{let}~{}x=f~{}m_{i}~{}\mathbf{in}~{}\pi_{2}(x)\\}$

with type $S_{M}(T)\Rightarrow T$ for any $T$. So, by composing this handler
with the previous one, we obtain a handler of type $T\Rightarrow T$, and the
memory becomes totally hidden from the user. This construction is a way to
mimic the $\mathbf{finally}~{}$clause of the EFF language, that we used in
Section 2, using the standard syntax of handler.

####  4.3.3 The Interface

As the previous handler uses additional algebraic operations (the one from the
interface), we need to handle them. Also, the previous handler is for the
operations $\mathtt{choice}_{\mathit{RL}}$ and $\mathtt{reward}_{\mathit{RL}}$
and we need to make the bridge between those operations and the one for the
main program: $\mathtt{choice}$ and $\mathtt{reward}$. We do this by defining
two handlers in $\lambda_{\mathit{eff}}^{I}$.

The first handler is a simple one, mainly abstracting the set of actions. For
this, we need to define a bijection $f:A_{\mathit{RL}}\rightarrow A_{E}$,
which is easy to do as they are both finite sets with the same size. Then, the
handler for abstracting actions is given by:

$\displaystyle
H_{\mathit{Act}}\equiv\mathbf{handler}~{}\\{\mathbf{return}~{}x$
$\displaystyle\mapsto\mathbf{return}~{}x,$ $\displaystyle\mathtt{choice}(k)$
$\displaystyle\mapsto\mathtt{choice}_{\mathit{RL}}(();x.k~{}(f~{}x))$
$\displaystyle\mathtt{reward}(r;k)$
$\displaystyle\mapsto\mathtt{reward}_{\mathit{RL}}(r;x.k~{}x)\\}$

With this handler $H_{\mathit{Act}}$, with type $T\Rightarrow T$ for any $T$,
we can go from the operations from the main program to the operation for the
learner. And now the only thing to do in order to successfully use the handler
defined by the learner is to define the handler for abstract interface. With
the interface we defined for this example, the two operations
$\mathtt{observe_{\mathit{RL}}}$ and $\mathtt{getactions_{\mathit{RL}}}$, then
the interface handler would look like:

$H_{I}\equiv\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto\mathbf{return}~{}x,\mathtt{observe}_{\mathit{RL}}(k)\mapsto
C_{o},\mathtt{getactions}_{\mathit{RL}}(o;k)\mapsto C_{a}\\}$

with

$k:O_{\mathit{RL}}\rightarrow T\vdash C_{o}:T\qquad
o:O_{\mathit{RL}},k:(A_{\mathit{RL}}~{}\mathtt{List})\rightarrow T\vdash
C_{a}:T$

so that the handler $H_{I}$ has type $T\Rightarrow T$ for any $T$. Those
computations may use the $\mathtt{observe}$ operation, and so with this
handler, that can depend on the environment, we can handle the computations
coming from the handler for the learner $H_{\mathit{RL}}$. Now, only two
operations remain to be handled $\mathtt{do}$ and $\mathtt{observe}$

####  4.3.4 The Environment

To handle the environment, we only need the types and functions of
$\lambda_{\mathit{eff}}^{E}$, without $\mathtt{reward}$ and $\mathtt{choice}$.
The handler for the environment should have the shape:

$H_{E}\equiv\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto
C_{r},\mathtt{observe}(k)\mapsto C_{o},\mathtt{do}(a;k)\mapsto C_{a}\\}$

such that this handler is typable with type $T\Rightarrow F(T)$ for any type
$T$ where $F(T)$ a transformation of $T$. The actual computations for this
handler depend strongly on the environment and so we cannot give additional
information for the general case. However, in order to illustrate this
handler, we show how to implement it in the case where we have a specific
model of the environment.

Suppose that we can model the environment by a type $E$ and two functions:
$Next_{E}:A_{E}\times E\rightarrow E$ and $Observe_{E}:E\rightarrow O$. This
may seem ad-hoc but it is in fact close to a Markov Decision Process which is
a common model for the environment in RL algorithm [34]. Indeed, in this case
the $Observe_{E}$ function corresponds to observing a reward and the current
state of the Markov Decision Process, and the $Next_{E}$ function corresponds
to moving in the MDP after an action in $A_{E}$. With those functions, we can
define the following handler for the environment:

$\displaystyle H_{E}\equiv\mathbf{handler}~{}\\{\mathbf{return}~{}x$
$\displaystyle\mapsto\lambda e.\mathbf{return}~{}(e,x),$
$\displaystyle\mathtt{observe}(k)$ $\displaystyle\mapsto\lambda
e.k~{}(Observe_{E}~{}e)~{}e$ $\displaystyle\mathtt{do}(a;k)$
$\displaystyle\mapsto k~{}()~{}(Next_{E}~{}(a,e))\\}$

with type $T\Rightarrow S_{E}(T)$ for any $T$. As we saw with the learner, it
is possible in this case to hide the type $E$ for the main program. This is
what we did for example in the description of the MAB environment in Section
2.

####  4.3.5 The Main Program with Handlers

And now, we can interpret all the four main operations for the main program.
Thus, given a computation $C$ in $\lambda_{\mathit{eff}}^{E}$, we can handle
all those operations with the computation:

$\mathbf{with}~{}H_{E}~{}\mathbf{handle}~{}(\mathbf{with}~{}H_{I}~{}\mathbf{handle}~{}(\mathbf{with}~{}H_{\mathit{RL}}~{}\mathbf{handle}~{}(\mathbf{with}~{}H_{\mathit{Act}}~{}\mathbf{handle}~{}C)))$

With this composition, that we could see in the main program of Section 2, we
obtain a handler of type $T\Rightarrow F(T)$ if the learner hides its memory
as explained before. And, with a complete model of the environment, by hiding
we can then obtain a type $T\Rightarrow T$.

##  5 Type Safety

In the previous section, we have introduced a core simply-typed calculus and
used it to implement our running example. The choice of the language was
driven by a simple goal: highlighting in the simplest way the _essential_
features needed to implement our functional approach to reinforcement learning
systems. The price we have to pay for such a simplicity is the lack of several
desirable guarantees on program behavior. In fact, functional programming
languages usually come endowed with expressive type systems — such as
polymorphic [32], linear [40, 6, 17], and graded [24] type systems — ensuring
the validity of nontrivial program properties at static time. Due to its
simple type discipline, our calculus offers only but a few guarantees on
program correctness, especially if one takes into account that the simplicity
of the type system is not reflected at the operational level, which is instead
characterised by highly expressive constructs, such as algebraic operations
and handlers.

In light of that, it is desirable to strengthen the power of the type system
defined in the previous section. Clearly, there are several possible
extensions we may look for, and it thus natural to ask what path we should
choose. In this section, we first identify three program properties well-known
in the field functional programming that we believe to be particularly
relevant when modelling reinforcement learning systems functionally, and then
outline how such properties could ensured by way of expressive type systems.
Let us begin with the target program properties.

  1. 1.

Locality of Operations. As a first property, we would like to ensure (families
of) algebraic operations to be used only in _specific parts of programs_. In
MAB, for instance, we would like the code describing the environment, i.e. the
slot machines, not to be able to perform the $\mathtt{choice}$ operation.

  2. 2.

Polymorphism. Secondly, we would like to ensure code to be as modular as
possible, this way enhancing its (re)usability. Concretely, that means having
some form of _polymorphism_ at disposal. This way, algorithms may be written
just once, the same code being called in many different environments, possibly
within the same program. In other words, the learner should use the types
$O_{\mathit{RL}}$ and $A_{\mathit{RL}}$ in a restricted way, the only relevant
information about them being that they are _finite_ types, whose values can
thus be enumerated. As an example, the naive algorithm we have presented in
Section 2 could be used in any context. In the particular case of MAB, we have
defined $O_{\mathit{RL}}$ as the unit type $\mathtt{Unit}$. However, we could
very well replaced $\mathtt{Unit}$ with any other _finite_ type, meaning that
our strategy scales to environments with more information.

  3. 3.

Linearity and Order. Finally, we would like force algebraic operations to be
performed _in a specified order_ , this way ensuring the learner to have all
the information it needs. Let us clarify this point with an example. In the
main program presented in Section 2, we see that the flow of information
follows a certain logic: for each iteration, we make a choice; we perform such
a choice in the environment; we observe its results; and, finally, we give the
reward. Such a logic is reflected in a specific execution order of algebraic
operation, and breaking such an order may lead the learner to obtain false
information.

Having isolated our target properties, we spend the rest of this section
outlining some possible ways to force such properties by means of type
systems. In particular, we focus on the use of type and effect systems [23],
polymorphism [32], and graded modal types [24].

###  5.1 Algebraic Operations and Effect Typing

Type and effect systems [23] endowed traditional type systems with annotations
giving information on what effects are produced during program execution. For
our purposes, we can build upon well-known effect typing systems keeping track
of which operations are handled during a computation [19]. Extending the
simple type system of Section 4 in this way, we can then ensure well-typed
programs to handle all their algebraic operations.

We now define effect typing for our core calculus and show how to take
advantage of such a typing in the context of a reinforcement learning problem.
We define an effect signature as a collection of operations and annotate the
type of handlers with those signatures. Formally, leave the the syntax of
terms as in Figure 2, but we replace the one of types as follows:

$\displaystyle T$
$\displaystyle::=\mathtt{B}\;\mbox{\Large{$\mid$}}\;\mathtt{Unit}\;\mbox{\Large{$\mid$}}\;T\times
T\;\mbox{\Large{$\mid$}}\;T\rightarrow^{E}T\;\mbox{\Large{$\mid$}}\;T\prescript{E}{}{\Rightarrow}^{E}T$
$\displaystyle E$ $\displaystyle::=\\{\mathtt{op}:T\rightsquigarrow T\\}\sqcup
E\;\mbox{\Large{$\mid$}}\;\emptyset$

Typing judgments for computations now are of the form $\Gamma\vdash_{E}C:T$,
with the informal reading that that $C$ has type $T$ in a context where the
only _unhandled_ algebraic operations $C$ can possibly perform are included in
$E$. Typing judgments for values, instead, remain the same (i.e. $\Gamma\vdash
V:T$), as values not being executed, they cannot perform any algebraic
operation at all. The inference system for our new typing judgment is given in
Figure 5.

$\Gamma,x:T\vdash x:T$ $\Gamma,x:T_{1}\vdash_{E}C:T_{2}$ $\Gamma\vdash\lambda
x.C:T_{1}\rightarrow^{E}T_{2}$ $\Gamma\vdash V_{1}:T_{1}$ $\Gamma\vdash
V_{2}:T_{2}$ $\Gamma\vdash(V_{1},V_{2}):T_{1}\times T_{2}$
$\Gamma\vdash():\mathtt{Unit}$ $c:\mathtt{B}\in\mathcal{C}$
$\Gamma\vdash\underline{c}:\mathtt{B}$
$f:\mathtt{B}_{1}\times\cdots\mathtt{B}_{n}\rightarrow\mathtt{B}\in\mathcal{F}$
$\Gamma\vdash\underline{f}:\mathtt{B}_{1}\times\cdots\mathtt{B}_{n}\rightarrow\mathtt{B}$
$E_{1}=\\{\mathtt{op}_{i}:T^{p}_{i}\rightsquigarrow T^{a}_{i}\mid 1\leq i\leq
n\\}\sqcup E_{f}\qquad E_{2}=E_{2}^{\prime}\sqcup E_{f}$
$(\Gamma,x:T_{i}^{p},k:T_{i}^{a}\rightarrow^{E_{2}}T_{c}\vdash_{E_{2}}C_{i}:T_{c})_{1\leq
i\leq n}\qquad\Gamma,x:T_{v}\vdash_{E_{2}}C_{r}:T_{c}$
$\Gamma\vdash\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto
C_{r},\mathtt{op}_{1}(x;k)\mapsto C_{1},\dots,\mathtt{op}_{n}(x;k)\mapsto
C_{n}\\}:T_{v}\prescript{E_{1}}{}{\Rightarrow}^{E_{2}}T_{c}$ $\Gamma\vdash
V:T$ $\Gamma\vdash_{E}\mathbf{return}~{}V:T$ $\Gamma\vdash V:T_{1}\times
T_{2}$ $\Gamma\vdash_{E}\pi_{i}(V):T_{i}$ $(\mathtt{op}:T_{p}\rightsquigarrow
T_{a})\in E$ $\Gamma\vdash V:T_{p}$ $\Gamma,x:T_{a}\vdash_{E}C:T$
$\Gamma\vdash_{E}\mathtt{op}(V;x.C):T$ $\Gamma\vdash_{E}C_{1}:T_{1}$
$\Gamma,x:T_{1}\vdash_{E}C_{2}:T_{2}$
$\Gamma\vdash_{E}\mathbf{let}~{}x=C_{1}~{}\mathbf{in}~{}C_{2}:T_{2}$
$\Gamma\vdash V_{1}:T_{2}\rightarrow^{E}T_{1}$ $\Gamma\vdash V_{2}:T_{2}$
$\Gamma\vdash_{E}V_{1}~{}V_{2}:T_{1}$ $\Gamma\vdash
V:T_{2}\prescript{E_{1}}{}{\Rightarrow}^{E_{2}}T_{1}$
$\Gamma\vdash_{E_{1}}C:T_{2}$
$\Gamma\vdash_{E_{2}}\mathbf{with}~{}V~{}\mathbf{handle}~{}C:T_{1}$

Figure 5: Typing Rules with Type Effects

The most important rule in Figure 5 is the one for handlers (cf. the typing
rule for open handlers by Kammar et al. [19]): it states that if a handler can
handle a subset of the available operations (denoted by
$\\{\mathtt{op}_{i}:T^{p}_{i}\rightsquigarrow T^{a}_{i}\mid 1\leq i\leq n\\}$
in Figure 5) and introduce some new operations in their computations
($E_{2}^{\prime}$), then the final set of free operations contains the
unhandled ones in the original set ($E_{f}$) together with the new operations
introduced by the handler.

This new type system satisfies better safety properties than the previous one.
In particular, it enjoys preservation (as the type system of previous section)
and progress.

######  Theorem 2.

Progress and preservation hold for the type system in Figure 5. That is:

  1. 1.

_Preservation._ If $\Gamma\vdash_{E}C:T$ and $C\rightarrow C^{\prime}$ then
$\Gamma\vdash_{E}C^{\prime}:T$.

  2. 2.

_Progress._ Suppose that all functions for base types are total for the
constants in the language. If $\vdash_{E}C:T$, then either there exists
$C^{\prime}$ such that $C\rightarrow C^{\prime}$, or $C$ has the shape
$\mathbf{return}~{}V$ for some $V$, or $C$ has the shape
$\mathtt{op}(V,x.C^{\prime})$ with $\mathtt{op}\in E$.

###### Proof.

We prove progress by induction on $C$. The use of typed effects is important
to keep track of what are exactly the set of operations that can appear, and
the commutation of $\mathtt{op}$ with $\mathbf{let}~{}$and
$\mathbf{handler}~{}$is also essential in this proof. The hypothesis on base
type functions ensures that an application of a base type function can always
be reduced. The case of $\mathbf{with}~{}H~{}\mathbf{handle}~{}C$ is the most
interesting one, by induction hypothesis and typing, there are four cases for
the computation $C$, either it can be reduced to $C^{\prime}$, and then we use
the first rule for handlers of Figure 4, either it is an operation
$\mathtt{op}\in E_{f}$ and we use the second rule, either it is a
$\mathbf{return}~{}V$ and we use the third rule, or it is an operation
$\mathtt{op}\in E_{1}/E_{f}$ and we use the fourth rule. ∎

######  Remark.

Even if we have focused on progress and preservation, it is worth mentioning
that that termination of the reduction relation can be proved using standard
methods [19].

We now have all the ingredients needed to encode the informal policies we
could build the MAB example upon. Let us define the following sets of effects:

$\displaystyle E_{E}$
$\displaystyle=\\{\mathtt{observe}:\mathtt{Unit}\rightsquigarrow
O_{E}~{};~{}\mathtt{do}:A_{E}\rightsquigarrow\mathtt{Unit}\\}$ $\displaystyle
E_{\mathit{RL}}$
$\displaystyle=\\{\mathtt{choice}:\mathtt{Unit}\rightsquigarrow
A_{E}~{};~{}\mathtt{reward}:\mathtt{Real}\rightsquigarrow\mathtt{Unit}\\}$
$\displaystyle E^{\mathit{Abs}}_{\mathit{RL}}$
$\displaystyle=\\{\mathtt{choice}_{\mathit{RL}}:\mathtt{Unit}\rightsquigarrow
A_{\mathit{RL}}~{};~{}\mathtt{reward}_{\mathit{RL}}:\mathtt{Real}\rightsquigarrow\mathtt{Unit}\\}$
$\displaystyle E^{\mathit{Abs}}_{I}$
$\displaystyle=\\{\mathtt{observe}_{\mathit{RL}}:\mathtt{Unit}\rightsquigarrow
O_{\mathit{RL}}~{};~{}\mathtt{getactions}:O_{\mathit{RL}}\rightsquigarrow
A_{\mathit{RL}}~{}\mathtt{List}~{};~{}\cdots\\}$

These are, respectively, the set of effects for the environment, the learner
seen by the environment, the learner seen by the learner, and the interface
used by the learner.

##### The Learner

The handler $H_{\mathit{RL}}$ for the learner should have the type

$\vdash
H_{\mathit{RL}}:T\prescript{E_{\mathit{RL}}^{\mathit{Abs}}}{}{\Rightarrow}^{E_{I}^{\mathit{Abs}}}S_{M}(T),$

where $T$ is any type and $S_{M}(T)\equiv M\rightarrow M\times T$. This means
that the learner handles the operations $\mathtt{choice}_{\mathit{RL}}$ and
$\mathtt{reward}_{\mathit{RL}}$ using only the operations in the interface
$E^{\mathit{Abs}}_{I}$. Thus, with this type, we ensure that the learner does
not have a direct access to the environment, and it only sees effects for the
abstract types $A_{\mathit{RL}}$ and $O_{\mathit{RL}}$ and not the concrete
types $O_{E}$ and $A_{E}$. Then, with hiding, we can obtain a handler of type
$T\prescript{E_{\mathit{RL}}^{\mathit{Abs}}}{}{\Rightarrow}^{E_{I}^{\mathit{Abs}}}T$
as long as the learner provides an initial memory. Notice that in this hiding
handler of type
$T\prescript{E_{I}^{\mathit{Abs}}}{}{\Rightarrow}^{E_{I}^{\mathit{Abs}}}T$,
the initial memory can depend on the abstract interface, this being useful in
those cases in which some parameters in the initial memory have to be exposed.

##### The Interface

The interface is separated into two handlers: $H_{\mathit{Act}}$ and $H_{I}$.
This first handler is only a bridge between abstract actions and concrete
actions. It is not difficult to see that the former should have the type:

$\vdash
H_{\mathit{Act}}:T\prescript{E_{\mathit{RL}}}{}{\Rightarrow}^{E_{\mathit{RL}}^{\mathit{Abs}}}T,$

for any type $T$, thus handling the operations $\mathtt{choice}$ and
$\mathtt{reward}$ seen from the exterior to the internal one of the learner.
As for the interface, it should be a bridge between the environment and
learner abstracted by the user, so it should have the type:

$\vdash H_{I}:T\prescript{E_{I}^{\mathit{Abs}}\sqcup
E_{E}}{}{\Rightarrow}^{E_{E}}T,$

where the fixed set of operations ($E_{f}$ in the rule) would be $E_{E}$.

##### The Environment

As for the environment, the handler only has to handle the two operations
$\mathtt{observe}$ and $\mathtt{do}$, without using the learner nor the
interface. So, it should have the type:

$\vdash H_{E}:T\prescript{E_{E}}{}{\Rightarrow}^{\emptyset}F(T).$

####  5.1.1 Composition of Handlers and Main Program

Now that we have types for each of the four handlers needed, we compose them.
An important point of our effect typing is that it supports weakening: in the
handler rule, we can always take a larger set $E_{f}$, so that we are licensed
to use the handler in different contexts.333This is one of the main reasons
why this rule is very useful to achieve polymorphism. In our case, it means
that we can give the following types to handlers:

$\displaystyle\vdash H_{\mathit{RL}}$
$\displaystyle:T\prescript{E_{\mathit{RL}}^{\mathit{Abs}}\sqcup
E_{E}}{}{\Rightarrow}^{E_{I}^{\mathit{Abs}}\sqcup E_{E}}T$
$\displaystyle\vdash H_{\mathit{Act}}$
$\displaystyle:T\prescript{E_{\mathit{RL}}\sqcup
E_{E}}{}{\Rightarrow}^{E_{\mathit{RL}}^{\mathit{Abs}}\sqcup E_{E}}T$
$\displaystyle\vdash H_{I}$
$\displaystyle:T\prescript{E_{I}^{\mathit{Abs}}\sqcup
E_{E}}{}{\Rightarrow}^{E_{E}}T$ $\displaystyle\vdash H_{E}$
$\displaystyle:T\prescript{E_{E}}{}{\Rightarrow}^{\emptyset}F(T).$

Consequently, we can compose them to obtain:

$H_{E}\circ H_{I}\circ H_{\mathit{RL}}\circ
H_{\mathit{Act}}:T\prescript{E_{\mathit{RL}}\sqcup
E_{E}}{}{\Rightarrow}^{\emptyset}F(T).$

When we have a model of the environment, with hiding, we have

$H_{E}\circ H_{I}\circ H_{\mathit{RL}}\circ
H_{\mathit{Act}}:T\prescript{E_{\mathit{RL}}\sqcup
E_{E}}{}{\Rightarrow}^{\emptyset}T.$

This shows that the main program can use the four main effects, as expected.
Without hiding, we would have a type which is essentially the composition of
the two state monads on $E$ and $M$, meaning that the program should be
understood in a context with both an environment and a memory for the learner.

###  5.2 Polymorphism

The typing rule for handlers allows us to assign handlers arbitrary types $T$.
To ensure such types not to be inspected by programs, and to ensure uniqueness
of typing derivation of handlers, it is natural to extend our type system with
polymorphic types. Moreover, the base types we presented for the language,
$A_{\mathit{RL}},O_{\mathit{RL}},A_{E}$ and $O_{E}$ all depend on the actual
environment, whereas we expect the handler $H_{\mathit{RL}}$ for the learner
not to do so. Consequently, we may rely on polymorphism to enforce
$A_{\mathit{RL}}$ and $O_{\mathit{RL}}$ not to be inspected, this way giving a
unique polymorphic type to the handler $H_{\mathit{RL}}$ and thus ensuring the
latter to be usable in any environment.

Languages, however, can be polymorphic in may ways: especially in presence of
effects. We now outline what kind of polymorphism is needed for our purposes.
As a first requirement, we need to be able to declare polymorphic handlers;
write their implementation once and for all; and then use them in different
contexts. To do that, we believe having handlers as first-class citizen of the
language, as we presented in Figure 2, is necessary. Secondly, we also want to
declare polymorphic effects, so to give a sense to those polymorphic handlers.

We take as an inspiration the language by Biernacki et al. [8]. However, since
the aforementioned language does not consider handlers as first-class
citizens, we cannot directly rely on that. In the rest of this section, we
informally outline a possible polymorphic type assignment for our language,
leaving its formal definition and analysis (such as type soundness) as future
work.

We consider different kinds, starting from the base kinds of types, effects,
and rows, and building complex kinds using a functional arrow. Formally, kinds
are generated by the following grammar:

$\kappa:=T\;\mbox{\Large{$\mid$}}\;E\;\mbox{\Large{$\mid$}}\;R\;\mbox{\Large{$\mid$}}\;\kappa\rightarrow\kappa.$

A row $\rho$ is a sequence of effects $\langle E_{1}\mid\rho^{\prime}\rangle$,
with intuitively the same meaning as effect signature in our last type system,
the main difference being that we can have polymorphism on row, and an effect
can appear several time in a row (but possibly with different instantiation of
their polymorphic types). We would like to write, as in [8], the following
computation:

$\mathbf{effect}~{}E_{\mathit{RL}}^{\mathit{Abs}}=\forall\alpha_{A}::T.\\{\mathtt{choice}_{\mathit{RL}}:\mathtt{Unit}\rightsquigarrow\alpha_{A};\mathtt{reward}_{\mathit{RL}}:\mathtt{Real}\rightsquigarrow\mathtt{Unit}\\}~{}\mathbf{in}~{}\cdots$

declaring a new effect, called $E_{\mathit{RL}}^{\mathit{Abs}}$, waiting for a
type $\alpha_{A}$ representing the type (of kind $T$) of actions, and then
declare the types of those two algebraic operations. The kind of
$E_{\mathit{RL}}^{\mathit{Abs}}$ would then be $T\rightarrow E$, so given a
type of kind $T$ this indeed gives an effect of kind $E$. Similarly, the
abstract interface would be declared with:

$\mathbf{effect}~{}E_{I}^{\mathit{Abs}}=\forall\alpha_{A}::T,\alpha_{O}::T.\\{\mathtt{observe}_{\mathit{RL}}:\mathtt{Unit}\rightsquigarrow\alpha_{O};\mathtt{getactions}_{\mathit{RL}}:\alpha_{O}\rightsquigarrow\alpha_{A}~{}\mathtt{List};\cdots\\}$

And then, in this context, the type of the handler for the learner,
$H_{\mathit{RL}}$ would be, after hiding:

$H_{\mathit{RL}}:\forall\alpha_{A}::T,\alpha_{O}::T,\alpha_{T}::T,\rho::R.\alpha_{T}\prescript{\langle
E_{\mathit{RL}}^{\mathit{Abs}}~{}\alpha_{A}\mid\rho\rangle}{}{\Rightarrow}^{\langle
E_{I}^{\mathit{Abs}}~{}\alpha_{A}~{}\alpha_{O}\mid\rho\rangle}\alpha_{T}$

meaning that for any type of actions $\alpha_{A}$, any type of observations
$\alpha_{O}$, any type of computation $\alpha_{T}$ and any effect environment
$\rho$, the handler for the learner has an identity type on the computation,
handling the operations in $E_{\mathit{RL}}^{\mathit{Abs}}~{}\alpha_{A}$ and
introducing the new operations of
$E_{I}^{\mathit{Abs}}~{}\alpha_{A}~{}\alpha_{O}$. In practice, we would like
$\alpha_{A}$ and $\alpha_{O}$ to always represent base types, and especially
finite sets, so we would need some more restriction on this polymorphism. But
informally, this is the shape of type we would like for the handler written by
the learner, as it ensures that it can be used in any environment without
modifications. Notice that in order to do this, we want handlers as first-
class citizens but we do not need the full power of polymorphism since the
algebraic operations themselves do not need to be polymorphic. This kind of
polymorphism that we need differs slightly from the polymorphism mainly
studied in the literature: usually, it allows the programmer to use different
handlers for the same operation, however what we want in our case is to use a
unique handler for different contexts.

###  5.3 Imposing an Order on Operations

Our last property of interest focuses on linearity and order of algebraic
operations. For instance, we would like to ensure that when a call to
$\mathtt{choice}$ is made, it is always followed by a $\mathtt{do}$ and a
$\mathtt{reward}$ ($\mathtt{observe}$ can be useful to give the reward but it
is not mandatory as it should have no effect on the environment). We now
outline how such a goal can be achieved in presence of algebraic operations
relying on suitable graded type systems [20]. Such an approach, however, is
not readily extendable to effect handlers. As far as we know, graded types
have not been extended to handlers.

Informally, we define a monoid on algebraic operations and associate each
computation to an element of this monoid, the latter giving information on the
operations executed during program evaluation. Sequential composition of
computations corresponds to monoid multiplication, basic computations to the
unit of the monoid, and algebraic operations to the corresponding elements of
the monoid. A typing rule (for computations) then has shape
$\Gamma\vdash_{E}C:T;m$, where $m$ is an element of the monoid with, for
example, the following rules:

$\Gamma\vdash V:T$ $\Gamma\vdash_{E}\mathbf{return}~{}V:T;1$
$\Gamma\vdash_{E}C_{1}:T_{1};m_{1}$
$\Gamma,x:T_{1}\vdash_{E}C_{2}:T_{2};m_{2}$
$\Gamma\vdash_{E}\mathbf{let}~{}x=C_{1}~{}\mathbf{in}~{}C_{2}:T_{2}:m_{1}\cdot
m_{2}$

$(\mathtt{op}:T_{p}\rightsquigarrow T_{a})\in E$ $\Gamma\vdash V:T_{p}$
$\Gamma,x:T_{a}\vdash_{E}C:T;m$
$\Gamma\vdash_{E}\mathtt{op}(V;x.C):T;m_{\mathtt{op}}\cdot m$

where $1$ is the unit of the monoid, $m_{1}\cdot m_{2}$ is monoid
multiplication and $m_{\mathtt{op}}$ is the element of the monoid
corresponding to the operation $\mathtt{op}$.

In our case, the monoid would be the free monoid on the three element
associated to the algebraic operations $\mathtt{choice},\mathtt{do}$ and
$\mathtt{reward}$, with $\mathtt{observe}$ confounded with the unit of the
monoid, with the following equation

$\displaystyle m_{\mathtt{choice}}\cdot m_{\mathtt{do}}\cdot
m_{\mathtt{reward}}=1$

and then, we would like the main program to be associated to an element of
this monoid with the shape $m_{\mathtt{do}}^{n}$. With this, we can ensure
that, if we forget about $\mathtt{observe}$ since it has no effect at all,
then any $\mathtt{choice}$ is always followed by exactly one $\mathtt{do}$ and
one $\mathtt{reward}$. Moreover, only the $\mathtt{do}$ operation can be done
outside of this loop, because essentially the user can make choices without
calling the learner, and for the point of view of the learner then the user
would just be a part of the transition function of the environment.

However, this method, which is standard for effects, does not generalise well
in presence of handlers. Indeed, we need to take into account the potentially
new operations introduced by a handler, and intuitively the handler would then
represent a map from the new operations to an element of the monoid. For a
very simple example, consider the operation
$\mathtt{choicedoandobserve}:1\rightsquigarrow A_{E}\times O_{E}$ with the
handler

$\mathbf{handler}~{}\\{\mathbf{return}~{}x\mapsto
x;\mathtt{choicedoandobserve}(k)\mapsto\mathtt{choice}(a.\mathtt{do}(a;\\_.\mathtt{observe}(o.k~{}(a,o))))\\}$

doing the three operations $\mathtt{choice}$, $\mathtt{do}$ and
$\mathtt{observe}$ in sequence. Then, this handler should be typed with the
information that the new operation $\mathtt{choicedoandobserve}$ is associated
to the element $m_{\mathtt{choice}}\cdot m_{\mathtt{do}}\cdot
m_{\mathtt{observe}}$.

We believe such a type system should be feasible, but we have no concrete
formalization of this. So, as for polymorphism, those kind of type system
would be desirable for safety but we leave the formalization to future work.

##  6 Related Work

The interaction between programming language theory and machine learning is an
active and flourishing research area. Arguably, the current, most well-
established products of such an interaction are the so-called Bayesian [36,
37, 35, 9, 11] and differentiable [7, 3] programming languages, and their
associated theories [18, 39, 1, 25, 33].

Choice-based operations are not new in programming language theory, as they
first appeared in the context of computational effects (more specifically,
choice operations has been first studied as nondeterministic choices [21]).
However, their integration with reward constructs as a way to structure
machine learning systems as data-driven, decision-making processes is quite
recent. As an example of that, the programming language SmartChoice [10]
integrates choice and rewards operations with traditional programming
constructs. To the best of the authors’ knowledge, the first work dealing with
semantic foundations for choice-based programming languages is the recent work
by Abadi and Plotkin [2]. There, a modular approach to higher-order choice-
based programming languages is developed in terms of the selection monad [14,
16, 15] and its algebraic operations [27, 26, 28], both at the level of
operational and denotational semantics. As such, that work is the closest to
ours.

The results presented in this paper has been obtained starting from an
investigation of possible applications of the aforementioned work by Abadi and
Plotkin to modelling reinforcement learning systems. We have explained in
Section 3 why, when dealing with reinforcement learning, moving from the
selection to the state monad is practically beneficial. From a theoretical
point of view, such a shift can be seen as obtained by looking at comodels
[30] of choice operations, which directly leads to view reinforcement learning
algorithms as ultimately defining stateful runners [38, 4] for such
operations, and thus as generic effects [26] for the state monad. Following
this path, we have consequently relied on handlers [29, 5, 31] to define
modular implementations of such generic effects, and thus of reinforcement
learning algorithms. Even if handlers and algebraic operations are well-known
tools in functional programming, to the best of our knowledge the present work
is the first one investigating their application to modelling reinforcement
learning systems.

Finally, we mention that applications of functional programming techniques in
the context of machine learning similar in spirit to ones investigated in this
work, as well as in the work by Abadi and Plotkin [2], have been proposed [12]
in terms of induction and abduction constructs, rather than in terms of
choices and rewards

##  7 Conclusion

In this article, we address the problem of implementing reinforcement learning
algorithms within a functional programming language. The starting idea is to
manage the interaction between the three involved agents (namely the learner,
the user, and the environment) through a set of algebraic operations and
handlers for them. This way, a certain degree of modularity is guaranteed.

The path we followed starts from practice, i.e. from the implementation of
these ideas in a concrete language such as EFF, and then progressively moves
towards theory, i.e. towards the study of a paradigmatic language for effects
and handlers in which these ideas can be formalized, thus becoming an object
of study. Technically, the most important contribution of this work lies in
highlighting where the state of the art is deficient with respect to the type
of type safety and code reuse properties that one would like.

Some ideas for future works can be sought precisely in the direction just
mentioned and, in particular, in the definition of systems of types
sufficiently powerful to guarantee that the algebraic operations involved are
actually carried out in the good order, or that they allow the right level of
polymorphism.

An alternative to powerful type systems for some safety properties could also
be the use of some advanced features of programming language for abstraction.
For example, we presented the abstract interface as a handler, with a learner
polymorphic in the types of actions and observation. In OCAML, an alternative
could be to use modules and signatures: an abstract interface would be
represented by a signature, with abstract data types for actions and
observations, and additional functions to replace the operations. The learner
would then have access to elements of this signature, and the user would need
to implement an actual module respecting this signature in order to use the
learning algorithm. This way, the fact that the learner can be written
independently from the environment would come from the OCAML abstraction,
instead of polymorphism in a type and effect system.

## References

  * Abadi and Plotkin [2020] M. Abadi and G. D. Plotkin.  A simple differentiable programming language.  _Proc. ACM Program. Lang._ , 4(POPL):38:1–38:28, 2020.
  * Abadi and Plotkin [2021] M. Abadi and G. D. Plotkin.  Smart choices and the selection monad.  In _36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021_ , pages 1–14, 2021\.  doi: 10.1109/LICS52264.2021.9470641.
  * Abadi et al. [2016] M. Abadi, P. Barham, J. Chen, Z. Chen, A. Davis, J. Dean, M. Devin, S. Ghemawat, G. Irving, M. Isard, M. Kudlur, J. Levenberg, R. Monga, S. Moore, D. G. Murray, B. Steiner, P. A. Tucker, V. Vasudevan, P. Warden, M. Wicke, Y. Yu, and X. Zheng.  Tensorflow: A system for large-scale machine learning.  In _12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016_ , pages 265–283, 2016.
  * Ahman and Bauer [2020] D. Ahman and A. Bauer.  Runners in action.  In _Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings_ , pages 29–55, 2020.  doi: 10.1007/978-3-030-44914-8\\_2.
  * Bauer and Pretnar [2015] A. Bauer and M. Pretnar.  Programming with algebraic effects and handlers.  _J. Log. Algebr. Meth. Program._ , 84(1):108–123, 2015.
  * Benton and Wadler [1996] P. N. Benton and P. Wadler.  Linear logic, monads and the lambda calculus.  In _Proc. of LICS 1996_ , pages 420–431, 1996.  doi: 10.1109/LICS.1996.561458.
  * Bergstra et al. [2010] J. Bergstra, O. Breuleux, F. Bastien, P. Lamblin, R. Pascanu, G. Desjardins, J. Turian, D. Warde-farley, and Y. Bengio.  Theano: A cpu and gpu math compiler in python.  In _Proceedings of the 9th Python in Science Conference_ , pages 3–10, 2010.
  * Biernacki et al. [2019] D. Biernacki, M. Piróg, P. Polesiuk, and F. Sieczkowski.  Abstracting algebraic effects.  _Proc. ACM Program. Lang._ , 3(POPL), 2019.
  * Bingham et al. [2019] E. Bingham, J. P. Chen, M. Jankowiak, F. Obermeyer, N. Pradhan, T. Karaletsos, R. Singh, P. A. Szerlip, P. Horsfall, and N. D. Goodman.  Pyro: Deep universal probabilistic programming.  _J. Mach. Learn. Res._ , 20:28:1–28:6, 2019.
  * Carbune et al. [2019] V. Carbune, T. Coppey, A. Daryin, T. Deselaers, N. Sarda, and J. Yagnik.  Predicted variables in programming, 2019.
  * Carpenter et al. [2017] B. Carpenter, A. Gelman, M. D. Hoffman, D. Lee, B. Goodrich, M. Betancourt, M. Brubaker, J. Guo, P. Li, and A. Riddell.  Stan: A probabilistic programming language.  _Journal of Statistical Software_ , 76(1):1–32, 2017.  doi: 10.18637/jss.v076.i01.
  * Cheung et al. [2018] S. Cheung, V. Darvariu, D. R. Ghica, K. Muroya, and R. N. S. Rowe.  A functional perspective on machine learning via programmable induction and abduction.  In J. P. Gallagher and M. Sulzmann, editors, _Proc. of FLOPS_ , volume 10818 of _Lecture Notes in Computer Science_ , pages 84–98. Springer, 2018.  doi: 10.1007/978-3-319-90686-7\\_6.
  * Dal Lago et al. [2022] U. Dal Lago, F. Gavazzo, and A. Ghyselen.  Source Code in EFF.  https://github.com/GhyselenAlexis/GhyselenAlexis.github.io/tree/main/EFF, 2022\.
  * Escardó and Oliva [2010] M. H. Escardó and P. Oliva.  The peirce translation and the double negation shift.  In _Proc. of CiE 2010_ , pages 151–161, 2010.  doi: 10.1007/978-3-642-13962-8\\_17.
  * Escardó and Oliva [2012] M. H. Escardó and P. Oliva.  The peirce translation.  _Ann. Pure Appl. Log._ , 163(6):681–692, 2012\.  doi: 10.1016/j.apal.2011.11.002.
  * Escardó et al. [2011] M. H. Escardó, P. Oliva, and T. Powell.  System T and the product of selection functions.  In _Proc. of CSL 2011_ , pages 233–247, 2011.  doi: 10.4230/LIPIcs.CSL.2011.233.
  * Ghica and Smith [2014] D. R. Ghica and A. I. Smith.  Bounded linear types in a resource semiring.  In _Proc. of ESOP 2014_ , pages 331–350, 2014.  doi: 10.1007/978-3-642-54833-8\\_18.
  * Goodman [2013] N. D. Goodman.  The principles and practice of probabilistic programming.  In _Proc. of POPL ’13_ , pages 399–402, 2013.  doi: 10.1145/2429069.2429117.
  * Kammar et al. [2013] O. Kammar, S. Lindley, and N. Oury.  Handlers in action.  In _Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming_ , ICFP ’13, page 145–158, New York, NY, USA, 2013\. Association for Computing Machinery.
  * Katsumata [2014] S.-y. Katsumata.  Parametric effect monads and semantics of effect systems.  In _Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ , pages 633–645, 2014.
  * McCarthy [1961] J. McCarthy.  A basis for a mathematical theory of computation, preliminary report.  In _Papers presented at the 1961 western joint IRE-AIEE-ACM computer conference, IRE-AIEE-ACM 1961 (Western), Los Angeles, California, USA, May 9-11, 1961_ , pages 225–238, 1961.  doi: 10.1145/1460690.1460715.
  * Moggi [1988] E. Moggi.  _Computational Lambda-calculus and Monads_.  University of Edinburgh, Department of Computer Science, 1988.
  * Nielson and Nielson [1999] F. Nielson and H. R. Nielson.  Type and effect systems.  In _Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel)_ , pages 114–136, 1999.
  * Orchard et al. [2019] D. Orchard, V.-B. Liepelt, and H. Eades III.  Quantitative program reasoning with graded modal types.  _Proc. ACM Program. Lang._ , 3(ICFP):110:1–110:30, 2019.  doi: 10.1145/3341714.
  * Pearlmutter and Siskind [2008] B. A. Pearlmutter and J. M. Siskind.  Reverse-mode AD in a functional framework: Lambda the ultimate backpropagator.  _ACM Trans. Program. Lang. Syst._ , 30(2):7:1–7:36, 2008.
  * Plotkin and Power [2003] G. Plotkin and J. Power.  Algebraic operations and generic effects.  _Applied Categorical Structures_ , 11:69–94, 2003.  https://doi.org/10.1023/A:1023064908962.
  * Plotkin and Power [2001] G. D. Plotkin and J. Power.  Adequacy for algebraic effects.  In _Proc. of FOSSACS 2001_ , pages 1–24, 2001.  doi: 10.1007/3-540-45315-6\\_1.
  * Plotkin and Power [2002] G. D. Plotkin and J. Power.  Notions of computation determine monads.  In _Proc. of FOSSACS 2002_ , pages 342–356, 2002.
  * Plotkin and Pretnar [2013] G. D. Plotkin and M. Pretnar.  Handling algebraic effects.  _Logical Methods in Computer Science_ , 9(4), 2013.
  * Power and Shkaravska [2004] A. J. Power and O. Shkaravska.  From comodels to coalgebras: State and arrays.  In _Proceedings of the Workshop on Coalgebraic Methods in Computer Science, CMCS 2004, Barcelona, Spain, March 27-29, 2004_ , pages 297–314, 2004.  doi: 10.1016/j.entcs.2004.02.041.
  * Pretnar [2015] M. Pretnar.  An introduction to algebraic effects and handlers. invited tutorial paper.  _Electronic notes in theoretical computer science_ , 319:19–35, 2015.
  * Reynolds [1983] J. Reynolds.  Types, abstraction and parametric polymorphism.  In _IFIP Congress_ , pages 513–523, 1983.
  * Siskind and Pearlmutter [2008] J. M. Siskind and B. A. Pearlmutter.  Nesting forward-mode AD in a functional framework.  _Higher-Order and Symbolic Computation_ , 21(4):361–376, 2008.
  * Sutton and Barto [2018] R. S. Sutton and A. G. Barto.  _Reinforcement Learning: An Introduction_.  MIT press, 2018.
  * Tolpin et al. [2016] D. Tolpin, J.-W. van de Meent, H. Yang, and F. Wood.  Design and implementation of probabilistic programming language anglican.  In _Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages_ , IFL 2016, pages 6:1–6:12, 2016\.
  * Tran et al. [2016] D. Tran, A. Kucukelbir, A. B. Dieng, M. Rudolph, D. Liang, and D. M. Blei.  Edward: A library for probabilistic modeling, inference, and criticism.  _arXiv preprint arXiv:1610.09787_ , 2016.
  * Tran et al. [2017] D. Tran, M. D. Hoffman, R. A. Saurous, E. Brevdo, K. Murphy, and D. M. Blei.  Deep probabilistic programming.  In _International Conference on Learning Representations_ , 2017.
  * Uustalu [2015] T. Uustalu.  Stateful runners of effectful computations.  In _The 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25, 2015_ , pages 403–421, 2015.  doi: 10.1016/j.entcs.2015.12.024.
  * van de Meent et al. [2018] J. van de Meent, B. Paige, H. Yang, and F. Wood.  An introduction to probabilistic programming.  _CoRR_ , abs/1809.10756, 2018.  URL http://arxiv.org/abs/1809.10756.
  * Wadler [1990] P. Wadler.  Linear types can change the world!  In _Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990_ , page 561, 1990.