This is a framework for generic composable effectful asynchronous programming
basically using only objects and polymorphic variants.
Ability to write
"monad generic code".
Functors, Applicatives, Monads, ...
Extensible environment or reader.
Laziness via η-expansion.
Inferred checked exception handing.
Extensible with user defined effects.
Plays well with type inference allowing relatively concise code.
Interoperable with existing monadic libraries.
More specifically, this uses a
with the signatures specified using objects and a
higher-kinded type encoding. Programs can
be written against abstract generic interfaces allowing the same program to be
executed with multiple interpreters. Interpreters are implemented as objects and
passed via the reader pattern. Polymorphic variants can be used for errors. The
end result is a system that provides a variety of effects (environment, checked
exceptions, asynchronicity, ...) à la carte.
This library requires OCaml version 4.08 or later for
binding operators and some other
convenience features, but it seems a library like this could have already been
written for OCaml 3.
The following subsections introduce some aspects of the Rea framework via simple
examples. The code snippets are also extracted as a
test to ensure that they are accurate.
Let's look at a rather familiar example, the implementation of a naïve
exponential time Fibonacci function as an effectful computation. We use such a
trivial example in order to focus on some of the basics of the Rea framework. It
is assumed that the reader has basic familiarity with monads and the like. If
not, rest assured, there is
no shortage of material introducing monads
on the Internet.
To use the framework, we just
Rea module, which brings a lot of
generic combinators to scope:
And here is a naïvely written eager Fibonacci function implementation using the
lift'2 combinators from the framework:
let rec eager_fib n = if n <= 1 then pure n else lift'2 ( + ) (eager_fib (n - 2)) (eager_fib (n - 1))
return combinator should already be familiar to you. The
lift'2 combinator (sometimes called
map2) combinator takes an ordinary
function of two plain value arguments and returns a function that works on
effectful computations. In this case, the
+ operator is used to combine the
results of the two recursive Fibonacci computations as a computation.
The below definition shows the type inferred for
eager_fib (after renaming
some type variables to match what is used in the Rea framework):
let _ = (eager_fib : int -> (< map' : 'e 'a 'b. ('b -> 'a) -> ('R, 'e, 'b, 'D) er -> ('R, 'e, 'a) s ; pair' : 'e 'a 'b. ('R, 'e, 'a, 'D) er -> ('R, 'e, 'b, 'D) er -> ('R, 'e, 'a * 'b) s ; pure' : 'e 'a. 'a -> ('R, 'e, 'a) s ; .. > as 'D) -> ('R, 'e, int) s)
The above undoubtedly looks rather complicated. We can simplify it by using type
abbreviations (class types) that are used in the definition of the framework
itself. In particular, each of the methods
above are defined by classes of the same name and each of those classes takes
two type parameters
let _ = (eager_fib : int -> (< ('R, 'D) map' ; ('R, 'D) pair' ; ('R, 'D) pure' ; .. > as 'D) -> ('R, 'e, int) s)
The curious recursive use of the
'D type parameter makes sure that all of the
individual elements of the combined type agree on the type of the whole
Why do the class names have an apostrophe at the end? IOW, why
map' instead of
map? Well, there are lots of such a classes, multiple are often used in
type signatures, and they tend to have fairly common names. The apostrophe is
there to allow the classes to be conveniently at the top level of the
module with reduced risk of naming collisions with other libraries.
Recall that we used two combinators
lift'2 from the framework in
eager_fib function. Obviously
pure corresponds to or requires the
lift'2 requires both of the
pair' classes. OCaml
conveniently infers the required combination for us.
We can simplify the type further. The combination of
pure' is well known. That combination is the signature of the so called
applicative functor. The Rea library defines the abbreviation
a class) for the combination:
let _ = (eager_fib : int -> (('R, 'D) #applicative' as 'D) -> ('R, 'e, int) s)
We are not quite done yet. Ignore the
int ->. The remaining part of the type
is of the form
'D -> ('R, 'e, 'a) s. This is the type of "effect readers" of
('R, 'e, 'a, 'D) er type which is actually the main abstraction of the Rea
framework. Combinators in the Rea framework take effect readers as arguments and
return effect readers as results. So, we end up with the following equivalent
let _ = (eager_fib : int -> ('R, 'e, int, (('R, 'D) #applicative' as 'D)) er)
Let's discuss the general form of the effect reader type
('R, 'e, 'a, 'D) er.
The type has four type arguments:
'Rrepresents a higher-kinded abstract type constructor that is specific to
a particular representation of effects.
'eis the type of errors or failures that may be signaled during
interpretation of the effect reader.
'ais the type of answers or results of the effect reader in case it does
not signal an error.
'Dis the type of the dictionary of capabilities or of the environment
required by the effect reader. In other words, it is the type of the effect
('R, +'e, +'a) s type we saw earlier is the abstract effect signature
type. It represents the application
('e, 'a) 'R of the higher-kinded
constructor to the
Now, let's interpret the effect reader type of our Fibonacci function:
('R, 'e, int, (('R, 'D) #applicative' as 'D)) er
First of all, we can see that it returns an
int in case it does not fail with
an error. Speaking of which, the type of errors is
'e, which, due to
parametricity, means that it cannot produce errors. In other words, we (and the
OCaml type system) statically know that it cannot fail. The representation
'R is also parametric, which means that it does not
require a specific representation. The dictionary type
'D is also parametric
and must be a subtype of
applicative'. In other words, we can run the effect
reader with any interpreter that implements the
For example, we can use the identity monad implementation provided by the Rea
let () = assert (55 = Identity.of_rea (run Identity.monad (eager_fib 10)))
The identity monad does not perform any effects per se and the values computed
during interpretation are not wrapped. In other words, with the identity monad,
('R, 'e, 'a) s is equivalent to
'a. This equivalence is witnessed by a pair
of identity functions
Identity.to_rea. By itself, the
identity monad cannot support the error handling effects of the Rea framework
nor it can support asynchronous computations. It may seem like a useless
interpreter, but it actually has many interesting applications.
run function used above just passes the interpreter to the computation.
One could also just write
eager_fib 10 Identity.monad.
let () = assert (`Ok 55 = Tailrec.run Tailrec.sync (eager_fib 10))
The tail recursive interpreter provides both a synchronous, as seen above, and
an asynchronous interpreter and also supports error handling. The Rea framework
also provides a number of other interpreter implementations, that we could use
here, but let's move on.
At the beginning we mentioned that the
eager_fib function is written naïvely.
The problem with it is that it is eager: as soon as the first argument is passed
to it, a whole tree of suspended computations is built.
Now, we saw that the result of
eager_fib n is actually a function —
namely an effect reader. Because it is a function, we can use (eta) η-expansion
to make it lazy. For this purpose the Rea framework provides a simple
function that takes a thunk and returns a single parameter function. Using
eta'0 we can write an η-expanded Fibonacci function as follows:
let rec fib n = eta'0 @@ fun () -> if n <= 1 then pure n else lift'2 ( + ) (fib (n - 2)) (fib (n - 1))
eager_fib functions have exactly the same types. The difference
is that the η-expanded
fib function returns in O(1) time with a function
fib n = fun d -> ...
eager_fib function builds a complete computation tree
eager_fib 0 = pure 0 eager_fib 1 = pure 1 eager_fib 2 = lift'2 (+) (pure 0) (pure 1) eager_fib 3 = lift'2 (+) (pure 1) (lift'2 (+) (pure 0) (pure 1)) eager_fib 4 = lift'2 (+) (lift'2 (+) (pure 0) (pure 1)) (lift'2 (+) (pure 1) (lift'2 (+) (pure 0) (pure 1))) ...
taking exponential time and space.
Of course, when either one of the effect readers is interpreted, it will take
exponential time due to the naïve exponential Fibonacci algorithm. Again, the
difference is that one of the computations is generated lazily on demand while
the other is generated eagerly.
Just like with the previous
eager_fib, we can use multiple interpreters to run
let () = assert (55 = Identity.of_rea (run Identity.monad (fib 10))) let () = assert (`Ok 55 = Tailrec.run Tailrec.sync (fib 10))
This concludes the Fibonacci example. We now have a basic understanding of
effect readers. They are just functions that take a dictionary of capabilities
aka an interpreter as an argument.
Let's continue with an example demonstrating the extensible environment of the
Rea approach. To do so, let's implement a very rudimentary interpreter using a
modular approach. Although the techniques in this section scale to more
interesting language processors, we will keep the example very minimal.
First we'll implement a simple arithmetic language:
module Num = struct type 't t = [`Num of int | `Uop of [`Neg] * 't | `Bop of [`Add | `Mul] * 't * 't]
we use polymorphic variants with open recursion for the AST representation.
We will also use open recursion in the
let uop = function | `Neg -> ( ~-) let bop = function | `Add -> ( + ) | `Mul -> ( * ) let eval eval = eta'1 @@ function | `Num _ as v -> pure v | `Uop (op, x) -> ( eval x >>= function | `Num x -> pure @@ `Num (uop op x) | x -> fail @@ `Error_attempt_to_apply_uop (op, x)) | `Bop (op, l, r) -> ( eval l <*> eval r >>= function | `Num l, `Num r -> pure @@ `Num (bop op l r) | l, r -> fail @@ `Error_attempt_to_apply_bop (op, l, r))
eta'1 combinator is another way to write η-expanded functions. It takes a
function and returns a two parameter function. The
is for monadic bind and
let+ ... and+ ... is for
applicative pairing of computation.
Errors are reported with the
fail combinator. We use polymorphic variants for
After a bit of cleaning up, the type inferred for
eval is roughly equivalent
to the following definition:
let _ = (eval : ('t -> ( 'R, ([> `Error_attempt_to_apply_bop of ([< `Add | `Mul] as 'bop) * ([> `Num of int] as 'v) * 'v | `Error_attempt_to_apply_uop of ([< `Neg] as 'uop) * 'v ] as 'e), 'v, (< ('R, 'D) monad' ; ('R, 'D) errors' ; .. > as 'D) ) er) -> [< 't t] -> ('R, 'e, [> `Num of int], 'D) er) end
Notice that the above type shows both of the errors that might arise from
Let's then move on to implement (lambda) λ-expressions:
module Lam = struct module Id = String type 't t = [`Lam of Id.t * 't | `App of 't * 't | `Var of Id.t]
Deviating from Garrigue's example, we'll use an environment of bindings
module Bindings = Map.Make (Id)
that maps variables to values. Recall that the arithmetic language above knows
nothing about environments. To pass around the environment we'll use the
extensible environment of the Rea framework. For that we define a new class
['v] bindings that exposes a
class ['v] bindings : object method bindings : 'v Bindings.t Prop.t end = object val mutable v : 'v Bindings.t = Bindings.empty method bindings = Prop.make (fun () -> v) (fun x -> v <- x) end
Prop.t type, whose values are introduced by
Prop.make, is provided by
the Rea framework to concisely expose a mutable instance variable as a readable
and functionally updatable property. To be clear, it is not actually possible to
observably mutate the
v instance variable outside of the
For easy access to the
bindings method we define a trivial extractor:
let bindings d = d#bindings
Now we are ready to write the open
eval function for λ-expressions:
let eval eval = eta'1 @@ function | `Lam (i, e) -> let+ bs = get bindings in `Fun (bs, i, e) | `App (f, x) -> ( eval f >>= function | `Fun (bs, i, e) -> let* v = eval x in setting bindings (Bindings.add i v bs) (eval e) | f -> fail @@ `Error_attempt_to_apply f) | `Var i -> ( get_as bindings (Bindings.find_opt i) >>= function | None -> fail @@ `Error_unbound_var i | Some v -> pure v)
let+ binding operator is the
map operation of functors. The
combinator reads the value of a property extracted from the environment. The
setting combinator runs a computation with the value of a property
functionally updated to the given value. The
get_as combinator reads a
property and also maps it through the given function.
The following definition shows a cleaned up type for the
let _ = (eval : ('t -> ( 'R, ([> `Error_attempt_to_apply of ([> `Fun of 'v Bindings.t * Id.t * 't] as 'v) | `Error_unbound_var of Id.t ] as 'e), 'v, (< ('R, 'D) monad' ; ('R, 'D) errors' ; 'v bindings ; .. > as 'D) ) er) -> [< 't t] -> ('R, 'e, 'v, 'D) er) end
bindings as part of the
'D dictionary of capabilities.
To compose the full interpreter
module Full = struct
from the above parts, we write a recursive
eval function that dispatches to
one of the above
eval functions depending on the input:
let rec eval = function | #Num.t as e -> Num.eval eval e | #Lam.t as e -> Lam.eval eval e
Again, here is a cleaned up type for the
let _ = (eval : ([< 't Num.t | 't Lam.t] as 't) -> ( 'R, [> `Error_attempt_to_apply of ([> `Fun of 'v Lam.Bindings.t * Lam.Id.t * 't | `Num of int] as 'v) | `Error_attempt_to_apply_bop of [`Add | `Mul] * 'v * 'v | `Error_attempt_to_apply_uop of [`Neg] * 'v | `Error_unbound_var of Lam.Id.t ], 'v, (< ('R, 'D) monad' ; ('R, 'D) fail' ; 'v Lam.bindings ; .. > as 'D) ) er) end
Notice how the type combines
the arithmetic and λ-expressions (as
the errors (
the value type (as
the capability dictionaries (as
To actually run
eval we will need an effect interpreter that provides the
error' capabilities as well as
bindings. There is an
interpreter for the standard
result type that we can use for the
errors' capabilities. For the
bindings we can just use
bindings. Here is
let () = assert ( Error (`Error_unbound_var "y") = StdRea.Result.of_rea (run (object inherit [_] StdRea.Result.monad_errors inherit [_] Lam.bindings end) (Full.eval (`App (`Lam ("x", `Bop (`Add, `Num 2, `Var "y")), `Num 1)))))
Another interpreter that comes bundled with the Rea framework that provides both
errors' is the
Tailrec interpreter we used previously. So, we
could also use
Tailrec as follows:
let () = assert ( `Ok (`Num 3) = Tailrec.run (object inherit [_] Tailrec.sync inherit [_] Lam.bindings end) (Full.eval (`App (`Lam ("x", `Bop (`Add, `Num 2, `Var "x")), `Num 1))))
We could also use the asynchronous version of the
Tailrec interpreter. To
ensure that neither errors nor results are implicitly ignored, the
Tailrec.spawn function requires that the computation throws
(). We need to wrap the computation with handlers:
let () = let result = ref @@ Ok (`Num 0) in Tailrec.spawn (object inherit [_] Tailrec.async inherit [_] Lam.bindings end) (Full.eval (`App (`Lam ("x", `Bop (`Add, `Num 2, `Var "x")), `Num 1)) |> tryin (fun e -> pure (result := Error e)) (fun v -> pure (result := Ok v))); assert (!result = Ok (`Num 3))
tryin combinator allows us to handle errors and continue with results.
Since we handle all of the errors, the error type for the whole computation
becomes parametric and can be unified with
Normally one cannot assume that a computation started with
completes immediately. In this case we had nothing asynchronous in the
implementation and nothing asynchronous running in the background.
This concludes the example. We now know about the extensible environment as well
as about error handling.
Let's suppose next that we have an existing monadic library that we need to
interoperate with. For the sake of argument, let's assume the following
continuation monad implementation:
module Cont : sig type 'a t val return : 'a -> 'a t val bind : 'a t -> ('a -> 'b t) -> 'b t val callcc : (('a -> 'b t) -> 'a t) -> 'a t val run : 'a t -> 'a end = struct type 'a t = ('a -> unit) -> unit let return x k = k x let bind xK xyK k = xK (fun x -> (xyK x) k) let callcc kxK k = kxK (fun x _ -> k x) k let run xK = let result = ref None in xK (fun x -> result := Some x); Option.get !result end
First we notice that we ran into a bit of a snag. Although Rea provides a number
of related effects, at the time of writing, no
callcc effect is provided.
Fortunately nothing prevents users from extending the framework. We just write
class virtual ['R, 'D] callcc' = object method virtual callcc' : 'e 'f 'a 'b. (('a -> ('R, 'f, 'b, 'D) er) -> ('R, 'e, 'a, 'D) er) -> ('R, 'e, 'a) s end
And the generic effect reader combinator
let callcc f (d: (_, _) #callcc') = d#callcc' f
Now, how do we relate
'a Cont.t with the Rea framework? What we need to do is
to embed it into the abstract
('R, 'e, 's) s effect signature type. We create
an abstract representation type
r corresponding to the
constructor and an injection projection pair:
module ContRea = struct type r external to_rea : 'a Cont.t -> (r, 'e, 'a) s = "%identity" external of_rea : (r, 'e, 'a) s -> 'a Cont.t = "%identity"
Rea probably should provide a functor for the above, but it currently doesn't.
external fn : s -> t = "%identity"
construct tells OCaml that
fn is an external function of type
s -> t that is
actually the identity function. Because both the above type
r and the type
(_, _, _) s from Rea are abstract, the above two coercions are safe — as
long as we don't provide other incompatible coercions between the abstract
Now we can write down an interpreter class
class ['D] monad_callcc = object (d: 'D) inherit [r, 'D] monad'd method pure' x = to_rea (Cont.return x) method bind' x f = to_rea (Cont.bind (of_rea (x d)) (fun x -> of_rea (f x d))) inherit [r, 'D] callcc' method callcc' f = to_rea (Cont.callcc (fun k -> of_rea (f (fun x _ -> to_rea (k x)) d))) end end
Cont. As an example, we can use it with the previously defined
let () = assert ( 55 = Cont.run (ContRea.of_rea (run (new ContRea.monad_callcc) (fib 10))))
callcc is also available:
let () = assert ( 101 = Cont.run (ContRea.of_rea (run (new ContRea.monad_callcc) (callcc (fun k -> k 101)))))
All the generic combinators for monads and simpler functors, and the extensible
environment are now available when constructing
Cont computations via the Rea
We now know that we can write effect interpreters using existing monadic
libraries that run their computations embedded into the Rea framework and that
we can also introduce new effects into the framework.
Wonder what the last example will be about?
Indeed, mapping with an effect reader,
map_er, or "traverse" as it is often
called, tends to be the answer to many problems. So, let's explore the topic a
bit. We'll build on the earlier modular interpreter example.
Although we could use a modular approach and build traversal functions modularly
for expressions, that's not really the point here. So, let's just work on the
full AST. Here is a generic traversal function for the structural AST:
module TheAnswer = struct let map_er' nE o1E o2E iE eE = eta'1 @@ function | `Num x -> map_er'1 nE x >>- fun x -> `Num x | `Uop x -> map_er'2 o1E eE x >>- fun x -> `Uop x | `Bop x -> map_er'3 o2E eE eE x >>- fun x -> `Bop x | `Lam x -> map_er'2 iE eE x >>- fun x -> `Lam x | `App x -> map_er'2 eE eE x >>- fun x -> `App x | `Var x -> map_er'1 iE x >>- fun x -> `Var x
Instead of just traversing over the direct subexpressions of an expression, the
map_er' also allows traversing over the numbers, unary and binary
operators, and identifiers. The constructors of the datatype are traversed in a
systematic way using a family of canned
map_er'n functions for each arity of a
tuple the constructors are carrying.
Why call it
map_er rather than
traverse? Well, mapping over a datatype with
an effect constructor is just one of many useful generalizations of ordinary
Systematic naming hopefully makes the API easier to learn.
I find it convenient to implement traversal for a structural type in the above
manner as it allows one to easily specialize to the basic traversal over
let map_er eE = map_er' pure pure pure pure eE
and also use the generic traverse for other purposes.
The type of the
map_er over subexpressions is seen in the below definition:
type 't t = [ 't Num.t | 't Lam.t ] let _ = (map_er : ('s -> ('R, 'e, 't, (('R, 'D) #applicative' as 'D)) er) -> [< 's t] -> ('R, 'e, [> 't t], 'D) er)
What can one do with traversals? Well, a lot of things.
For example, here is a function that recursively traverses an expression to find
out whether a given variable is free or not in a given expression:
let rec is_free i' = function | `Var i -> i = i' | `Lam (i, _) when i = i' -> false | e -> Traverse.to_exists map_er (is_free i') e let () = assert (is_free "y" (`App (`Lam ("x", `Var "x"), `Var "y"))) let () = assert (not (is_free "x" (`App (`Lam ("x", `Var "x"), `Var "y"))))
map_er we can treat all the "basic" cases of the datatype generically
and focus on the two cases that are interesting with respect to bindings.
But we kind of got ahead of ourselves. How does
map_er does is that it maps every element of a datatype to an
effect and then combines those effects to reconstruct the shape of the datatype.
If, for example, we use the previously mentioned
Identity monad to run the
effects, then we basically get a
map function for the datatype.
Effects are not limited to simply returning a value of the answer type. We
already previously saw the
fail effect, which doesn't return an answer.
Another example is the
Constant functor, which, as its name suggests, carries
along a constant value of some type and the answer type is a phantom type. The
Constant functor can be augmented to an applicative over a monoid. For
example, we can use disjunction. And that is what
Traverse.to_exists does. It
maps the traversed elements to boolean constants as returned by the given
predicate. Then those booleans are combined using disjunction.
But this is all quite common knowledge. Why are we discussing this? Well, recall
that the Rea framework provides a form of laziness via η-expansion. That same
laziness also works with traversals over monoids, among other things. So, when
Traverse.to_exists map_er (is_free i') e, instead of first eagerly
building the computation for the whole expression tree
e, as one might expect
to be the case in a strict language like OCaml, the computation is built on
demand and actually stops roughly as soon as the first free variable occurrence
has been encountered. So, although the use of objects and whatnot brings quite a
bit of overhead, at least we actually get the desired asymptotic time complexity
This concludes the example and the introduction.
We now know about most aspects of the Rea framework. Perhaps the best way to
learn more is to take a brief look at the
reference manual and
start using the framework. Have fun!
The main drawbacks of this approach come from the deficiencies and limitations
of OCaml's objects:
OCaml does not aggressively optimize (statically known) method invocations.
This means that every effect invocation has some overhead.
OCaml's object system does not support adding methods to or removing methods
from objects (i.e. polymorphic record extension). This means that effects
cannot be easily handled locally.
On the other hand, this approach arguably has a rather straightforward
implementation and is convenient to use (modulo the inability to handle effects
Unfortunately the library
reference manual is
rather unfinished at the moment.