/HasChor-clone

Functional choreographic programming in Haskell

Primary LanguageHaskellBSD 3-Clause "New" or "Revised" LicenseBSD-3-Clause

HasChor

HasChor is a library for functional choreographic programming in Haskell.

  • HasChor provides a monadic interface for choreographic programming where choreographies are expressed as computations in a monad.

  • Based on Haskell's type system, HasChor supports higher-order choreographies and location polymorphism, both features that enable modularity and code reuse.

  • HasChor's implementation is flexible, extensible, and concise (less than 150 lines of code for the core implementation; the swappable backends add another 150 lines) thanks to the mixed embedding technique it uses. Freer monads let us reuse existing Haskell constructs as much as possible while interpreting choreographic primitives freely.

See our ICFP 2023 paper (preprint) for more details. For API specifications, check out the documentation.

HasChor's design is heavily influenced by Pirouette. For a general introduction to choreographic programming, we recommend Fabrizio Montesi's excellent book: Introduction to Choreographies.

Directory structure

Building the library

HasChor is a Haskell library and built with the Glasgow Haskell Compiler (GHC). You can either build from the source or use the Docker image.

Building from the source

HasChor is tested with the following Haskell environment:

Newer versions might work but are not guaranteed. We recommend using GHCup to set up the environment.

To build HasChor, do:

git clone https://github.com/gshen42/HasChor.git
cd HasChor
cabal build -j20

Using the Docker image

First, clone the repo and build the Docker image:

git clone https://github.com/gshen42/HasChor.git
cd HasChor
docker build -t haschor .

Next, create a container and run Bash in it:

docker run -it -name foo haschor bash

You should be presented with HasChor's root directory with everything built.

To create another Bash shell in the container for running and testing choreographies, do:

docker exec -it foo bash

To remove the created container, do:

docker rm foo

Running example choreographies

HasChor comes with a set of illustrative example choreographies located in the examples directory. To run these examples, do:

cabal run <executable-name> <location>

The <executable-name> for each example can be found in the executable section of the HasChor.cabal file, and they usually match with their directory name in examples.

The <location> specifies what location the choreography should be projected to and run. In most cases, you would open up multiple shells and run the choreography with a participating location in each of them to simulate a distributed system. It is crucial that you run the choreography with all participanting locations and roughly at the same time, otherwise the system would deadlock or throw an error. Most examples come with a README.md in their directory that details the commands to run them properly.

As an example, here we show how to run the bookseller-1-simple example. First, check out the README.md for general information about the example. To run the example, do:

# in shell 1
cabal run bookseller-1-simple buyer

# in shell 2
cabal run bookseller-1-simple seller

# shell 1 will prompt the user to type in the book they want to buy
> Enter the title of the book to buy
Types and Programming Languages

# shell 1 will return the delivery date it receives from the seller
# then both programs terminate
> The book will be delivered on 2022-12-19

Writing your own choreography

The easist way to write your choreography is to use the playground example where we provide a template for writing your own choreography. Edit the Main.hs file and run the chreography as follows:

cabal run playground <location>

If you want to depend on HasChor in your own package, add this to your cabal.project.

source-repository-package
    type: git
    location: https://github.com/gshen42/HasChor.git
    branch: main

Notes for artifact evaluation

Step 1: Obtaining and building the artifact

See Building the library from above. The following steps assume the reviewer is in the root directory of the repo.

Step 2: Running the examples from the paper

In this step we describe how to run each of the examples from our paper. Most of the examples are interactive programs requiring command-line inputs from the user, so this is not a "press one key and walk away" step.

Step 2.1: Bookseller examples

These examples use a protocol that defines an interaction between two participants: a seller and a (would-be) buyer. The protocol begins with the buyer sending the title of a book they want to buy to the seller. The seller replies with the book’s price, and the buyer checks if the price is within their budget. If the buyer can afford the book, they inform the seller and get back a delivery date; otherwise, they tell the seller they will not buy the book.

In these examples, we assume the only books that a buyer can buy are "Types and Programming Languages" and "Homotopy Type Theory", as priceOf and deliveryOf are partial functions:

priceOf :: String -> Int
priceOf "Types and Programming Languages" = 80
priceOf "Homotopy Type Theory"            = 120

