MoonBit Pearls Vol 4: Choreographic Programming with Moonchor

Traditional distributed programming is notoriously painful, primarily because we need to reason about the implicit global behavior while writing the explicit local programs that actually run on each node. This fragmented implementation makes programs difficult to debug, understand, and deprives them of type-checking provided by programming languages. Choreographic Programming makes the global behavior explicit by allowing developers to write a single program that requires communication across multiple participants, which is then projected onto each participant to achieve global behavior.
Choreographic programming is implemented in two distinct approaches:
- As a completely new programming language (e.g., Choral), where developers write Choral programs that will be compiled into participant-specific Java programs.
- As a library (e.g., HasChor), leveraging Haskell's type system to ensure static properties of choreographic programming while seamlessly integrating with Haskell's ecosystem.
MoonBit's functional programming features and powerful type system make it particularly suitable for building choreographic programming libraries.
This article demonstrates the core concepts and basic usage of choreographic programming using MoonBit's moonchor library through several examples.
Guided Tour: Bookstore Application
Let's examine a bookstore application involving two roles: Buyer and Seller. The core logic is as follows:
- The buyer sends the desired book title to the seller.
- The seller queries the database and informs the buyer of the price.
- The buyer decides whether to purchase the book.
- If the buyer decides to purchase, the seller deducts the book from inventory and sends the estimated delivery date to the buyer.
- Otherwise, the interaction terminates.
Traditional Implementation
Here, we focus on core logic rather than implementation details, using send and recv functions to represent message passing. In the traditional approach, we need to develop two separate applications for buyer and seller. We assume the following helper functions and types exist:
fn fn get_title() -> String
get_title() -> String
String {
"Homotopy Type Theory"
}
fn fn get_price(title : String) -> Int
get_price(String
title : String
String) -> Int
Int {
50
}
fn fn get_budget() -> Int
get_budget() -> Int
Int {
100
}
fn fn get_delivery_date(title : String) -> String
get_delivery_date(String
title : String
String) -> String
String {
"2025-10-01"
}
enum Role {
Role
Buyer
Role
Seller
}
async fn[T] async fn[T] send(msg : T, target : Role) -> Unit
send(T
msg : type parameter T
T, Role
target : enum Role {
Buyer
Seller
}
Role) -> Unit
Unit {
...
}
async fn[T] async fn[T] recv(source : Role) -> T
recv(Role
source : enum Role {
Buyer
Seller
}
Role) -> type parameter T
T {
...
}
The buyer's application:
async fn async fn book_buyer() -> Unit
book_buyer() -> Unit
Unit {
let String
title = fn get_title() -> String
get_title()
async fn[T] send(msg : T, target : Role) -> Unit
send(String
title, Role
Seller)
let Int
price = async fn[T] recv(source : Role) -> T
recv(Role
Seller)
if Int
price (x : Int, y : Int) -> Bool
<= fn get_budget() -> Int
get_budget() {
async fn[T] send(msg : T, target : Role) -> Unit
send(true, Role
Seller)
let Unit
delivery_date = async fn[T] recv(source : Role) -> T
recv(Role
Seller)
fn[T : Show] println(input : T) -> Unit
Prints any value that implements the Show trait to the standard output,
followed by a newline.
Parameters:
value : The value to be printed. Must implement the Show trait.
Example:
println(42)
println("Hello, World!")
println([1, 2, 3])
println("The book will be delivered on: \{Unit
delivery_date}")
} else {
async fn[T] send(msg : T, target : Role) -> Unit
send(false, Role
Seller)
}
}
The seller's application:
async fn async fn book_seller() -> Unit
book_seller() -> Unit
Unit {
let String
title = async fn[T] recv(source : Role) -> T
recv(Role
Buyer)
let Int
price = fn get_price(title : String) -> Int
get_price(String
title)
async fn[T] send(msg : T, target : Role) -> Unit
send(Int
price, Role
Buyer)
let Bool
decision = async fn[T] recv(source : Role) -> T
recv(Role
Buyer)
if Bool
decision {
let String
delivery_date = fn get_delivery_date(title : String) -> String
get_delivery_date(String
title)
async fn[T] send(msg : T, target : Role) -> Unit
send(String
delivery_date, Role
Buyer)
}
}
These two implementations suffer from at least the following issues:
-
No type safety guarantee: Note that both
sendandrecvare generic functions. Type safety is only ensured when the types of sending and receiving messages match; otherwise, runtime errors may occur during (de)serialization. The compiler cannot verify type safety at compile time because it cannot determine whichsendcorresponds to whichrecv. Type safety is dependent on the developer not making mistakes. -
Potential deadlocks: If the developer accidentally forgets to write some
sendin the buyer's program, both buyer and seller may wait indefinitely for each other's messages and be stuck. Alternatively, if a buyer's connection is temporarily interrupted during network communication, the seller will keep waiting for the buyer's message. Both scenarios lead to deadlocks. -
Explicit synchronization required: To communicate the purchase decision, the buyer must explicitly send a
Boolmessage. Subsequent coordination requires ensuring both buyer and seller follow the same execution path at theif price <= get_budget()andif decisionbranches - a property that cannot be guaranteed at compile time.
The root cause of these problems lies in splitting what should be a unified coordination logic into two separate implementations based on implementation requirements. Next, we'll examine how choreographic programming addresses these issues.
moonchor Implementation
With choreographic programming, we can write the buyer's and seller's logic in the same function, which then exhibits different behaviors with different parameters when called. We use moonchor's API to define the buyer and seller roles. In moonchor, roles are defined as trait Location. To provide better static properties, roles are not only values but also unique types that need to implement the Location trait.
struct Buyer {} derive(trait Show {
output(Self, &Logger) -> Unit
to_string(Self) -> String
}
Trait for types that can be converted to String
Show, trait Hash {
hash_combine(Self, Hasher) -> Unit
hash(Self) -> Int
}
Trait for types that can be hashed
The hash method should return a hash value for the type, which is used in hash tables and other data structures.
The hash_combine method is used to combine the hash of the current value with another hash value,
typically used to hash composite types.
When two values are equal according to the Eq trait, they should produce the same hash value.
The hash method does not need to be implemented if hash_combine is implemented,
When implemented separately, hash does not need to produce a hash value that is consistent with hash_combine.
Hash)
impl @moonchor.Location for struct Buyer {
} derive(Show, Hash)
Buyer with (_/0) -> String
name(_) {
"buyer"
}
struct Seller {} derive(trait Show {
output(Self, &Logger) -> Unit
to_string(Self) -> String
}
Trait for types that can be converted to String
Show, trait Hash {
hash_combine(Self, Hasher) -> Unit
hash(Self) -> Int
}
Trait for types that can be hashed
The hash method should return a hash value for the type, which is used in hash tables and other data structures.
The hash_combine method is used to combine the hash of the current value with another hash value,
typically used to hash composite types.
When two values are equal according to the Eq trait, they should produce the same hash value.
The hash method does not need to be implemented if hash_combine is implemented,
When implemented separately, hash does not need to produce a hash value that is consistent with hash_combine.
Hash)
impl @moonchor.Location for struct Seller {
} derive(Show, Hash)
Seller with (_/0) -> String
name(_) {
"seller"
}
let Buyer
buyer : struct Buyer {
} derive(Show, Hash)
Buyer = struct Buyer {
} derive(Show, Hash)
Buyer::{ }
let Seller
seller : struct Seller {
} derive(Show, Hash)
Seller = struct Seller {
} derive(Show, Hash)
Seller::{ }
Buyer and Seller types don't contain any fields. Types implementing the Location trait only need to provide a name method that returns a string as the role's identifier. This name method is critically important - it serves as the definitive identity marker for roles and provides a final verification mechanism when type checking cannot guarantee type safety. Never assign the same name to different roles, as this will lead to unexpected runtime errors. Later we'll examine how types provide a certain level of safety and why relying solely on types is insufficient.
Next, we define the core logic of the bookstore application, which is referred to as a choreography:
async fn async fn bookshop(ctx : ?) -> Unit
bookshop(?
ctx : @moonchor.ChoreoContext) -> Unit
Unit {
let Unit
title_at_buyer = ?
ctx.(Buyer, (Unit) -> String) -> Unit
locally(let buyer : Buyer
buyer, Unit
_unwrapper => fn get_title() -> String
get_title())
let Unit
title_at_seller = ?
ctx.(Buyer, Seller, Unit) -> Unit
comm(let buyer : Buyer
buyer, let seller : Seller
seller, Unit
title_at_buyer)
let Unit
price_at_seller = ?
ctx.(Seller, (Unit) -> Int) -> Unit
locally(let seller : Seller
seller, fn(Unit
unwrapper) {
let String
title = Unit
unwrapper.(Unit) -> String
unwrap(Unit
title_at_seller)
fn get_price(title : String) -> Int
get_price(String
title)
})
let Unit
price_at_buyer = ?
ctx.(Seller, Buyer, Unit) -> Unit
comm(let seller : Seller
seller, let buyer : Buyer
buyer, Unit
price_at_seller)
let Unit
decision_at_buyer = ?
ctx.(Buyer, (Unit) -> Bool) -> Unit
locally(let buyer : Buyer
buyer, fn(Unit
unwrapper) {
let Int
price = Unit
unwrapper.(Unit) -> Int
unwrap(Unit
price_at_buyer)
Int
price (x : Int, y : Int) -> Bool
< fn get_budget() -> Int
get_budget()
})
if ?
ctx.(Buyer, Unit) -> Bool
broadcast(let buyer : Buyer
buyer, Unit
decision_at_buyer) {
let Unit
delivery_date_at_seller = ?
ctx.(Seller, (Unit) -> String) -> Unit
locally(let seller : Seller
seller, Unit
unwrapper => fn get_delivery_date(title : String) -> String
get_delivery_date(
Unit
unwrapper.(Unit) -> String
unwrap(Unit
title_at_seller),
))
let Unit
delivery_date_at_buyer = ?
ctx.(Seller, Buyer, Unit) -> Unit
comm(
let seller : Seller
seller, let buyer : Buyer
buyer, Unit
delivery_date_at_seller,
)
?
ctx.(Buyer, (Unit) -> Unit) -> Unit
locally(let buyer : Buyer
buyer, fn(Unit
unwrapper) {
let Unit
delivery_date = Unit
unwrapper.(Unit) -> Unit
unwrap(Unit
delivery_date_at_buyer)
fn[T : Show] println(input : T) -> Unit
Prints any value that implements the Show trait to the standard output,
followed by a newline.
Parameters:
value : The value to be printed. Must implement the Show trait.
Example:
println(42)
println("Hello, World!")
println([1, 2, 3])
println("The book will be delivered on \{Unit
delivery_date}")
})
|> fn[T] ignore(t : T) -> Unit
Evaluates an expression and discards its result. This is useful when you want
to execute an expression for its side effects but don't care about its return
value, or when you want to explicitly indicate that a value is intentionally
unused.
Parameters:
value : The value to be ignored. Can be of any type.
Example:
let x = 42
ignore(x) // Explicitly ignore the value
let mut sum = 0
ignore([1, 2, 3].iter().each(x => sum = sum + x)) // Ignore the Unit return value of each()
ignore
}
}
This program is somewhat lengthy, so let's analyze it line by line.
The function parameter ctx: @moonchor.ChoreoContext is the context object provided by moonchor to applications, containing all interfaces for choreographic programming on the application side. First, we use ctx.locally to execute an operation get_title() that only needs to run at the buyer role. The first parameter of ctx.locally is the role. The second parameter is a closure where the content is the operation to execute, with the return value being wrapped as the return value of ctx.locally. Here, get_title() returns a String, while title_at_buyer has type @moonchor.Located[String, Buyer], indicating this value exists at the buyer role and cannot be used by other roles. If you attempt to use title_at_buyer at the seller role, the compiler will report an error stating that Buyer and Seller are not the same type.
Next, the buyer needs to send the book title to the seller, which we implement using ctx.comm. The first parameter of ctx.comm is the sender role, the second is the receiver role, and the third is the message to send. Here, the return value title_at_seller has type @moonchor.Located[String, Seller], indicating this value exists at the seller role. As you might have guessed, ctx.comm corresponds precisely to the send and recv operations. However, here type safety is guaranteed: ctx.comm is a generic function that ensures (1) the sent and received messages have the same type, and (2) the sender and receiver roles correspond to the type parameters of the parameter and return types, namely @moonchor.Located[T, Sender] and @moonchor.Located[T, Receiver].
Moving forward, the seller queries the database to get the book price. At this step we use the unwrapper parameter passed to the ctx.locally closure. This parameter is an object for unpacking Located types, whose type signature also includes a role type parameter. We can understand how it works by examining the signature of Unwrapper::unwrap: fn[T, L] Unwrapper::unwrap(_ : Unwrapper[L], v : Located[T, L]) -> T. This means in ctx.locally(buyer, unwrapper => ...), unwrapper has type Unwrapper[Buyer], while title_at_seller has type Located[String, Seller], so unwrapper.unwrap(title_at_seller) yields a result of type String. This explains why we can use title_at_seller in the closure but not title_at_buyer.
Knowledge of Choice
Explicit synchronization in the subsequent process is critical. We need a dedicated section to explain that. In choreographic programming, this synchronization is referred to as Knowledge of Choice. In the example above, the buyer needs to know whether to purchase the book, and the seller needs to know the buyer's decision. We use ctx.broadcast to implement this functionality.
The first parameter of ctx.broadcast is the sender's role, and the second parameter is the message to be shared with all other roles. In this example, both buyer and seller need to know the purchase decision, so the buyer broadcasts this decision decision_at_buyer to all participants (here only the seller) via ctx.broadcast. Interestingly, the return value of broadcast is a plain type rather than a Located type, meaning it can be used by all roles directly at the top level without needing to be unwrapped with unwrapper in locally. This allows us to use MoonBit's native if conditional statements for subsequent flows, ensuring both buyer and seller follow the same branch.
As the name suggests, ctx.broadcast serves to broadcast a value throughout the entire choreography. It can broadcast not just Bool types but any other type as well. Its results can be applied not only to if conditions but also to while loops or any other scenarios requiring common knowledge.
Launch Code
How does such a choreography run? moonchor provides the run_choreo function to launch a choreography. Currently, due to MoonBit's multi-backend feature, providing stable, portable TCP servers and cross-process communication interfaces presents challenges. Therefore, we'll use coroutines and channels to explore the actual execution process of choreographies. The complete launch code is as follows:
test "Blog: bookshop" {
let Unit
backend = (Array[Buyer]) -> Unit
@moonchor.make_local_backend([let buyer : Buyer
buyer, let seller : Seller
seller])
(() -> Unit) -> Unit
@toolkit.run_async(() => (Unit, async (?) -> Unit, Buyer) -> Unit
@moonchor.run_choreo(Unit
backend, async fn bookshop(ctx : ?) -> Unit
bookshop, let buyer : Buyer
buyer) )
(() -> Unit) -> Unit
@toolkit.run_async(() => (Unit, async (?) -> Unit, Seller) -> Unit
@moonchor.run_choreo(Unit
backend, async fn bookshop(ctx : ?) -> Unit
bookshop, let seller : Seller
seller) )
}
The above code launches two coroutines that execute the same choreography at the buyer and seller respectively. This can also be understood as the bookshop function being projected (also called EPP, endpoint projection) into two completely different versions: the "buyer version" and "seller version". In this example, the first parameter of run_choreo is a Backend type object that provides the underlying communication mechanism required for choreographic programming. We use the make_local_backend function to create a local backend (not to be confused with MoonBit's multi-backend mentioned earlier), which can run in local processes using the channel API provided by peter-jerry-ye/async/channel as the communication foundation. In the future, moonchor will provide more backend implementations, such as HTTP.