HasChor-0.1.0.1: README.md
# HasChor
HasChor is a library for *functional choreographic programming* in Haskell, introduced by our [ICFP 2023 paper](https://doi.org/10.1145/3607849).
Choreographic programming is a programming paradigm where one writes a single program that describes the complete behavior of a distributed system and then compiles it to individual programs that run on each node.
In this way, the generated programs are guaranteed to be *deadlock-free*.
HasChor has the following features:
- HasChor provides a *monadic* interface for choreographic programming where choreographies are expressed as computations in a monad.
- HasChor is implemented as an *embedded* domain-specific language, enabling it to inherent features and libraries from Haskell for free.
- HasChor is built on top of *freer monads*, leading to a flexible, extensible, and concise implementation.
You can find the API specification [here](https://gshen42.github.io/HasChor/).
## Usage
### From Hackage
Simply list `HaChor` in your cabal `build-depends` field, and you're ready to go!
### From the Source Repository
Create a `cabal.project` file and list HasChor's repository as an external source:
``` cabal-config
packages:
. -- your package
source-repository-package
type: git
location: https://github.com/gshen42/HasChor.git
branch: main
```
Alternatively, if you want to make changes to HasChor, you could clone the repository and list it as a local package in the `cabal.project` file:
``` cabal-config
packages:
. -- your package
./HasChor -- path to HasChor repository
```
Either way, you can then list `HasChor` as a dependency in your `.cabal` file:
``` cabal-config
build-depends:
, base
, HasChor
```
## A Tour of HasChor
Let's say we want to implement a bookshop protocol with three participants: a buyer, a seller, and a deliverer.
The protocol goes as follows:
1. The buyer sends the title of a book they want to buy to the seller.
2. The seller replies to the buyer with the price of the book.
3. The buyer decides whether or not to buy the book based on their budget.
1. If yes. The seller sends the title to the deliverer and gets back a delivery date, then forwards it to the buyer.
2. If no. The protocol ends.
In HasChor, we could implement the bookshop protocol as the following program:
``` haskell
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
module Main where
import Choreography (Choreo, cond, locally, mkHttpConfig,
runChoreography, type (@), (~>))
import Control.Monad (void)
import Data.Proxy (Proxy (..))
import System.Environment (getArgs)
buyer :: Proxy "buyer"
buyer = Proxy
seller :: Proxy "seller"
seller = Proxy
deliverer :: Proxy "deliverer"
deliverer = Proxy
priceOf :: String -> Int
priceOf "Types and Programming Languages" = 80
priceOf "Homotopy Type Theory" = 120
priceOf _ = 100
type Date = String
deliveryDateOf :: String -> Date
deliveryDateOf "Types and Programming Languages" = "2002-01-04"
deliveryDateOf "Homotopy Type Theory" = "2013-04-20"
deliveryDateOf _ = "1970-01-01"
budget :: Int
budget = 100
bookshop :: Choreo IO (Maybe Date @ "buyer")
bookshop = do
title <- buyer `locally` \un -> getLine
title' <- (buyer, title) ~> seller
price <- seller `locally` \un -> return $ priceOf (un title')
price' <- (seller, price) ~> buyer
decision <- buyer `locally` \un -> return $ (un price') <= budget
cond (buyer, decision) \case
True -> do
title'' <- (seller, title') ~> deliverer
date <- deliverer `locally` \un -> return $ deliveryDateOf (un title'')
date' <- (deliverer, date) ~> seller
date'' <- (seller, date') ~> buyer
buyer `locally` \un -> do
putStrLn $ "The book will be delivered on " ++ (un date'')
return $ Just (un date'')
False ->
buyer `locally` \un -> do
putStrLn "The book is out of the budget"
return Nothing
main :: IO ()
main = do
[loc] <- getArgs
void $ runChoreography cfg bookshop loc
where
cfg = mkHttpConfig
[ ("buyer", ("localhost", 4242))
, ("seller", ("localhost", 4343))
, ("deliverer", ("localhost", 4444))
]
```
First, we define a set of locations we will use in the choreography.
Locations are HasChor's abstraction for nodes in a distributed system — they are just `String`s.
Since HasChor also uses locations at the type level, we turn on the `DataKinds` extension and define term-level `Proxy`s (`buyer`, `seller`, `deliverer`) for them.
Next, we have some auxiliary definitions (`priceOf`, `deliveryDateOf`, `budget`) for use in the choreography.
`bookshop` is a choreography that implements the bookshop protocol:
- `Choreo m a` is a monad that represents a choreography that returns a value of type `a`.
The `m` parameter is another monad that represents the local computation that locations can perform.
- `a @ l` is a located value that represents a value of type `a` at location `l`.
It's kept opaque to the user to avoid misusing values at locations they're not at.
- `locally :: Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)` is the operator for performing a local compuation at a location.
It takes a location `l`, a local computation `m a` with access to a unwrap function, and returns a value at `l`.
The unwrap function is of type `Unwrap l = a @ l -> a`, which can only unwrap values at `l`.
- `(~>) :: (Proxy l, a @ l) -> Proxy l' -> Choreo m (a @ l')` is the operator for communication between two locations.
It turns a value at `l` to the same value at `l'`.
- `cond :: (Proxy l, a @ l) -> (a -> Choreo m b) -> Choreo m b` is the operator for conditional execution.
It takes a condition `a` at `l`, a function `a -> Choreo m b` denoting branches, and returns one of the branches.
Finally, we use `runChoreography :: Backend cfg => cfg -> Choreo m a -> String -> m a` to project the choreography to a particular location and run the resulting program.
`runChoregraphy` takes a *backend configuration* cfg which specifies the message transport backend that acutally handles sending and receives messages.
## More Examples
HasChor comes with a set of illustrative examples in the [examples](examples) directory.
They are built as executables alongside the HasChor library and can be run with:
``` bash
cabal run executable-name location
```
## Further Readings
- [Introduction to Choreographies](https://www.fabriziomontesi.com/introduction-to-choreographies/)
- [Pirouette: higher-order typed functional choreographies](https://dl.acm.org/doi/10.1145/3498684)