Coop is a prototype programming language for programming with runners, also known as comodels.
Coop is part of ongoing research by Danel Ahman and Andrej Bauer. The theoretical aspects of our work are described in the paper Runners in action. You may also be interested in Danel's talk Interacting with external resources using runners (aka comodels) and his Haskell-Coop library.
To compile Coop you need:
The OPAM packages
opam install menhir opam install sedlex opam install dune
It is recommended that you also install the
leditcommand line wrapper.
If you're reading this file then you have probably found the Coop GitHub repository, where Coop is available.
You can type:
maketo make the
make byteto make the bytecode
make cleanto clean up.
make docto generate HTML documentation (see the generated
To find out more about Coop, please consult the Coop manual.
Coop is an extension of
λ-coop, a calculus devised by Danel Ahman and Andrej
Bauer, cf. our paper Runners in action, to
study how runners (also known as comodels) can be used to program with
external resources. These are similar to handlers for algebraic effects, except
that they carry state and use the continuation at most one in a tail-call
position. There are two kinds of computations in
λ-coop: the kernel
computations implement access to resources as co-operations, while the user
computations use resources by calling algebraic operations. The kernel mode has
the ability to report errors to user mode by raising exceptions (recoverable
errors), or aborting user code by sending it signals (unrecoverable errors).
The central construct of
using R @ I run M finally F
which runs user code
M and handles its operations using the (kernel mode) co-operations
R. It is a kind of "virtual machine" which runs user code inside a kernel
R. The runner has access to state (hidden from the user code) which is
I. The finalisation code
F intercepts the return value, exceptions and
signals, with the purpose of properly disposing of any resources used by the runner
The calculus guarantee that
F will be reached (unless an outer runner kills the present
The type system of
λ-cup keeps track of effects and supports subtyping.