Choret: Functional Choreographic Programming for Racket🔗

Choret is an in-development Racket library which allows for choreographic programming. It implements an untyped language based off of Pirouette, a functional choreographic programming language developed by Andrew K. Hirsch (my research advisor) and Deepak Garg. Their paper, Pirouette: Higher-Order Typed Functional Choreographies, can be found here: https://dl.acm.org/doi/10.1145/3498684.

1 Getting Started🔗

1.1 Requirements to Run🔗

1.2 Installing Choret as a Library🔗

2 What is Choreographic Programming?🔗

In a traditional system with multiple locations (threads, processes, etc.) interacting with each other, the programmer has to carefully write multiple independent programs while also avoiding things such as deadlock or livelock. In particular, encoding a pattern of sends and recieves between locations in a system can be error prone since it is relatively easy to write mismatched send and recieve actions between two separately maintained programs; it is entirely up to the programmer to maintain the state and invariants of the entire system.

Choreographic programming aims to solve this problem by allowing programmers to give a "global" description of the program. In other words, the programmer writes a single program that describes the logic of the system/protocol as a whole, explicity specifying the when data needs to be transferred from one participant to another.

2.1 The Bookseller Example in Racket🔗

Seems simple enough, this is what such a program might look like in Racket, with the matching sends and recieves commented with a number in square brackets (using threads and channels for simplicity):

(define ch (make-channel))

; Buyer thread

