MultiChor: Census Polymorphic Choreographic Programming with Multiply Located Values

TL;DR

MultiChor is presented, a library for writing and running choreographies as monadic values in Haskell that can express choreographies that are polymorphic over the number of participants.

Abstract

Choreographic programming is a concurrent paradigm in which a single global program called a choreography describes behavior across an entire distributed network of participants. Choreographies are easier to reason about than separate programs running in parallel, and choreographic programming systems can check for deadlocks statically. We present MultiChor, a library for writing and running choreographies as monadic values in Haskell. Unlike prior Haskell implementations, MultiChor does not require excess communication to handle Knowledge-of-Choice. Unlike all prior general-purpose choreographic languages, MultiChor can express choreographies that are polymorphic over the number of participants.

Figures (13)

• Figure 1: A card game expressed as a choreography written in Multi-Chor. This choreography is polymorphic over the number and identity of the players, but the party named [breaklines]haskell"dealer" is an explicit member. The inner monad [breaklines]haskellCLI that all parties have access to is a simple freer monad that can be handled to IO operations, or as [breaklines]haskellState for testing purposes. The [breaklines]haskellnewtype Card encapsulates the modulo operation in its [breaklines]haskellNum instance.
• Figure 2: An example choreography, written with Multi-Chor, in which an [breaklines]haskellInt, originating at a party [breaklines]haskellbob, is passed back and forth. Ultimately, a version of that value owned only by [breaklines]haskellcarroll is returned. Part of the choreography takes place in an [breaklines]haskellenclave involving some collection of parties specified by [breaklines]haskellclique.
• Figure 3: The monadic functions for constructing [breaklines]haskellChoreo expressions.
• Figure 4: A system for building key-value-store choreographies, including an example backup strategy that's polymorphic on the number of backup servers.
• Figure 5: Choreographies for secret sharing [breaklines]haskellp's secret value among [breaklines]haskellparties and for revealing a secret-shared value. [breaklines]haskellp constructs secret shares locally (line 9), then sends one share to each party (lines 10--11), including themselves. The result is a [breaklines]haskellFaceted value---each party has one secret share of the secret.