deliveryDateOf :: String -> Day
deliveryDateOf "Types and Programming Languages" = fromGregorian 2022 12 19
deliveryDateOf "Homotopy Type Theory"            = fromGregorian 2023 01 01

It's straightforward to extend these definitions and make them total.

By default, the buyer's budget is set to 100.

Bookseller as individual network programs

To run a simple, non-choreographic "bookseller" example from the paper (shown in Figures 1 and 2), open two shells and then run the following commands from the project directory:

# in shell 1
cabal run bookseller-0-network buyer

# in shell 2
cabal run bookseller-0-network seller

The buyer can then interact by typing in the name of the book they want to buy. For example:

# in shell 1
> Enter the title of the book to buy
Types and Programming Languages

# in shell 1
> The book will be delivered on 2022-12-19

Bookseller as a simple choreography

Next, to run the simple choreographic bookseller example from the paper (shown in Figures 3 and 4) with a book different than before:

# in shell 1
cabal run bookseller-1-simple buyer

# in shell 2
cabal run bookseller-1-simple seller

# in shell 1
> Enter the title of the book to buy
Homotopy Type Theory

# in shell 1
> The book's price is out of the budget

Higher-order bookseller

To run the higher-order choreographic bookseller example from the paper (shown in Figure 5) with mkDecision2:

# in shell 1
cabal run bookseller-2-higher-order buyer

# in shell 2
cabal run bookseller-2-higher-order buyer2

# in shell 3
cabal run bookseller-2-higher-order seller

# in shell 1
> Enter the title of the book to buy
Homotopy Type Theory

# in shell 2
> How much you're willing to contribute?
100

# in shell 1
The book will be delivered on 2023-01-01

Note that previously, the buyer couldn't buy Homotopy Type Theory as it was out of the budget, but with buyer2's contribution, now they can.

Location-polymorphic bookseller

Finally, to run the location-polymorphic choreographic bookseller example from the paper (shown in Figure 6):

# in shell 1
cabal run bookseller-3-loc-poly buyer

# in shell 2
cabal run bookseller-3-loc-poly seller

# in shell 1
> Enter the title of the book to buy
Types and Programming Languages

# in shell 1
> The book will be delivered on 2022-12-19

Step 2.2: Key-value store examples

These examples define a protocol for a key-value store (KVS). A client sends requests to a server, and the server handles requests and sends responses back to the client. The server supports two kinds of requests: PUT, to set a given key-value pair, and GET, to look up the value associated with a specified key.

Both the client and server run in an infinite loop waiting for commands.

Simple KVS

To run the simple choreographic key-value store example from the paper (shown in Figures 7 and 8):

# start server
cabal run kvs1 server
# on a different terminal for client
cabal run kvs1 client

The client will then be prompted for a command, and the user can input PUT and GET commands. An example interaction on the client side might look like the following:

# on the client terminal
Command?
GET hello
> Nothing
Command?
PUT hello world
> Just "world"
Command?
GET hello
> Just "world"
Primary-backup KVS

To run the primary-backup key-value store example from the paper (shown in Figure 9):

# start primary
cabal run kvs2 primary

# on a different terminal, start backup
cabal run kvs2 backup

# another terminal for client
cabal run kvs2 client
GET hello
> Nothing
PUT hello world
> Just "world"
GET hello
> Just "world"
Higher-order KVS

To run the higher-order key-value store example from the paper (shown in Figure 10):

# start primary
cabal run kvs3 primary

# on a different terminal, start backup
cabal run kvs3 backup

# another terminal for client
cabal run kvs3 client
GET hello
> Nothing
PUT hello world
> Just "world"
GET hello
> Just "world"
Location-polymorphic and higher-order KVS

To run the (location-polymorphic and higher-order) double-backup key-value store example from the paper (shown in Figures 11 and 12):

# start primary
cabal run kvs4 primary

# on a different terminal, start backup1
cabal run kvs4 backup1

# another terminal for backup2
cabal run kvs4 backup2

# yet another terminal for client
cabal run kvs4 client
GET hello
> Nothing
PUT hello world
> Just "world"
GET hello
> Just "world"

Step 2.3: Brief tour of the implementation

See Directory structure from above.