(define buyer

(thread

(lambda ()

(define book-title "Alice in Wonderland")

(define budget 20)

(channel-put ch book-title) ; [1]

(define price (channel-get ch)) ; [2]

(if (< price budget)

(let ()

(channel-put ch 'buy-book) ; [3]

(define date (channel-get ch))

(printf "My book should arrive on ~a!~n" date)) ; [4]

(printf "Nevermind!~n")))))

; Seller thread

(define seller

(thread

(lambda ()

(define price-catalog (make-hash '(["Alice in Wonderland" . 25])))

(define book-title (channel-get ch)) ; [1]

(define price (hash-ref price-catalog book-title))

(channel-put ch price) ; [2]

(define will-buy (channel-get ch)) ; [3]

(if (equal? will-buy 'buy-book)

(channel-put ch "January 1, 1970") ; [4]

(printf "Let me know if you change your mind!~n")))))

(thread-wait buyer)

(thread-wait seller)

Even though this may be a trivial example, it emphasizes the importance of correctly matching sends and recieves; in much more complicated programs it may be much harder to correctly do this by hand.

2.2 The Bookseller Example in Choret🔗

If manually matching sends and recieves is error prone, what can be done differently?

Looking back in the last section, the bookseller system was described as a series of steps:

1. The buyer sends the title of a book they would like to buy to the seller.

2. The seller looks up the book title and retrieves the cost of the book; the price is communicated back to the buyer.

3. The buyer tells the seller whether or not they will buy the book.

4. If the buyer says they will buy the book, the seller completes the transaction by giving the buyer a shipping date.

This English prose description already describes what the system should do in a global manner. This can be translated into pseudo-code:

The above pseudo-code basically describes a choreographic program! Finally here is the bookseller program written in Choret:

(require choret)

(chor (buyer seller)

(define (at buyer book-title) (at buyer "Alice in Wonderland"))

(define (at buyer budget) (at buyer 30))

(define (at seller price-catalog)

(at seller (make-hash '(["Alice in Wonderland" . 25]))))

(define (at seller book-title) (~> (at buyer book-title) seller)) ; [1]

(define (at seller price) (at seller (hash-ref price-catalog book-title)))

(define (at buyer price) (~> (at seller price) buyer))

(if (at buyer (< price budget))

(sel~> buyer ([seller 'buy-book])

(let ()

(define (at seller date)

(at seller "January 1, 1970"))

(define (at buyer date)

(~> (at seller date) buyer))

(at buyer

(printf

"My book should arrive on ~a!~n"

date))))

(sel~> buyer ([seller 'reject-book])

(begin

(at buyer (printf "Nevermind!~n"))

(at seller

(printf

"Let me know if you change your mind!~n"))))))

This is a somewhat verbose piece of code so here is a breakdown of what is going on:

First, there are these (define (at LOCATION ID) EXPR) forms which define a variable which is located at LOCATION; EXPR can be any Choret form which evaluates to a value that is also located at LOCATION.

There are also communication primitives of the form (~> (at SENDER LOCAL-EXPR) RECIEVER), these forms evaluate LOCAL-EXPR at the location SENDER and produce a value located at RECIEVER; the underlying implementation executes a ~> form by sending the result of evaluating LOCAL-EXPR and sending the value from SENDER to RECIEVER.

"at" expressions, which have the form (at LOCATION LOCAL-EXPR) evaluate LOCAL-EXPR as a normal Racket expression located at LOCATION.

The forms that comprise the first half of the choreography are fairly straightforward, however, things get a little more involved when handling conditionals.

2.3 Conditional Expressions🔗

What makes conditional branching difficult in choreographic programming? It helps to think about the code that has to be generated for each location, which is referred to as the projection of each location.

This combining of the branches of the if form is known as merging. In fact whenever an if expresssion is projected for locations other than the one in the guard expression (in this case L1), the two branches are merged together. Merging is strictly something that is performed at compile time.

There are two problems here. First, since L2 now needs to do something different in each branch, there needs to be some way to communicate the knowledge of L1’s decision to L2. Second, L2’s projections of the branches cannot be merged together as they are not identical (the 5 and 10 do not match). In the next section, selections will be used to solve both of these problems.

2.4 Selection and Knowledge of Choice🔗

The dependency between locations about which branch should be taken is known as Knowledge of Choice. To comminicate Knowledge of Choice a message from the deciding location (such as L1 in the example above) to other dependent locations needs to be sent.

In the previous example, it is trivial to understand that L1 should send L2 a message about which branch to take. So why not have the compiler just automatically do this for the programmer? A problem arises in programs with more locations; if the compiler does this naively, then it has to send a message to every location, even if not all locations need to know the decision at L1; otherwise the compiler needs to automatically infer which locations need Knowledge of Choice, which can be difficult to do.

Instead of doing either of those things, Choret requires the programmer to explicitly state Knowledge of Choice where appropriate. This is accomplished using the (sel~> SENDER ([RECIEVER LABEL] ...) EXPR) form to perform what is known as a selection. The selection form can be thought of as sending a message from SENDER, which should be the location which actually determines whether to take the branch, to a multiple recieving locations, where for each RECIEVER, LABEL is a unique value that represents the branch to be taken and EXPR is a Choret expression to be evaluated for that particular branch.

The example from the last section can be updated to use selections as appropriate:

As seen above, selections are also important for merging. In fact the case where two selections (sel~> forms) are being merged together is actually a special case; the set labels between the two selections are compared and the sub-expressions corresponding to unique labels are simply left alone to be projected as-is; if two labels are shared between the selections however, the sub-expressions corresponding to those labels are recursively merged together.

In the example above, since the selections in either branch do not match, they do not need to be merged together.

It should be noted that the reason why unique labels between selections do not need to be merged is because the sel~> form also generates the code needed to communicate the appropriate Knowledge of Choice; merging is only needed in the absence of Knowledge of Choice.

2.5 Simplified Bookseller Example in Choret🔗

The previous bookseller example in Choret was a bit verbose and repetitive, but this can be improved by using more of the forms and idioms availible in Choret:

(chor (buyer seller)

(define (at buyer book-title) (at buyer "Alice in Wonderland"))

(define (at buyer budget) (at buyer 30))

(define (at seller price-catalog)

(at seller (make-hash '(["Alice in Wonderland" . 25]))))

(define (at buyer price)

(let ([(at seller book-title) (~> (at buyer book-title) seller)])

(~> (at seller (hash-ref price-catalog book-title)) buyer)))

(if (at buyer (< price budget))

(sel~> buyer ([seller 'buy-book])

(let ([(at buyer date)

(~> (at seller "January 1, 1970") buyer)])

(at buyer

(printf

"My book should arrive on ~a!~n"

date))))

(sel~> buyer ([seller 'reject-book])

(begin

(at buyer (printf "Nevermind!~n"))

(at seller

(printf

"Let me know if you change your mind!~n"))))))

3 Choret Forms🔗

(define (global-id binding-form ...) global-body ...+)

Syntactic sugar, equivalent to:

(define global-id (lambda (binding-form ...) global-body ...))

(define (at reciever id) (~> (at sender local-expr) reciever))

4 Future Work🔗

Being an experimental library, there are still many things that could be added and/or ammended to improve Choret:

• A type system for tracking and checking located-types and choreographic function types

• Implement Location Polymorphism

• Prohibit choreographic variables from being used directly in local expressions

• More unit tests and measurement of code coverage

• Better logging functionality

• Better error messages when projecting code

• Wrap all choreographic values with some kind of "chor-value" struct to provide better runtime errors (and perhaps other functionality)

• Provide Choret as a proper "#lang" rather than just a library

• Allow Choret to create module level definitions

• Lift more forms from Racket into Choret

• Integrate Choret with Racket Places

• Implement a library of convenience functions and macros for syntactic sugar for Choret

• Improve the underlying system of macros in "threads-network.rkt" which helps with implementing locations as Racket threads with synchronous channels