packages feed

MultiChor (empty) → 1.0.0.0

raw patch · 43 files changed

+5560/−0 lines, 43 filesdep +Cabaldep +MultiChordep +QuickCheck

Dependencies added: Cabal, MultiChor, QuickCheck, async, base, binary, bytestring, cabal-detailed-quickcheck, containers, cryptonite, finite-field, http-client, mtl, random, servant, servant-client, servant-server, split, template-haskell, time, transformers, unordered-containers, warp

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2024, Mako Bates++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Gan Shen nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ LICENSE.inherited view
@@ -0,0 +1,34 @@+MultiChor is based on the earlier HasChor; code, documentation, and associated+material that is unchanged from said earlier work retains the original+license and copyright, included below:++Copyright (c) 2022, Gan Shen;++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Gan Shen nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ MultiChor.cabal view
@@ -0,0 +1,230 @@+cabal-version:      3.0+name:               MultiChor+version:            1.0.0.0+license-files:+    , LICENSE+    , LICENSE.inherited+license:            BSD-3-Clause+maintainer: mako.bates@uvm.edu+category: Distributed-Computing+synopsis: Type-safe and efficient choreographies with location-set polymorphism.+description:+    MultiChor is a library for functional choreographic programming in Haskell.++tested-with:+    GHC == 9.4.8++extra-doc-files:+    README.md++source-repository head+  type:     git+  location: https://github.com/ShapeOfMatter/MultiChor+++common basic-config+    default-language: GHC2021+    build-depends:+        , base                 >= 4.16 && < 4.20+        , bytestring           >= 0.11 && < 0.13+        , http-client          >= 0.7  && < 0.8+        , mtl                  >= 2.2.2 && < 3.0+        , servant              >= 0.19 && < 0.21+        , servant-client       >= 0.19 && < 0.21+        , servant-server       >= 0.19 && < 0.21+        , template-haskell     >= 2.18 && < 2.22+        , unordered-containers >= 0.2  && < 0.3+        , warp                 >= 3.3  && < 3.4+    ghc-options:+      -Wall+      -Wno-incomplete-uni-patterns+      -fprint-potential-instances+      -haddock+      -Winvalid-haddock+    default-extensions: BlockArguments+                       ,DataKinds+                       ,ExplicitNamespaces+                       ,FunctionalDependencies+                       ,GADTs+                       ,ImpredicativeTypes+                       ,LambdaCase+                       ,LiberalTypeSynonyms+                       ,TypeFamilies++library+    import: basic-config+    hs-source-dirs:   src+    exposed-modules:+        Choreography+        Choreography.Choreography+        Choreography.Choreography.Batteries+        Choreography.Core+        Choreography.Locations+        Choreography.Locations.Batteries+        Choreography.Network+        Choreography.Network.Http+        Choreography.Network.Local+        Choreography.Polymorphism+        Control.Monad.Freer++common lib-dependent+    import: basic-config+    build-depends: MultiChor+++common example+    import: lib-dependent+    hs-source-dirs:   examples+    build-depends:+        , async      >= 2.2  && < 2.3+        , binary               >= 0.8.9.0 && < 0.10.1.0+        -- trying to get hls to work with TestSuite+        , Cabal >= 3.6.3 && < 3.7+        , cabal-detailed-quickcheck >= 0.2.0 && < 0.3+        --+        , containers >= 0.6  && < 0.7+        , cryptonite           >= 0.10  && < 0.31+        , finite-field >= 0.10.0 && < 0.11.0+        , split   >= 0.2  && < 0.3+        , random  >= 1.2  && < 1.3+        , time    >= 1.11 && < 1.13+        , transformers >= 0.5  && < 0.7+        , QuickCheck >= 2.14 && < 3+    other-modules: Data+                 , CLI++Test-Suite testExamples+    import: example+    type:             detailed-0.9+    test-module:      Tests+    other-modules: Data+                 , Bank2PC+                 , Bookseller0Network+                 , Bookseller1Simple+                 , Bookseller2HigherOrder+                 , Bookseller3LocPoly+                 , BooksellerFancy+                 , CardGame+                 , ChooseTeams+                 , DelegationFig20+                 , DiffieHellman+                 , GMWReal+                 , Karatsuba+                 , KVS1Simple+                 , KVS2PrimaryBackup+                 , KVS3HigherOrder+                 , KVS4LocPoly+                 , KVS5Fig17+                 , KVS6SizePoly+                 , KVS7SimplePoly+                 , Lottery+                 , MergeSort+                 , MPCFake+                 , ObliviousTransfer+                 , QuickSort+                 , RingLeader++executable bank-2pc+    import: example+    main-is:          Bank2PC.hs+    ghc-options:+      -main-is Bank2PC++executable lottery+    import: example+    main-is:          Lottery.hs+    ghc-options:+      -main-is Lottery+++executable bookseller-0-network+    import: example+    main-is:          Bookseller0Network.hs+    ghc-options:+      -main-is Bookseller0Network++executable bookseller-1-simple+    import: example+    main-is:          Bookseller1Simple.hs+    ghc-options:+      -main-is Bookseller1Simple++executable bookseller-2-higher-order+    import: example+    main-is:          Bookseller2HigherOrder.hs+    ghc-options:+      -main-is Bookseller2HigherOrder++executable bookseller-3-loc-poly+    import: example+    main-is:          Bookseller3LocPoly.hs+    ghc-options:+      -main-is Bookseller3LocPoly++executable diffiehellman+    import: example+    main-is:          DiffieHellman.hs+    ghc-options:+      -main-is DiffieHellman++executable gmw-real+    import: example+    main-is:          GMWReal.hs+    ghc-options:+      -main-is GMWReal+    other-modules:+      ObliviousTransfer++executable karatsuba+    import: example+    main-is:          Karatsuba.hs+    ghc-options:+      -main-is Karatsuba++executable kvs1+    import: example+    main-is:          KVS1Simple.hs+    ghc-options:+      -main-is KVS1Simple++executable kvs2+    import: example+    main-is:          KVS2PrimaryBackup.hs+    ghc-options:+      -main-is KVS2PrimaryBackup++executable kvs3+    import: example+    main-is:          KVS3HigherOrder.hs+    ghc-options:+      -main-is KVS3HigherOrder++executable kvs4+    import: example+    main-is:          KVS4LocPoly.hs+    ghc-options:+      -main-is KVS4LocPoly++executable mergesort+    import: example+    main-is:          MergeSort.hs+    ghc-options:+      -main-is MergeSort++executable oblivious-transfer+    import: example+    main-is:          ObliviousTransfer.hs+    ghc-options:+      -main-is ObliviousTransfer++executable quicksort+    import: example+    main-is:          QuickSort.hs+    ghc-options:+      -main-is QuickSort++executable ring-leader+    import: example+    main-is:          RingLeader.hs+    ghc-options:+      -main-is RingLeader
+ README.md view
@@ -0,0 +1,100 @@+# MultiChor++MultiChor is a library for writing choreographic programs in Haskell.++That means you write _one_ program, a _"choreography"_ which seamlessly describes the actions of _many_ communicating machines;+these participants can be native Haskell threads, or various humans' laptops communicating over HTTPS, or anything in between.+Each of these "endpoints" will "project" their behavior out of the choreography.++Choreographies aren't just easier to write than distributed programs, they're automatically deadlock-free!++MultiChor uses some of the same conventions and internal machinery as [HasChor](https://hackage.haskell.org/package/HasChor),+but the API is incompatible and can express more kinds of choreographic behavior.++- The heart of the MultiChor library is a choreography monad `Choreo ps m a`.+  - `ps` is a type-level list of parties participating in the choreography,+  - `m` is an monad used to write _local_ actions those parties can take (often this is simply `IO`),+  - `a` is the returned value, typically this will be a `Located` or `Faceted` value as described below.+- MultiChor is an _embedded_ DSL, as interoperable with the rest of the Haskell ecosystem as any other monad.+  In particular, MultiChor gets recursion, polymorphism, and location-polymorphism "for free" as features of Haskell!+- MultiChor uses enclaves, and multiply-located values to achieve excellent expressivity and efficient Knowledge of Choice management.+  - A value of type `Located ls a` is a single `a` known to all the parties listed in `ls`.+    In a well-typed choreography, other parties, who may not know the `a`, will never attempt to use it.+  - In the expression `(s, v) ~> rs`, a sender `s` sends the value `v` to _all_ of the recipients in `rs`, resulting in a `Located rs v`.+- Safe handing of parties, party-sets, and located values is enforced using term-level proof objects.+  In particular, instead of specifying the party `"alice"` in a choreography as a `String` or a `Proxy "alice"`,+  they're specified by a "proof" that the type-level `"alice"` is present in the choreography and has access to the relevant values.+  MultiChor provides utilities to write these proofs compactly.+- In addition to location polymorphism, MultiChor allows you to write choreographies+  that are polymorphic with respect to the _number of parties_ in a polymorphic party-set.+  This is trivial if they're passively receiving values; new functions allow them to actively communicate:+  - `fanOut` lets a single party send different values (of the same type `a`) to a list of parties `rs`, resulting in a `Faceted rs a`.+  - `fanIn` lets a list of parties `ss` each send a value to the same parties `rs`, resulting in a `Located rs (Quire ss a)`.+  - A `x :: Faceted ps qs a` represents _distinct_ `a`s known to each of `ps` _respectively_; the parties in `qs` know _all_ the `a`s.+- MultiChor allows parallel behavior of many parties to be concisely expressed.+  - `parallel` lets many parties perform local monadic actions in parallel using their `Located` and `Faceted` values;+    the return is `Faceted`.+  - `congruently` lets many parties perform _the same pure computation_ in parallel, using only their `Located` values;+    the return is `Located`.++## Examples++Consider the choreography `game`:++```haskell+{- A simple black-jack-style game. The dealer gives everyone a card, face up. Each player may+ - request a second card. Then the dealer reveals one more card that applies to everyone. Each+ - player individually wins if the sum of their cards (modulo 21) is greater than 19.  -}+game :: forall players m. (KnownSymbols players) => Choreo ("dealer" ': players) (CLI m) ()+game = do+  let players = consSuper (refl @players)+      dealer = listedFirst @"dealer"+      everyone = refl @("dealer" ': players)+  hand1 <-+    ( fanIn everyone \(player :: Member player players) -> do+        card1 <- locally dealer (\_ -> getInput ("Enter random card for " ++ toLocTm player))+        (dealer, card1) ~> everyone+      )+      >>= naked everyone+  wantsNextCard <- parallel players \_ _ -> do+    putNote $ "All cards on the table: " ++ show hand1+    getInput "I'll ask for another? [True/False]"+  hand2 <- fanOut \(player :: Member player players) ->+    enclave (inSuper players player @@ dealer @@ nobody) do+      let dealer' = listedSecond @"dealer"+      choice <- broadcast (listedFirst @player, localize player wantsNextCard)+      if choice+        then do+          cd2 <- locally dealer' (\_ -> getInput (toLocTm player ++ "'s second card:"))+          card2 <- broadcast (dealer', cd2)+          return [getLeaf hand1 player, card2]+        else return [getLeaf hand1 player]+  tblCrd <- locally dealer (\_ -> getInput "Enter a single card for everyone:")+  tableCard <- (dealer, tblCrd) ~> players+  void $ parallel players \player un -> do+    let hand = un player tableCard : viewFacet un player hand2+    putNote $ "My hand: " ++ show hand+    putOutput "My win result:" $ sum hand > card 19+```++The type signature tells us that this choreography (computation in the `Choreo` monad)+involves a partially-polymorphic list of participants;+the first of whom is specifically `"dealer"` and the rest of whom are represented collectively in the type variable `players`.+All parties can perform computations in a local monad, in this case `CLI m`+(the details of `CLI` are orthogonal to choreographic programming; it's basically just `IO`).+The return type `()` indicates that this choreography doesn't yield any values; it's just a program.+The first thing we do is declare the values `players`, `dealer`, and `everyone`;+these are term-level identifiers for the type level parties, but they're also proofs of subset or membership that+attest that the respective parties are valid to participate in the choreography.+`hand1` has type `Quire players Card`; since these cards are supposed to be dealt face down, they're known to everyone.+To accomplish this, we use a `fanIn` loop in which the dealer selects a card for each player and sends it to everyone.+`wantsNextCard` is the result of a parallel computation (CLI interaction);+it's type is `Faceted players '[] Bool`.+The computation of `hand2` is private between each player and the dealer, so we `fanOut` over the players+and then `enclave` a sub-choreography involving only the given player and `"dealer"`.+The `broadcast` inside the enclave shares that player's value of `wantsNextCard` with everyone _who's present_, which is just `"dealer"`.+At the end, the players each observer if they've won or lost in parallel.++Check the source repository for many more example choreographies.+You can also read the preprint of [_Efficient, Portable, Census-Polymorphic Choreographic Programming_](https://arxiv.org/abs/2412.02107)+for more theoretical discussion of choreographic programming _à la_ MultiChor.
+ examples/Bank2PC.hs view
@@ -0,0 +1,178 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# Example: bank-2pc++## Overview++This example implements the two-phase commit protocol.++This system models a bank. Alice and Bob each have their accounts on the bank, and the balance of each account is stored at separate locations `alice` and `bob`. This bank has a policy that does not allow balances to be negative.++As a bank administrator, you can change the balance of accounts. An `Action` changes a single account's balance by specifying the account (`String`, "alice" or "bob") and the amount to add to the account (Int, can be negative to indicate withdrawal). A `Transaction` is a list of `Action`s.++When executing a `Transaction`, the system will perform Alice's actions at `alice` and Bob's actions at `bob`. However, the transaction aborts if one of the actions violates the bank policy and makes the balance negative. We use the two-phase commit protocol to ensure consistency between `alice` and `bob`.++In the voting phase, `alice` and `bob` check if the given transaction violates the policy. If one or more locations determine that the transaction violates the policy, the entire transaction aborts. If the transaction is valid, each location will commit the transaction.++## Execution++For simplicity, this example uses `runChoreo` and executes the choreography directly. On the terminal, you can write transactions as follows. Both accounts' balances are initialized to 0.++```text+> cabal run bank-2pc+Command? (alice|bob {amount};)++alice 10; bob 10                  # deposit 10 each to Alice and Bob's accounts+Committed+Alice's balance: 10+Bob's balance: 10+Command? (alice|bob {amount};)+   # deposit 20 to Alice's and withdraw 10 from Bob's+alice 20; bob -5+Committed+Alice's balance: 30+Bob's balance: 5+Command? (alice|bob {amount};)+   # move 10 from Bob to Alice (Invalid, Bob's account will be negative)+alice 10; bob -10+Not committed+Alice's balance: 30+Bob's balance: 5+```+-}++module Bank2PC where++import CLI+import Choreography+import Control.Monad (unless)+import Data (TestArgs, reference)+import Data.List (intercalate, transpose)+import Data.List.Split (splitOn)+import Data.Maybe (mapMaybe)+import Data.Proxy (Proxy (Proxy))+import GHC.TypeLits (KnownSymbol, symbolVal)+import Test.QuickCheck (Arbitrary, arbitrary, elements, listOf, listOf1)+import Text.Read (readMaybe)++$(mkLoc "client")+$(mkLoc "coordinator")+$(mkLoc "alice")+$(mkLoc "bob")++type Participants = ["client", "coordinator", "alice", "bob"]++type State = (Located '["alice"] Int, Located '["bob"] Int)++type Action = (String, Int)++type Transaction = [Action]++newtype Args p q = Args [Transaction] deriving (Eq, Show, Read)++instance (KnownSymbol p, KnownSymbol q) => TestArgs (Args p q) [[String]] where+  reference (Args tx) = addCoordinator . transpose $ showAll <$> ref start tx+    where+      start = (,0) <$> [symbolVal (Proxy @p), symbolVal (Proxy @q)]+      ref _ [] = []+      ref state (t : ts) =+        let (s', r) = refAs state t+            s'' = if r then s' else state+         in (r, s'') : ref s'' ts+      refAs state [] = (state, True)+      refAs state (a : as) =+        let (s', r) = refA state a+         in if r then refAs s' as else (state, False)+      refA state (name, amount) =+        let (otherL, (_, s) : otherR) = ((== name) . fst) `break` state+            s' = s + amount+         in (otherL ++ ((name, s') : otherR), 0 <= s')+      showAll :: (Bool, [(String, Int)]) -> [String]+      showAll (clnt, servers) = show clnt : (show . snd <$> servers)+      addCoordinator (clnt : servers) = clnt : [] : servers+      addCoordinator _ = error "this can't happen, right? I could enforce it by types, but it's a core..."++instance (KnownSymbol p, KnownSymbol q) => Arbitrary (Args p q) where+  arbitrary = (Args . (++ [[]]) <$>) . listOf . listOf1 $ (,) <$> elements [symbolVal $ Proxy @p, symbolVal $ Proxy @q] <*> arbitrary++-- | `validate` checks if a transaction can be executed while keeping balance >= 0+-- returns if the transaction satisfies the property and the balance after the transaction+validate :: String -> Int -> Transaction -> (Bool, Int)+validate name balance tx = foldl (\(valid, i) (_, amount) -> (let next = i + amount in (valid && next >= 0, next))) (True, balance) actions+  where+    actions = filter (\(n, _) -> n == name) tx++render :: Transaction -> String+render txns = intercalate ";" $ (\(a, b) -> a ++ " " ++ show b) <$> txns++-- | `parse` converts the user input into a transaction+parse :: String -> Transaction+parse s = tx+  where+    t = splitOn ";" s+    f :: String -> Maybe Action+    f l = do+      [target, amountStr] <- return $ words l+      amount <- readMaybe amountStr :: Maybe Int+      target' <- if target == "alice" || target == "bob" then Just target else Nothing+      return (target', amount)+    tx = mapMaybe f t++-- | `handleTransaction` is a choreography that handles a transaction.+-- Given the current state and a transaction, it will first ask alice and bob to vote,+-- then it will decide whether to commit the transaction or not.+-- If the transaction is committed, it will update the state.+-- Otherwise, it will keep the state unchanged.+handleTransaction ::+  (Monad m) =>+  State ->+  Located '["coordinator"] Transaction ->+  Choreo Participants m (Located '["coordinator"] Bool, State)+handleTransaction (aliceBalance, bobBalance) tx = do+  -- Voting Phase+  txa <- (coordinator, tx) ~> alice @@ nobody+  voteAlice <- (alice, \un -> do { return $ fst $ validate "alice" (un alice aliceBalance) (un alice txa) }) ~~> coordinator @@ nobody+  txb <- (coordinator, tx) ~> bob @@ nobody+  voteBob <- (bob, \un -> do { return $ fst $ validate "bob" (un bob bobBalance) (un bob txb) }) ~~> coordinator @@ nobody++  -- Check if the transaction can be committed+  canCommit <- coordinator `locally` \un -> do return $ un coordinator voteAlice && un coordinator voteBob++  -- Commit Phase+  broadcast (coordinator, canCommit) >>= \case+    True -> do+      aliceBalance' <- alice `locally` \un -> do return $ snd $ validate "alice" (un alice aliceBalance) (un alice txa)+      bobBalance' <- bob `locally` \un -> do return $ snd $ validate "bob" (un bob bobBalance) (un bob txb)+      return (canCommit, (aliceBalance', bobBalance'))+    False -> do+      return (canCommit, (aliceBalance, bobBalance))++-- | `bank` loops forever and handles transactions.+bank :: State -> Choreo Participants (CLI m) ()+bank state = do+  tx <-+    ( client,+      parse <$> getstr "Command? (alice|bob {amount};)+"+      )+      -~> coordinator+      @@ nobody+  (committed, state') <- handleTransaction state tx+  committed' <- (coordinator, committed) ~> client @@ nobody+  client `locally_` \un -> putOutput "Committed?" (un client committed')+  alice `locally_` \un -> putOutput "Alice's balance:" (un alice (fst state'))+  bob `locally_` \un -> putOutput "Bob's balance:" (un bob (snd state'))+  c <- coordinator `locally` (\un -> return $ null $ un coordinator tx)+  broadcast (coordinator, c) >>= (`unless` bank state') -- repeat++-- | `startBank` is a choreography that initializes the states and starts the bank application.+startBank :: Choreo Participants (CLI m) ()+startBank = do+  aliceBalance <- alice `_locally` return 0+  bobBalance <- bob `_locally` return 0+  bank (aliceBalance, bobBalance)++main :: IO ()+main = do+  runCLIIO $ runChoreo startBank
+ examples/Bookseller0Network.hs view
@@ -0,0 +1,63 @@+module Bookseller0Network where++{-+# Bookseller as individual network programs++This example implmenets the bookseller protocol as individual network+programs (non-choreographic way). See+[`bookseller-1-simple`](../bookseller-1-simple) for a description of+the protocol.++## Running the example++Same as [`bookseller-1-simple`](../bookseller-1-simple) but with `cabal run bookseller-0-network`.+-}++import CLI+import Choreography.Network+import Choreography.Network.Http+import Data (deliveryDateOf, priceOf)+import Data.Time+import System.Environment++buyer :: Network (CLI m) ()+buyer = do+  budget <- run $ getInput @Int "Enter your total budget:"+  title <- run $ getstr "Enter the title of the book to buy:"+  send title ["seller"]+  price <- recv "seller"+  if price <= budget+    then do+      send True ["seller"]+      (deliveryDate :: Day) <- recv "seller"+      run $ putOutput "The book will be delivered on:" deliveryDate+    else do+      send False ["seller"]+      run $ putNote "The book's price is out of the budget"++seller :: Network (CLI m) ()+seller = do+  database <- run $ getInput "Enter the book database (for `Read`):"+  title <- recv "buyer"+  send (database `priceOf` title) ["buyer"]+  decision <- recv "buyer"+  if decision+    then do+      send (database `deliveryDateOf` title) ["buyer"]+    else do+      return ()++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "buyer" -> runCLIIO $ runNetwork cfg "buyer" buyer+    "seller" -> runCLIIO $ runNetwork cfg "seller" seller+    _ -> error "unknown party"+  return ()+  where+    cfg =+      mkHttpConfig+        [ ("buyer", ("localhost", 4242)),+          ("seller", ("localhost", 4343))+        ]
+ examples/Bookseller1Simple.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++module Bookseller1Simple where++import CLI+import Choreography+import Choreography.Network.Http+import Data (deliveryDateOf, priceOf)+import System.Environment++$(mkLoc "buyer")+$(mkLoc "seller")++type Participants = ["buyer", "seller"]++-- | `bookseller` is a choreography that implements the bookseller protocol.+bookseller :: Choreo Participants (CLI m) ()+bookseller = do+  database <- seller `_locally` getInput "Enter the book database (for `Read`):"+  buyer_budget <- buyer `_locally` getInput "Enter your total budget:"+  title <- buyer `_locally` getstr "Enter the title of the book to buy:"++  title' <- (buyer, title) ~> seller @@ nobody+  price <- seller `locally` \un -> return $ priceOf (un seller database) (un seller title')+  price' <- (seller, price) ~> buyer @@ nobody+  decision <- buyer `locally` \un -> return $ un buyer price' <= un buyer buyer_budget++  broadcast (buyer, decision) >>= \case+    True -> do+      deliveryDate <- seller `locally` \un -> return $ deliveryDateOf (un seller database) (un seller title')+      deliveryDate' <- (seller, deliveryDate) ~> buyer @@ nobody+      buyer `locally_` \un -> putOutput "The book will be delivered on:" $ un buyer deliveryDate'+    False -> do+      buyer `_locally_` putNote "The book's price is out of the budget"++-- `bookseller'` is a simplified version of `bookseller` that utilizes `~~>`+bookseller' :: Choreo Participants (CLI m) ()+bookseller' = do+  database <- seller `_locally` getInput "Enter the book database (for `Read`):"+  buyer_budget <- buyer `_locally` getInput "Enter your total budget:"+  title <- (buyer, getstr "Enter the title of the book to buy:") -~> seller @@ nobody+  price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> buyer @@ nobody++  inBuyerBudget <- buyer `locally` (\un -> return $ un buyer price <= un buyer buyer_budget)+  broadcast (buyer, inBuyerBudget) >>= \case+    True -> do+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> buyer @@ nobody+      buyer `locally_` \un -> putOutput "The book will be delivered on:" $ un buyer deliveryDate+    False -> do+      buyer `_locally_` putNote "The book's price is out of the budget"++main :: IO ()+main = do+  [loc] <- getArgs+  delivery <- case loc of+    "buyer" -> runCLIIO $ runChoreography cfg bookseller' "buyer"+    "seller" -> runCLIIO $ runChoreography cfg bookseller' "seller"+    _ -> error "unknown party"+  print delivery+  where+    cfg =+      mkHttpConfig+        [ ("buyer", ("localhost", 4242)),+          ("seller", ("localhost", 4343))+        ]
+ examples/Bookseller2HigherOrder.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# Higher-order bookseller++This example implements the higher-order bookseller protocol where+how the buyer decides whether to buy the book is abstracted as an+argument, making it a higher-order choreography.+For a general description of the protocol, see [`bookseller-1-simple`](../bookseller-1-simple).++We provide two decision-making functions:++- `mkDecision1` only checks if buyer's budget is greater than the+  book's price, which has the same behavior as [`bookseller-1-simple`](../bookseller-1-simple)+- `mkDecision2` asks buyer2 how much they're willing to contribute and+  checks if the buyer's budget is greater than the book's price minus+  buyer2's contribution.++By default, this example uses `mkDecision2`. To use `mkDecision1`,+change the line `choreo = bookseller mkDecisiont2` to `choreo = bookseller mkDecision1`.++## Running the protocol++```bash+# 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 previously in [`bookseller-1-simple`](../bookseller-1-simple),+the buyer can't buy `Homotopy Type Theory` as it's out of the budget,+but with buyer2's contribution, now it can.+-}++module Bookseller2HigherOrder where++import CLI+import Choreography+import Choreography.Network.Http+import Data (deliveryDateOf, priceOf)+import System.Environment++$(mkLoc "buyer")+$(mkLoc "seller")+$(mkLoc "buyer2")++type Participants = ["buyer", "seller", "buyer2"]++-- | `bookseller` is a choreography that implements the bookseller protocol.+-- This version takes a choreography `mkDecision` that implements the decision making process.+bookseller ::+  (Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool)) ->+  Choreo Participants (CLI m) ()+bookseller mkDecision = do+  database <- seller `_locally` getInput "Enter the book database (for `Read`):"+  title <- (buyer, getstr "Enter the title of the book to buy:") -~> seller @@ nobody++  -- the seller checks the price of the book and sends it to the buyer+  price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> buyer @@ nobody++  -- the buyer makes a decision using the `mkDecision` choreography+  decision <- mkDecision price++  -- if the buyer decides to buy the book, the seller sends the delivery date to the buyer+  broadcast (buyer, decision) >>= \case+    True -> do+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> buyer @@ nobody+      buyer `locally_` \un -> putstr "The book will be delivered on:" $ show (un buyer deliveryDate)+    False -> do+      buyer `_locally_` putNote "The book's price is out of the budget"++-- | `mkDecision1` checks if buyer's budget is greater than the price of the book+mkDecision1 :: Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool)+mkDecision1 price = do+  budget <- buyer `_locally` getInput "What are you willing to pay?"+  buyer `locally` \un -> return $ un buyer price <= un buyer budget++-- | `mkDecision2` asks buyer2 how much they're willing to contribute and checks+-- if the buyer's budget is greater than the price of the book minus buyer2's contribution+mkDecision2 :: Located '["buyer"] Int -> Choreo Participants (CLI m) (Located '["buyer"] Bool)+mkDecision2 price = do+  contrib1 <- buyer `_locally` getInput "What are you willing to pay?"+  contrib2 <- (buyer2, getInput "How much you're willing to contribute?") -~> buyer @@ nobody+  buyer `locally` \un -> return $ un buyer price - un buyer contrib2 <= un buyer contrib1++main :: IO ()+main = do+  [loc] <- getArgs+  _ <- case loc of+    "buyer" -> runCLIIO $ runChoreography cfg choreo "buyer"+    "seller" -> runCLIIO $ runChoreography cfg choreo "seller"+    "buyer2" -> runCLIIO $ runChoreography cfg choreo "buyer2"+    _ -> error "unknown party"+  return ()+  where+    choreo = bookseller mkDecision2++    cfg =+      mkHttpConfig+        [ ("buyer", ("localhost", 4242)),+          ("seller", ("localhost", 4343)),+          ("buyer2", ("localhost", 4444))+        ]
+ examples/Bookseller3LocPoly.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# Location-polymorphic bookseller++This example implements the location-polymorphic bookseller where the+buyer's location is abstracted away as an argument.++For a general description of the protocol, see [`bookseller-1-simple`](../bookseller-1-simple).++# Running the protocol++Same as [`bookseller-1-simple`](../bookseller-1-simple) but with `cabal run bookseller-3-loc-poly`.+-}++module Bookseller3LocPoly where++import CLI+import Choreography+import Choreography.Network.Http+import Data (deliveryDateOf, priceOf)+import GHC.TypeLits+import System.Environment++$(mkLoc "buyer")+$(mkLoc "seller")++-- type Participants = ["buyer", "seller"]++-- | `bookseller` is a choreography that implements the bookseller protocol.+-- This version takes the name of the buyer as a parameter (`someBuyer`).+bookseller :: (KnownSymbol a, KnownSymbols ps) => Member a ps -> Choreo ("seller" ': ps) (CLI m) ()+bookseller someBuyer = do+  let theBuyer = inSuper consSet someBuyer+  database <- seller `_locally` getInput "Enter the book database (for `Read`):"+  buyer_budget <- theBuyer `_locally` getInput "Enter your total budget:"+  -- the buyer reads the title of the book and sends it to the seller+  title <- (theBuyer, getstr "Enter the title of the book to buy") -~> seller @@ nobody+  -- the seller checks the price of the book and sends it to the buyer+  price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> theBuyer @@ nobody++  inBuyerBudget <- theBuyer `locally` (\un -> return $ un singleton price <= un singleton buyer_budget)+  broadcast (theBuyer, inBuyerBudget) >>= \case+    True -> do+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> theBuyer @@ nobody++      theBuyer `locally_` \un -> putOutput "The book will be delivered on:" $ un singleton deliveryDate+    False -> do+      theBuyer `_locally_` putNote "The book's price is out of the budget"++main :: IO ()+main = do+  [loc] <- getArgs+  _ <- case loc of+    "buyer" -> runCLIIO $ runChoreography cfg choreo "buyer"+    "seller" -> runCLIIO $ runChoreography cfg choreo "seller"+    _ -> error "unknown party"+  return ()+  where+    choreo = bookseller $ singleton @"buyer"++    cfg =+      mkHttpConfig+        [ ("buyer", ("localhost", 4242)),+          ("seller", ("localhost", 4343))+        ]
+ examples/BooksellerFancy.hs view
@@ -0,0 +1,94 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# Maximally fancy bookseller+-}++module BooksellerFancy where++import CLI+import Choreography+import Choreography.Network.Http+import Data (deliveryDateOf, priceOf)+import System.Environment++$(mkLoc "buyer")+$(mkLoc "seller")++-- | `bookseller` is a choreography that implements the bookseller protocol.+-- This version takes a choreography `mkDecision` that implements the decision making process.+bookseller ::+  forall supporters {m}.+  (KnownSymbols supporters) =>+  (Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool)) ->+  Choreo ("buyer" ': "seller" ': supporters) (CLI m) ()+bookseller mkDecision = do+  database <- seller `_locally` getInput "Enter the book database (for `Read`):"+  title <- (buyer, getstr "Enter the title of the book to buy:") -~> seller @@ nobody++  -- the seller checks the price of the book and sends it to the buyer+  price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> buyer @@ nobody++  -- the buyer and supporters (transactors) make a decision using the `mkDecision` choreography+  decision <- enclave transactors $ mkDecision price++  -- if the buyer decides to buy the book, the seller sends the delivery date to the buyer+  _ <-+    enclave buyerAndSeller $+      broadcast (buyer, flatten explicitSubset allOf decision) >>= \case+        True -> do+          deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> buyer @@ nobody+          buyer `locally_` \un -> putstr "The book will be delivered on:" $ show (un buyer deliveryDate)+        False -> do+          buyer `_locally_` putNote "The book's price is out of the budget"++  return ()+  where+    transactors :: Subset ("buyer" ': supporters) ("buyer" ': "seller" ': supporters)+    transactors = explicitMember @@ (consSuper . consSuper $ refl)++    buyerAndSeller :: Subset '["buyer", "seller"] ("buyer" ': "seller" ': supporters)+    buyerAndSeller = explicitSubset++-- | `mkDecision1` checks if buyer's budget is greater than the price of the book+mkDecision1 :: Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool)+mkDecision1 price = do+  budget <- buyer `_locally` getInput "What are you willing to pay?"+  buyer `locally` \un -> return $ un buyer price <= un buyer budget++-- | `mkDecision2` asks supporters how much they're willing to contribute and checks+-- if the buyer's budget is greater than the price of the book minus all supporters' contribution+mkDecision2 :: forall supporters {m}. (KnownSymbols supporters) => Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool)+mkDecision2 price = do+  budget <- buyer `_locally` getInput "What are you willing to pay?"++  contribs <- fanIn @supporters explicitSubset $ \supporter ->+    (Later supporter, getInput "How much you're willing to contribute?") -~> buyer @@ nobody+  contrib <-+    buyer `locally` \un ->+      return $ sum (un buyer contribs)+  buyer `locally` \un -> return $ un buyer price <= un buyer budget + un buyer contrib++main :: IO ()+main = do+  [loc] <- getArgs+  _ <- case loc of+    "buyer" -> runCLIIO $ runChoreography cfg choreo "buyer"+    "seller" -> runCLIIO $ runChoreography cfg choreo "seller"+    "buyer2" -> runCLIIO $ runChoreography cfg choreo "buyer2"+    "buyer3" -> runCLIIO $ runChoreography cfg choreo "buyer3"+    _ -> error "unknown party"+  return ()+  where+    choreo = bookseller @["buyer2", "buyer3"] mkDecision2++    cfg =+      mkHttpConfig+        [ ("buyer", ("localhost", 4242)),+          ("seller", ("localhost", 4343)),+          ("buyer2", ("localhost", 4444)),+          ("buyer3", ("localhost", 45454))+        ]
+ examples/CLI.hs view
@@ -0,0 +1,80 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImpredicativeTypes #-}++-- | This module defines `Choreo`, the monad for writing choreographies.+module CLI where++import Control.Monad (unless)+import Control.Monad.Cont (MonadIO (liftIO))+import Control.Monad.Freer+import Control.Monad.State (MonadState (get, put), StateT (runStateT), lift)+import Data.Typeable (Typeable, typeRep)+import Text.Read (readMaybe)++type Context = String++data CLISig m a where+  GetStr :: Context -> CLISig m String+  PutStr :: Context -> String -> CLISig m ()+  Internal :: m a -> CLISig m a++type CLI m = Freer (CLISig m)++instance (MonadIO m) => MonadIO (CLI m) where+  liftIO a = toFreer $ Internal $ liftIO a++runCLIIO :: forall m a. (MonadIO m) => CLI m a -> m a+runCLIIO = interpFreer handler+  where+    handler :: CLISig m b -> m b+    handler (GetStr prompt) = liftIO $ putStrLn prompt >> getLine+    handler (PutStr context l) = liftIO $ putStrLn $ context ++ " " ++ l+    handler (Internal m) = m++getstr :: Context -> CLI m String+getstr context = toFreer $ GetStr context++getln :: CLI m String+getln = getstr ""++getInput :: forall a m. (Read a, Typeable a) => Context -> CLI m a+getInput context = do+  str <- getstr context+  case readMaybe str of+    Just a -> return a+    a@Nothing -> error $ "Failed to read \"" ++ str ++ "\" as a " ++ show (typeRep a)++putstr :: Context -> String -> CLI m ()+putstr context l = toFreer $ PutStr context l++putNote :: Context -> CLI m ()+putNote = (`putstr` "")++putOutput :: (Show a) => Context -> a -> CLI m ()+putOutput context a = putstr context $ show a++data TTYEnv = TTYEnv+  { inputs :: [String],+    outputs :: [String]+  }++runCLIStateful :: forall m a. (MonadFail m, MonadIO m) => [String] -> CLI m a -> m ([String], a)+runCLIStateful ins tma = do+  (a, e) <- runStateT stateful TTYEnv {inputs = ins, outputs = []}+  return (reverse $ outputs e, a)+  where+    stateful :: StateT TTYEnv m a+    stateful = interpFreer handler tma+    handler :: forall b. CLISig m b -> StateT TTYEnv m b+    handler (GetStr c) = do+      env@TTYEnv {inputs} <- get+      case inputs of+        ln : lns -> do+          put env {inputs = lns}+          return ln+        [] -> error $ "No input to go with prompt " ++ show c ++ "."+    handler (PutStr _ o) = unless (null o) $ do+      env@TTYEnv {outputs = os} <- get+      put env {outputs = o : os}+    handler (Internal m) = lift m
+ examples/CardGame.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++module CardGame where++import CLI+import Choreography+import Control.Monad (void)+import Data (TestArgs, reference)+import Test.QuickCheck (Arbitrary, arbitrary, listOf1)++_modulo :: Int -> Int+_modulo = (`mod` 21)++newtype Card = Card_ Int deriving (Eq, Ord, Read, Show)++card :: Int -> Card+card = Card_ . _modulo++instance Num Card where+  (Card_ a) + (Card_ b) = card $ a + b+  (Card_ a) * (Card_ b) = card $ a * b+  abs = id+  signum = const 1+  fromInteger = card . fromInteger+  negate (Card_ a) = card $ (-1) * a++instance Arbitrary Card where+  arbitrary = Card_ <$> arbitrary++type Win = Bool++data Args = Args+  { deck :: [Card],+    choices :: (Bool, Bool, Bool)+  }+  deriving (Eq, Show, Read)++instance TestArgs Args (Bool, Bool, Bool) where+  reference Args {deck, choices = (c1, c2, c3)} =+    let h11 : h21 : h31 : deck1 = cycle deck -- should just use State+        (h12, deck12) = if c1 then ([h11, head deck1], tail deck1) else ([h11], deck1)+        (h22, deck22) = if c2 then ([h21, head deck12], tail deck12) else ([h21], deck12)+        (h32, deck32) = if c3 then ([h31, head deck22], tail deck22) else ([h31], deck22)+        common = head deck32+        [win1, win2, win3] = (> card 19) . sum . (common :) <$> [h12, h22, h32]+     in (win1, win2, win3)++instance Arbitrary Args where+  arbitrary = Args <$> listOf1 arbitrary <*> arbitrary++{- A simple black-jack-style game. The dealer gives everyone a card, face up. Each player may+ - request a second card. Then the dealer reveals one more card that applies to everyone. Each+ - player individually wins if the sum of their cards (modulo 21) is greater than 19.  -}+game :: forall players m. (KnownSymbols players) => Choreo ("dealer" ': players) (CLI m) ()+game = do+  let players = consSuper (refl @players)+      dealer = listedFirst @"dealer" -- listedFirst is just First with the type-arguments rearranged.+      everyone = refl @("dealer" ': players)+  hand1 <-+    ( fanIn everyone \(player :: Member player players) -> do+        card1 <- locally dealer (\_ -> getInput ("Enter random card for " ++ toLocTm player))+        (dealer, card1) ~> everyone+      )+      >>= naked everyone+  wantsNextCard <- parallel players \_ _ -> do+    putNote $ "All cards on the table: " ++ show hand1+    getInput "I'll ask for another? [True/False]"+  hand2 <- fanOut \(player :: Member player players) ->+    enclave (inSuper players player @@ dealer @@ nobody) do+      let dealer' = listedSecond @"dealer"+      choice <- broadcast (listedFirst @player, localize player wantsNextCard)+      if choice+        then do+          cd2 <- locally dealer' (\_ -> getInput (toLocTm player ++ "'s second card:"))+          card2 <- broadcast (dealer', cd2)+          return [getLeaf hand1 player, card2]+        else return [getLeaf hand1 player]+  tblCrd <- locally dealer (\_ -> getInput "Enter a single card for everyone:")+  tableCard <- (dealer, tblCrd) ~> players+  void $ parallel players \player un -> do+    let hand = un player tableCard : viewFacet un player hand2+    putNote $ "My hand: " ++ show hand+    putOutput "My win result:" $ sum hand > card 19
+ examples/ChooseTeams.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++module ChooseTeams where++import CLI+import Choreography+import Control.Monad (when)+import Data (TestArgs, reference)+import Data.Foldable (toList)+import Data.Maybe (catMaybes)+import Test.QuickCheck (Arbitrary, arbitrary)++newtype Args = Args+  { choices :: (Int, Int)+  }+  deriving (Eq, Show, Read)++instance TestArgs Args ([Int], [Int], [Int], [Int], [Int]) where+  reference Args {choices = (c1, c2)} = ([c1, c2], [], [c1, c2], [], [c1, c2])++instance Arbitrary Args where+  arbitrary = Args <$> arbitrary++chooseTeams :: [LocTm] -> ([LocTm], [LocTm]) -- Probably could find it off-the-shelf somewhere...+chooseTeams [] = ([], [])+chooseTeams (a : as) =+  let (t1, t2) = chooseTeams as+   in (t2, a : t1)++-- the game is just red-team sending numbers to blue team.+game :: forall players m. (KnownSymbols players) => Choreo players (CLI m) ()+game = do+  let players = allOf @players+  let (red, blue) = chooseTeams $ toLocs players+  numbers <- fanIn players \p ->+    if toLocTm p `elem` red+      then (p, Just <$> getInput @Int "A number to send:") -~> players+      else enclave players $ return Nothing+  parallel_ players \p un ->+    when (toLocTm p `elem` blue) $+      putOutput "Numbers recieved:" $+        catMaybes . toList $+          un p numbers
+ examples/Data.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE FunctionalDependencies #-}++module Data where++import Data.Time (Day (ModifiedJulianDay), fromGregorian)+import Test.QuickCheck (Arbitrary, Positive (Positive), arbitrary, arbitraryPrintableChar, elements, getPositive, listOf1)++data Book = Book+  { name :: String,+    price :: Int,+    deliverable :: Day+  }+  deriving (Eq, Read, Show)++instance Arbitrary Book where+  arbitrary =+    Book+      <$> listOf1 arbitraryPrintableChar+      <*> (getPositive <$> arbitrary)+      <*> (ModifiedJulianDay . getPositive <$> arbitrary)++type Database = [Book]++textbooks :: Database+textbooks =+  [ Book+      { name = "Types and Programming Languages",+        price = 80,+        deliverable = fromGregorian 2023 12 19+      },+    Book+      { name = "Homotopy Type Theory",+        price = 120,+        deliverable = fromGregorian 2023 09 18+      }+  ]++priceOf :: Database -> String -> Int+priceOf books title = price $ head $ filter ((== title) . name) books++deliveryDateOf :: Database -> String -> Day+deliveryDateOf books title = deliverable $ head $ filter ((== title) . name) books++data BooksellerArgs = BooksellerArgs+  { books :: Database,+    choice :: String,+    budget :: Int+  }+  deriving (Read, Show)++instance Arbitrary BooksellerArgs where+  arbitrary = do+    books <- listOf1 arbitrary+    choice <- name <$> elements books+    budget <- getPositive <$> arbitrary+    return BooksellerArgs {books, choice, budget}++class TestArgs a r | a -> r where+  reference :: a -> r++instance TestArgs BooksellerArgs (Maybe Day) where+  reference (BooksellerArgs {books, choice, budget}) =+    if budget < priceOf books choice+      then Nothing+      else Just $ deliveryDateOf books choice++instance TestArgs (BooksellerArgs, Positive Int) (Maybe Day) where+  reference (BooksellerArgs {books, choice, budget}, Positive contrib) =+    if budget < (priceOf books choice - contrib)+      then Nothing+      else Just $ deliveryDateOf books choice++-- a scenario where there's four buyers (one primary and three supporter)+instance TestArgs (BooksellerArgs, Positive Int, Positive Int, Positive Int) (Maybe Day) where+  reference (BooksellerArgs {books, choice, budget}, Positive contrib, Positive contrib2, Positive contrib3) =+    if budget < (priceOf books choice - contrib - contrib2 - contrib3)+      then Nothing+      else Just $ deliveryDateOf books choice
+ examples/DelegationFig20.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++module DelegationFig20 where++{-+let choice : ()+()@[alice, bob] = com[alice][alice, bob] alices_choice;+let query : Query@[alice] = case[alice, bob] choice of+Inl _ => com[bob][alice] bobs_query;+Inr _ => alices_query;+let answerer : (Query@[carroll] -> Response@[carroll])@[carroll] = carrolls_func;+let response = com[carroll][bob, alice] (answerer (com[alice][carroll] query));+case[alice, bob] choice of+Inl _ => bobs_terminal response;+Inr _ => alices_terminal response;+ -}++import CLI+import Choreography+import Data (TestArgs, reference)+import Data.List (sort)+import Data.Maybe (fromMaybe)+import Test.QuickCheck (Arbitrary, arbitrary, arbitraryPrintableChar, elements, listOf1)++$(mkLoc "alice")+$(mkLoc "bob")+$(mkLoc "carroll")++type Participants = ["alice", "bob", "carroll"]++data Args = Args+  { choice :: Bool,+    aliceQ :: String,+    bobQ :: String,+    carrollF :: String+  }+  deriving (Eq, Show, Read)++data Result = Result+  { aliceR :: [String],+    bobR :: [String],+    carrollR :: [String]+  }+  deriving (Eq, Show, Read)++instance TestArgs Args Result where+  reference Args {choice, aliceQ, bobQ, carrollF} =+    let f = fromMaybe carrollsDefault $ carrollF `lookup` carrollsFunctions+        result = f $ if choice then aliceQ else bobQ+     in Result {aliceR = [result | choice], bobR = [result | not choice], carrollR = []}++instance Arbitrary Args where+  arbitrary =+    Args+      <$> arbitrary+      <*> listOf1 arbitraryPrintableChar -- Avoiding wierd behavior of CLI on empty outputs :(+      <*> listOf1 arbitraryPrintableChar+      <*> elements (fst <$> carrollsFunctions)++carrollsFunctions :: [(String, String -> String)]+carrollsFunctions =+  [ ("reverse", reverse),+    ("alphabetize", sort)+  ]++carrollsDefault :: String -> String+carrollsDefault = const "No Handler"++mainCho :: Choreo Participants (CLI m) ()+mainCho = do+  choice <- (alice, getInput "Alice's choice:") -~> alice @@ bob @@ nobody+  query <-+    flatten (alice @@ nobody) (alice @@ nobody)+      <$> cond (explicitSubset, (refl, choice)) \case+        False -> (bob, getstr "Bob's query:") -~> alice @@ nobody+        True -> alice `_locally` getstr "Alice's query:"+  answerer <-+    carroll `_locally` do+      handlerName <- getstr "Carrol's function (reverse or alphabetize):"+      return $ fromMaybe carrollsDefault $ handlerName `lookup` carrollsFunctions+  query' <- (alice, query) ~> carroll @@ nobody+  response <- (carroll, \un -> return $ un carroll answerer (un carroll query')) ~~> alice @@ bob @@ nobody+  (_ :: Located '["alice", "bob"] ()) <- cond (explicitSubset, (refl, choice)) \case+    False -> bob `locally_` \un -> putstr "Recieved:" (un bob response)+    True -> alice `locally_` \un -> putstr "Recieved:" (un alice response)+  return ()
+ examples/DiffieHellman.hs view
@@ -0,0 +1,113 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# Example: diffie-hellman key exchange++## Overview++This example implements the [diffie-hellman key exchange protocol](https://en.wikipedia.org/wiki/Diffie%E2%80%93Hellman_key_exchange).++In this example, two locations, `alice` and `bob`, exchange the secret key without sending the key over the network.++## Execution++To run this example, you will need to run two locations (alice and bob) at the same time. Alice initiates the exchange, and Bob waits for Alice. When both locations are ready, press "enter" on Alice's terminal to start the protocol.++```+> cabal run diffiehellman bob+waiting for alice to initiate key exchange++# on a different terminal+> cabal run diffiehellman alice+enter to start key exchange...+[Enter]++# Alice's terminal+alice's shared key: 1544++# Bob's terminal+bob's shared key: 1544+```++This sample uses [`System.Random`](https://hackage.haskell.org/package/random-1.2.1.1/docs/System-Random.html) and will generate different keys at each invocation.+-}++module DiffieHellman where++import CLI+import Choreography+import Choreography.Network.Http+import Control.Monad.Cont (MonadIO)+import System.Environment+import System.Random++-- helper functions around prime number+-- https://nulldereference.wordpress.com/2012/02/04/generating-prime-numbers-with-haskell/+divisors :: Integer -> [Integer]+divisors 1 = [1]+divisors x = 1 : [y | y <- [2 .. (x `div` 2)], x `mod` y == 0] ++ [x]++isPrime :: Integer -> Bool+isPrime x = divisors x == [1, x]++primeNums :: [Integer]+primeNums = [x | x <- [2 ..], isPrime x]++$(mkLoc "alice")+$(mkLoc "bob")++type Participants = ["alice", "bob"]++diffieHellman ::+  (MonadIO m) =>+  Choreo Participants (CLI m) ()+diffieHellman = do+  -- wait for alice to initiate the process+  _ <- alice `_locally` getstr "enter to start key exchange..."+  bob `_locally_` putNote "waiting for alice to initiate key exchange"++  -- alice picks p and g and sends them to bob+  pa <-+    alice `_locally` do+      x <- randomRIO (200, 1000 :: Int)+      return $ primeNums !! x+  pb <- (alice, pa) ~> bob @@ nobody+  ga <- alice `locally` \un -> do randomRIO (10, un alice pa)+  gb <- (alice, ga) ~> bob @@ nobody++  -- alice and bob select secrets+  a <- alice `_locally` randomRIO (200, 1000 :: Integer)+  b <- bob `_locally` randomRIO (200, 1000 :: Integer)++  -- alice and bob computes numbers that they exchange+  a' <- alice `locally` \un -> do return $ un alice ga ^ un alice a `mod` un alice pa+  b' <- bob `locally` \un -> do return $ un bob gb ^ un bob b `mod` un bob pb++  -- exchange numbers+  a'' <- (alice, a') ~> bob @@ nobody+  b'' <- (bob, b') ~> alice @@ nobody++  -- compute shared key+  alice `locally_` \un ->+    let s = un alice b'' ^ un alice a `mod` un alice pa+     in putOutput "alice's shared key:" s+  bob `locally_` \un ->+    let s = un bob a'' ^ un bob b `mod` un bob pb+     in putOutput "bob's shared key:" s++main :: IO ()+main = do+  [loc] <- getArgs+  _ <- case loc of+    "alice" -> runCLIIO $ runChoreography config diffieHellman "alice"+    "bob" -> runCLIIO $ runChoreography config diffieHellman "bob"+    _ -> error "unknown party"+  return ()+  where+    config =+      mkHttpConfig+        [ ("alice", ("localhost", 5000)),+          ("bob", ("localhost", 5001))+        ]
+ examples/GMWReal.hs view
@@ -0,0 +1,202 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++module GMWReal where++import CLI+import Choreography+import Choreography.Network.Http+import Control.Monad (void)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Crypto.Random.Types qualified as CRT+import Data (TestArgs, reference)+import Data.Foldable (toList)+import Data.Kind (Type)+import Data.Maybe (fromJust)+import GHC.TypeLits (KnownSymbol)+import ObliviousTransfer+import System.Environment+import System.Random+import Test.QuickCheck (Arbitrary, arbitrary, chooseInt, elements, getSize, oneof, resize)++$(mkLoc "trusted3rdParty")+$(mkLoc "p1")+$(mkLoc "p2")+$(mkLoc "p3")+$(mkLoc "p4")++xor :: (Foldable f) => f Bool -> Bool+xor = foldr1 (/=)++data Circuit :: [LocTy] -> Type where+  InputWire :: (KnownSymbol p) => Member p ps -> Circuit ps+  LitWire :: Bool -> Circuit ps+  AndGate :: Circuit ps -> Circuit ps -> Circuit ps+  XorGate :: Circuit ps -> Circuit ps -> Circuit ps++instance Show (Circuit ps) where+  show (InputWire p) = "InputWire<" ++ toLocTm p ++ ">"+  show (LitWire b) = "LitWire " ++ show b+  show (AndGate left right) = "(" ++ show left ++ ") AND (" ++ show right ++ ")"+  show (XorGate left right) = "(" ++ show left ++ ") XOR (" ++ show right ++ ")"++instance Arbitrary (Circuit '["p1", "p2", "p3", "p4"]) where+  arbitrary = do+    size <- getSize+    if 1 >= size+      then oneof $ (LitWire <$> arbitrary) : (pure <$> [InputWire p1, InputWire p2, InputWire p3, InputWire p4])+      else do+        left <- chooseInt (1, size)+        a <- resize left arbitrary+        b <- resize (1 `max` (size - left)) arbitrary+        op <- elements [AndGate, XorGate]+        return $ a `op` b++data Args = Args+  { circuit :: Circuit '["p1", "p2", "p3", "p4"],+    p1in :: Bool, -- These should be lists, but consuming them would be a chore...+    p2in :: Bool,+    p3in :: Bool,+    p4in :: Bool+  }+  deriving (Show)++instance Arbitrary Args where+  arbitrary = Args <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary++instance TestArgs Args (Bool, Bool, Bool, Bool) where+  reference Args {circuit, p1in, p2in, p3in, p4in} = (answer, answer, answer, answer)+    where+      recurse c = case c of+        InputWire p -> fromJust $ toLocTm p `lookup` inputs+        LitWire b -> b+        AndGate left right -> recurse left && recurse right+        XorGate left right -> recurse left /= recurse right+      inputs = ["p1", "p2", "p3", "p4"] `zip` [p1in, p2in, p3in, p4in]+      answer = recurse circuit++genShares :: forall ps p m. (MonadIO m, KnownSymbols ps) => Member p ps -> Bool -> m (Quire ps Bool)+genShares p x = quorum1 p gs'+  where+    gs' :: forall q qs. (KnownSymbol q, KnownSymbols qs) => m (Quire (q ': qs) Bool)+    gs' = do+      freeShares <- sequence $ pure $ liftIO randomIO -- generate n-1 random shares+      return $ qCons (xor (qCons @q x freeShares)) freeShares++secretShare ::+  forall parties p m.+  (KnownSymbols parties, KnownSymbol p, MonadIO m) =>+  Member p parties ->+  Located '[p] Bool ->+  Choreo parties m (Faceted parties '[] Bool)+secretShare p value = do+  shares <- locally p \un -> genShares p (un singleton value)+  PIndexed fs <- scatter p (allOf @parties) shares+  return $ PIndexed $ Facet . othersForget (First @@ nobody) . getFacet . fs++reveal :: forall ps m. (KnownSymbols ps) => Faceted ps '[] Bool -> Choreo ps m Bool+reveal shares = xor <$> (gather ps ps shares >>= naked ps)+  where+    ps = allOf @ps++-- use OT to do multiplication+fAnd ::+  forall parties m.+  (KnownSymbols parties, MonadIO m, CRT.MonadRandom m) =>+  Faceted parties '[] Bool ->+  Faceted parties '[] Bool ->+  Choreo parties (CLI m) (Faceted parties '[] Bool)+fAnd uShares vShares = do+  let genBools = sequence $ pure randomIO+  a_j_s :: Faceted parties '[] (Quire parties Bool) <- _parallel (allOf @parties) genBools+  bs :: Faceted parties '[] Bool <- fanOut \p_j -> do+    let p_j_name = toLocTm p_j+    b_i_s <- fanIn (p_j @@ nobody) \p_i ->+      if toLocTm p_i == p_j_name+        then _locally p_j $ pure False+        else do+          -- bb is the truth table+          bb <- locally p_i \un ->+            let a_ij = getLeaf (viewFacet un p_i a_j_s) p_j+                u_i = viewFacet un p_i uShares+             in pure (xor [u_i, a_ij], a_ij)+          -- localize p_j vSHares is party j's share of v+          enclaveTo (p_i @@ p_j @@ nobody) (listedSecond @@ nobody) (ot2 bb $ localize p_j vShares)+    locally p_j \un -> pure $ xor $ un singleton b_i_s+  parallel (allOf @parties) \p_i un ->+    let computeShare u v a_js b = xor $ [u && v, b] ++ toList (qModify p_i (const False) a_js)+     in pure $+          computeShare+            (viewFacet un p_i uShares)+            (viewFacet un p_i vShares)+            (viewFacet un p_i a_j_s)+            (viewFacet un p_i bs)++gmw ::+  forall parties m.+  (KnownSymbols parties, MonadIO m, CRT.MonadRandom m) =>+  Circuit parties ->+  Choreo parties (CLI m) (Faceted parties '[] Bool)+gmw circuit = case circuit of+  InputWire p -> do+    -- process a secret input value from party p+    value :: Located '[p] Bool <- _locally p $ getInput "Enter a secret input value:"+    secretShare p value+  LitWire b -> do+    -- process a publicly-known literal value+    let chooseShare :: forall p. (KnownSymbol p) => Member p parties -> Choreo parties (CLI m) (Located '[p] Bool)+        chooseShare p = congruently (p @@ nobody) $ \_ -> case p of+          First -> b+          Later _ -> False+    fanOut chooseShare+  AndGate l r -> do+    -- process an AND gate+    lResult <- gmw l+    rResult <- gmw r+    fAnd lResult rResult+  XorGate l r -> do+    -- process an XOR gate+    lResult <- gmw l+    rResult <- gmw r+    parallel (allOf @parties) \p un -> pure $ xor [viewFacet un p lResult, viewFacet un p rResult]++mpc ::+  forall parties m.+  (KnownSymbols parties, MonadIO m, CRT.MonadRandom m) =>+  Circuit parties ->+  Choreo parties (CLI m) ()+mpc circuit = do+  outputWire <- gmw circuit+  result <- reveal outputWire+  void $ _parallel (allOf @parties) $ putOutput "The resulting bit:" result++mpcmany ::+  (KnownSymbols parties, MonadIO m, CRT.MonadRandom m) =>+  Circuit parties ->+  Choreo parties (CLI m) ()+mpcmany circuit = do+  mpc circuit++type Clients = '["p1", "p2"] -- , "p3", "p4"]++main :: IO ()+main = do+  let circuit :: Circuit Clients = AndGate (LitWire True) (LitWire True)+  [loc] <- getArgs+  delivery <- case loc of+    "p1" -> runCLIIO $ runChoreography cfg (mpcmany @Clients circuit) "p1"+    "p2" -> runCLIIO $ runChoreography cfg (mpcmany @Clients circuit) "p2"+    --    "p3" -> runCLIIO $ runChoreography cfg (mpcmany @Clients circuit) "p3"+    --    "p4" -> runCLIIO $ runChoreography cfg (mpcmany @Clients circuit) "p4"+    _ -> error "unknown party"+  print delivery+  where+    cfg =+      mkHttpConfig+        [ ("p1", ("localhost", 4242)),+          ("p2", ("localhost", 4343))+          --                       , ("p3", ("localhost", 4344))+          --                       , ("p4", ("localhost", 4345))+        ]
+ examples/KVS1Simple.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}++{-+# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++# Example: Simple client-server key-value store++This is the first version of the 4-stage key-value store tutorial and implements a simple client-server key-value store. The client can `PUT` a key-value pair to the server and `GET` a value for a given key.++## Execution++```bash+# start server+cabal run kvs1 server+# on a different terminal for client+cabal run kvs1 client+GET hello+> Nothing+PUT hello world+> Just "world"+GET hello+> Just "world"+```+-}++module KVS1Simple where++import Choreography+import Choreography.Network.Http+import Data.IORef+import Data.Map (Map)+import Data.Map qualified as Map+import System.Environment++$(mkLoc "client")+$(mkLoc "server")++type Participants = ["client", "server"]++type State = Map String String++data Request = Put String String | Get String deriving (Show, Read)++type Response = Maybe String++-- | `readRequest` reads a request from the terminal.+readRequest :: IO Request+readRequest = do+  putStrLn "Command?"+  line <- getLine+  case parseRequest line of+    Just t -> return t+    Nothing -> putStrLn "Invalid command" >> readRequest+  where+    parseRequest :: String -> Maybe Request+    parseRequest s =+      let l = words s+       in case l of+            ["GET", k] -> Just (Get k)+            ["PUT", k, v] -> Just (Put k v)+            _ -> Nothing++-- | `handleRequest` handle a request and returns the new the state.+handleRequest :: Request -> IORef State -> IO Response+handleRequest request stateRef = case request of+  Put key value -> do+    modifyIORef stateRef (Map.insert key value)+    return (Just value)+  Get key -> do+    state <- readIORef stateRef+    return (Map.lookup key state)++-- | `kvs` is a choreography that processes a single request located at the client and returns the response.+kvs ::+  Located '["client"] Request ->+  Located '["server"] (IORef State) ->+  Choreo Participants IO (Located '["client"] Response)+kvs request stateRef = do+  -- send the request to the server+  request' <- (client, request) ~> server @@ nobody+  -- the server handles the response and creates a response+  response <-+    server `locally` \un ->+      handleRequest (un server request') (un server stateRef)+  -- send the response back to the client+  (server, response) ~> client @@ nobody++-- | `mainChoreo` is a choreography that serves as the entry point of the program.+-- It initializes the state and loops forever.+-- HIII :> (*>_*)+mainChoreo :: Choreo Participants IO ()+mainChoreo = do+  stateRef <- server `_locally` newIORef (Map.empty :: State)+  loop stateRef+  where+    loop :: Located '["server"] (IORef State) -> Choreo Participants IO ()+    loop stateRef = do+      request <- client `_locally` readRequest+      response <- kvs request stateRef+      client `locally_` \un -> do putStrLn ("> " ++ show (un client response))+      loop stateRef++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "client" -> runChoreography config mainChoreo "client"+    "server" -> runChoreography config mainChoreo "server"+    _ -> error "unknown party"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("server", ("localhost", 4000))+        ]
+ examples/KVS2PrimaryBackup.hs view
@@ -0,0 +1,139 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++# Example: Primary-backup key-value store++This is the second version of the 4-stage key-value store tutorial. This builds on the first version and adds a backup location to improve durability.++```bash+# 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"+```+-}++module KVS2PrimaryBackup where++import Choreography+import Choreography.Network.Http+import Data.IORef+import Data.Map (Map)+import Data.Map qualified as Map+import System.Environment++$(mkLoc "client")+$(mkLoc "primary")+$(mkLoc "backup")++type Participants = ["client", "primary", "backup"]++type State = Map String String++data Request = Put String String | Get String deriving (Show, Read)++type Response = Maybe String++-- | `readRequest` reads a request from the terminal.+readRequest :: IO Request+readRequest = do+  putStrLn "Command?"+  line <- getLine+  case parseRequest line of+    Just t -> return t+    Nothing -> putStrLn "Invalid command" >> readRequest+  where+    parseRequest :: String -> Maybe Request+    parseRequest s =+      let l = words s+       in case l of+            ["GET", k] -> Just (Get k)+            ["PUT", k, v] -> Just (Put k v)+            _ -> Nothing++-- | `handleRequest` handle a request and returns the new the state.+handleRequest :: Request -> IORef State -> IO Response+handleRequest request stateRef = case request of+  Put key value -> do+    modifyIORef stateRef (Map.insert key value)+    return (Just value)+  Get key -> do+    state <- readIORef stateRef+    return (Map.lookup key state)++-- | `kvs` is a choreography that processes a single request located at the client and returns the response.+-- If the request is a `PUT`, it will forward the request to the backup node.+kvs ::+  Located '["client"] Request ->+  (Located '["primary"] (IORef State), Located '["backup"] (IORef State)) ->+  Choreo Participants IO (Located '["client"] Response)+kvs request (primaryStateRef, backupStateRef) = do+  -- send request to the primary node+  request' <- (client, request) ~> primary @@ nobody++  -- branch on the request+  broadcast (primary, request') >>= \case+    -- if the request is a `PUT`, forward the request to the backup node+    Put _ _ -> do+      request'' <- (primary, request') ~> backup @@ nobody+      ack <-+        backup `locally` \un -> do+          handleRequest (un backup request'') (un backup backupStateRef)+      _ <- (backup, ack) ~> primary @@ nobody+      return ()+    _ -> do+      return ()++  -- process request on the primary node+  response <-+    primary `locally` \un ->+      handleRequest (un primary request') (un primary primaryStateRef)++  -- send response to client+  (primary, response) ~> client @@ nobody++-- | `mainChoreo` is a choreography that serves as the entry point of the program.+-- It initializes the state and loops forever.+mainChoreo :: Choreo Participants IO ()+mainChoreo = do+  primaryStateRef <- primary `_locally` newIORef (Map.empty :: State)+  backupStateRef <- backup `_locally` newIORef (Map.empty :: State)+  loop (primaryStateRef, backupStateRef)+  where+    loop :: (Located '["primary"] (IORef State), Located '["backup"] (IORef State)) -> Choreo Participants IO ()+    loop stateRefs = do+      request <- client `_locally` readRequest+      response <- kvs request stateRefs+      client `locally_` \un -> do putStrLn ("> " ++ show (un client response))+      loop stateRefs++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "client" -> runChoreography config mainChoreo "client"+    "primary" -> runChoreography config mainChoreo "primary"+    "backup" -> runChoreography config mainChoreo "backup"+    _ -> error "unknown party"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("primary", ("localhost", 4000)),+          ("backup", ("localhost", 5000))+        ]
+ examples/KVS3HigherOrder.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++# Example: Key-value store with higher-order choreography++## Execution++By default, `primaryBackupReplicationStrategy` will be used. Change `mainChoreo` to `nullReplicationChoreo` to use `nullReplicationStrategy`.++```bash+# 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"+```+-}++module KVS3HigherOrder where++import Choreography+import Choreography.Network.Http+import Data.IORef+import Data.Map (Map)+import Data.Map qualified as Map+import System.Environment++$(mkLoc "client")+$(mkLoc "primary")+$(mkLoc "backup")++type Participants = ["client", "primary", "backup"]++type State = Map String String++data Request = Put String String | Get String deriving (Show, Read)++type Response = Maybe String++-- | `readRequest` reads a request from the terminal.+readRequest :: IO Request+readRequest = do+  putStrLn "Command?"+  line <- getLine+  case parseRequest line of+    Just t -> return t+    Nothing -> putStrLn "Invalid command" >> readRequest+  where+    parseRequest :: String -> Maybe Request+    parseRequest s =+      let l = words s+       in case l of+            ["GET", k] -> Just (Get k)+            ["PUT", k, v] -> Just (Put k v)+            _ -> Nothing++-- | `handleRequest` handle a request and returns the new the state.+handleRequest :: Request -> IORef State -> IO Response+handleRequest request stateRef = case request of+  Put key value -> do+    modifyIORef stateRef (Map.insert key value)+    return (Just value)+  Get key -> do+    state <- readIORef stateRef+    return (Map.lookup key state)++-- | ReplicationStrategy specifies how a request should be handled on possibly replicated servers+-- `a` is a type that represent states across locations+type ReplicationStrategy a =+  Located '["primary"] Request -> a -> Choreo Participants IO (Located '["primary"] Response)++-- | `nullReplicationStrategy` is a replication strategy that does not replicate the state.+nullReplicationStrategy :: ReplicationStrategy (Located '["primary"] (IORef State))+nullReplicationStrategy request stateRef = do+  primary `locally` \un ->+    handleRequest (un primary request) (un primary stateRef)++-- | `primaryBackupReplicationStrategy` is a replication strategy that replicates the state to a backup server.+primaryBackupReplicationStrategy ::+  ReplicationStrategy (Located '["primary"] (IORef State), Located '["backup"] (IORef State))+primaryBackupReplicationStrategy request (primaryStateRef, backupStateRef) = do+  -- relay request to backup if it is mutating (= PUT)+  broadcast (primary, request) >>= \case+    Put _ _ -> do+      request' <- (primary, request) ~> backup @@ nobody+      _ <-+        ( backup,+          \un ->+            handleRequest (un backup request') (un backup backupStateRef)+          )+          ~~> primary+          @@ nobody+      return ()+    _ -> do+      return ()++  -- process request on primary+  primary `locally` \un ->+    handleRequest (un primary request) (un primary primaryStateRef)++-- | `kvs` is a choreography that processes a single request at the client and returns the response.+-- It uses the provided replication strategy to handle the request.+kvs ::+  forall a.+  Located '["client"] Request ->+  a ->+  ReplicationStrategy a ->+  Choreo Participants IO (Located '["client"] Response)+kvs request stateRefs replicationStrategy = do+  request' <- (client, request) ~> primary @@ nobody++  -- call the provided replication strategy+  response <- replicationStrategy request' stateRefs++  -- send response to client+  (primary, response) ~> client @@ nobody++-- | `nullReplicationChoreo` is a choreography that uses `nullReplicationStrategy`.+nullReplicationChoreo :: Choreo Participants IO ()+nullReplicationChoreo = do+  stateRef <- primary `_locally` newIORef (Map.empty :: State)+  loop stateRef+  where+    loop :: Located '["primary"] (IORef State) -> Choreo Participants IO ()+    loop stateRef = do+      request <- client `_locally` readRequest+      response <- kvs request stateRef nullReplicationStrategy+      client `locally_` \un -> do print (un client response)+      loop stateRef++-- | `primaryBackupChoreo` is a choreography that uses `primaryBackupReplicationStrategy`.+primaryBackupChoreo :: Choreo Participants IO ()+primaryBackupChoreo = do+  primaryStateRef <- primary `_locally` newIORef (Map.empty :: State)+  backupStateRef <- backup `_locally` newIORef (Map.empty :: State)+  loop (primaryStateRef, backupStateRef)+  where+    loop :: (Located '["primary"] (IORef State), Located '["backup"] (IORef State)) -> Choreo Participants IO ()+    loop stateRefs = do+      request <- client `_locally` readRequest+      response <- kvs request stateRefs primaryBackupReplicationStrategy+      client `locally_` \un -> do putStrLn ("> " ++ show (un client response))+      loop stateRefs++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "client" -> runChoreography config mainChoreo "client"+    "primary" -> runChoreography config mainChoreo "primary"+    "backup" -> runChoreography config mainChoreo "backup"+    _ -> error "unknown party"+  return ()+  where+    mainChoreo = primaryBackupChoreo -- or `nullReplicationChoreo`+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("primary", ("localhost", 4000)),+          ("backup", ("localhost", 5000))+        ]
+ examples/KVS4LocPoly.hs view
@@ -0,0 +1,217 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++# Example: Key-value store with location polymorphism++This is the final version of the 4-stage key-value store tutorial where we define the location-polymorphic choreography `doBackup`. We use it to define `doubleBackupReplicationStrategy`, which replicates data to two backup locations (`backup1` and `backup2`).++## Execution++```bash+# 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"+```+-}++module KVS4LocPoly where++import Choreography+import Choreography.Network.Http+import Data.IORef+import Data.Map (Map)+import Data.Map qualified as Map+import GHC.TypeLits (KnownSymbol)+import System.Environment++$(mkLoc "client")+$(mkLoc "primary")+$(mkLoc "backup1")+$(mkLoc "backup2")++type Participants = ["client", "primary", "backup1", "backup2"]++type State = Map String String++data Request = Put String String | Get String deriving (Show, Read)++type Response = Maybe String++-- | `readRequest` reads a request from the terminal.+readRequest :: IO Request+readRequest = do+  putStrLn "Command?"+  line <- getLine+  case parseRequest line of+    Just t -> return t+    Nothing -> putStrLn "Invalid command" >> readRequest+  where+    parseRequest :: String -> Maybe Request+    parseRequest s =+      let l = words s+       in case l of+            ["GET", k] -> Just (Get k)+            ["PUT", k, v] -> Just (Put k v)+            _ -> Nothing++-- | `handleRequest` handle a request and returns the new the state.+handleRequest :: Request -> IORef State -> IO Response+handleRequest request stateRef = case request of+  Put key value -> do+    modifyIORef stateRef (Map.insert key value)+    return (Just value)+  Get key -> do+    state <- readIORef stateRef+    return (Map.lookup key state)++-- | ReplicationStrategy specifies how a request should be handled on possibly replicated servers+-- `a` is a type that represent states across locations+type ReplicationStrategy a = Located '["primary"] Request -> a -> Choreo Participants IO (Located '["primary"] Response)++-- | `nullReplicationStrategy` is a replication strategy that does not replicate the state.+nullReplicationStrategy :: ReplicationStrategy (Located '["primary"] (IORef State))+nullReplicationStrategy request stateRef = do+  primary `locally` \un -> case un primary request of+    Put key value -> do+      modifyIORef (un primary stateRef) (Map.insert key value)+      return (Just value)+    Get key -> do+      state <- readIORef (un primary stateRef)+      return (Map.lookup key state)++-- | `doBackup` relays a mutating request to a backup location.+doBackup ::+  ( KnownSymbol a,+    KnownSymbol b,+    KnownSymbols ps+  ) =>+  Member a ps ->+  Member b ps ->+  Located '[a] Request ->+  Located '[b] (IORef State) ->+  Choreo ps IO ()+doBackup locA locB request stateRef = do+  broadcast (locA, request) >>= \case+    Put _ _ -> do+      request' <- (locA, request) ~> locB @@ nobody+      _ <-+        (locB, \un -> handleRequest (un singleton request') (un singleton stateRef))+          ~~> locA+          @@ nobody+      return ()+    _ -> do+      return ()++-- | `primaryBackupReplicationStrategy` is a replication strategy that replicates the state to a backup server.+primaryBackupReplicationStrategy :: ReplicationStrategy (Located '["primary"] (IORef State), Located '["backup1"] (IORef State))+primaryBackupReplicationStrategy request (primaryStateRef, backupStateRef) = do+  -- relay request to backup if it is mutating (= PUT)+  doBackup primary backup1 request backupStateRef++  -- process request on primary+  primary `locally` \un -> handleRequest (un primary request) (un primary primaryStateRef)++-- | `doubleBackupReplicationStrategy` is a replication strategy that replicates the state to two backup servers.+doubleBackupReplicationStrategy ::+  ReplicationStrategy+    (Located '["primary"] (IORef State), Located '["backup1"] (IORef State), Located '["backup2"] (IORef State))+doubleBackupReplicationStrategy+  request+  (primaryStateRef, backup1StateRef, backup2StateRef) = do+    -- relay to two backup locations+    doBackup primary backup1 request backup1StateRef+    doBackup primary backup2 request backup2StateRef++    -- process request on primary+    primary `locally` \un ->+      handleRequest (un primary request) (un primary primaryStateRef)++-- | `kvs` is a choreography that processes a single request at the client and returns the response.+-- It uses the provided replication strategy to handle the request.+kvs :: Located '["client"] Request -> a -> ReplicationStrategy a -> Choreo Participants IO (Located '["client"] Response)+kvs request stateRefs replicationStrategy = do+  request' <- (client, request) ~> primary @@ nobody++  -- call the provided replication strategy+  response <- replicationStrategy request' stateRefs++  -- send response to client+  (primary, response) ~> client @@ nobody++-- | `nullReplicationChoreo` is a choreography that uses `nullReplicationStrategy`.+nullReplicationChoreo :: Choreo Participants IO ()+nullReplicationChoreo = do+  stateRef <- primary `_locally` newIORef (Map.empty :: State)+  loop stateRef+  where+    loop :: Located '["primary"] (IORef State) -> Choreo Participants IO ()+    loop stateRef = do+      request <- client `_locally` readRequest+      response <- kvs request stateRef nullReplicationStrategy+      client `locally_` \un -> do print (un client response)+      loop stateRef++-- | `primaryBackupChoreo` is a choreography that uses `primaryBackupReplicationStrategy`.+primaryBackupChoreo :: Choreo Participants IO ()+primaryBackupChoreo = do+  primaryStateRef <- primary `_locally` newIORef (Map.empty :: State)+  backupStateRef <- backup1 `_locally` newIORef (Map.empty :: State)+  loop (primaryStateRef, backupStateRef)+  where+    loop :: (Located '["primary"] (IORef State), Located '["backup1"] (IORef State)) -> Choreo Participants IO ()+    loop stateRefs = do+      request <- client `_locally` readRequest+      response <- kvs request stateRefs primaryBackupReplicationStrategy+      client `locally_` \un -> do print (un client response)+      loop stateRefs++-- | `doubleBackupChoreo` is a choreography that uses `doubleBackupReplicationStrategy`.+doubleBackupChoreo :: Choreo Participants IO ()+doubleBackupChoreo = do+  primaryStateRef <- primary `_locally` newIORef (Map.empty :: State)+  backup1StateRef <- backup1 `_locally` newIORef (Map.empty :: State)+  backup2StateRef <- backup2 `_locally` newIORef (Map.empty :: State)+  loop (primaryStateRef, backup1StateRef, backup2StateRef)+  where+    loop :: (Located '["primary"] (IORef State), Located '["backup1"] (IORef State), Located '["backup2"] (IORef State)) -> Choreo Participants IO ()+    loop stateRefs = do+      request <- client `_locally` readRequest+      response <- kvs request stateRefs doubleBackupReplicationStrategy+      client `locally_` \un -> do putStrLn ("> " ++ show (un client response))+      loop stateRefs++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "client" -> runChoreography config primaryBackupChoreo "client"+    "primary" -> runChoreography config primaryBackupChoreo "primary"+    "backup1" -> runChoreography config primaryBackupChoreo "backup1"+    "backup2" -> runChoreography config primaryBackupChoreo "backup2"+    _ -> error "unknown party"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("primary", ("localhost", 4000)),+          ("backup1", ("localhost", 5000)),+          ("backup2", ("localhost", 6000))+        ]
+ examples/KVS5Fig17.hs view
@@ -0,0 +1,112 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++{-+This is an implementation of the choreogrpahy shown in fig17 of We Know I Know You Know.+-}++module KVS5Fig17 where++import CLI+import Choreography+import Choreography.Network.Http+import Data (TestArgs, reference)+import Data.List (sort)+import Data.Maybe (fromMaybe)+import System.Environment+import Test.QuickCheck (Arbitrary, arbitrary, elements)++$(mkLoc "client")+$(mkLoc "primary")+$(mkLoc "backup")++type Servers = ["primary", "backup"]++type Participants = "client" ': Servers++servers :: Subset Servers Participants+servers = primary @@ backup @@ nobody++data Request = Put String String | Get String deriving (Eq, Show, Read)++instance Arbitrary Request where+  arbitrary =+    ( \case+        Nothing -> Get+        Just s -> Put s+    )+      <$> arbitrary+      <*> arbitrary++type Response = String++data Args = Args+  { request :: Request,+    handler :: String+  }+  deriving (Eq, Show, Read)++instance TestArgs Args Response where+  reference Args {request, handler} =+    let f = fromMaybe defaultHandler $ handler `lookup` handlers+     in handleRequest f request++instance Arbitrary Args where+  arbitrary =+    Args+      <$> arbitrary+      <*> elements (fst <$> handlers)++handlers :: [(String, String -> String)]+handlers =+  [ ("reverse", reverse),+    ("alphabetize", sort)+  ]++defaultHandler :: String -> String+defaultHandler = const "No Handler"++-- | `handleRequest` handle a request. Since we don't have a way of locking paralell state, this is a mock.+handleRequest :: (String -> Response) -> Request -> Response+handleRequest handler request = case request of+  Put key value -> show key ++ " saved as " ++ show value ++ "."+  Get key -> handler key++setup :: Choreo Servers (CLI m) (Located Servers (Request -> Response))+setup = do+  handlerName <-+    (primary, getstr "How should we mock `Get` Requests? (reverse or alphabetize)")+      -~> primary+      @@ backup+      @@ nobody+  primary @@ backup @@ nobody `congruently` \un -> handleRequest (fromMaybe defaultHandler $ un refl handlerName `lookup` handlers)++-- | `kvs` is a choreography that processes a single request located at the client and returns the response.+-- If the request is a `PUT`, it will forward the request to the backup node.+kvs :: Choreo Participants (CLI m) ()+kvs = do+  handler <- enclaveToAll servers setup+  request <- (client, getInput "Enter the `read`able Request:") -~> primary @@ backup @@ nobody+  response <- primary @@ backup @@ nobody `congruently` \un -> un refl handler $ un refl request+  response' <- (primary, response) ~> client @@ nobody+  client `locally_` \un -> putOutput "Recieved:" $ un client response'++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "client" -> runCLIIO $ runChoreography config kvs "client"+    "primary" -> runCLIIO $ runChoreography config kvs "primary"+    "backup" -> runCLIIO $ runChoreography config kvs "backup"+    _ -> error "unknown party"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("primary", ("localhost", 4000)),+          ("backup", ("localhost", 5000))+        ]
+ examples/KVS6SizePoly.hs view
@@ -0,0 +1,198 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-+-}++module KVS6SizePoly where++import CLI+import Choreography+import Control.Monad.IO.Class (MonadIO, liftIO)+import Data.Foldable (toList)+import Data.IORef (IORef)+import Data.IORef qualified as IORef+import Data.List (nub)+import Data.Map (Map)+import Data.Map qualified as Map+import GHC.TypeLits (KnownSymbol)+import Test.QuickCheck (Arbitrary, arbitrary, frequency, listOf)+import Text.Read (readMaybe)++readIORef :: (MonadIO m) => IORef a -> m a+readIORef = liftIO <$> IORef.readIORef++modifyIORef :: (MonadIO m) => IORef a -> (a -> a) -> m a+modifyIORef ref f = do+  a <- readIORef ref+  liftIO $ IORef.modifyIORef ref f+  return a++newIORef :: (MonadIO m) => a -> m (IORef a)+newIORef = liftIO <$> IORef.newIORef++-- $(mkLoc "client")++-- $(mkLoc "primary")++-- $(mkLoc "backup1")++-- $(mkLoc "backup2")+-- type Participants = ["client", "primary", "backup1", "backup2"]++kvs :: (KnownSymbol client) => ReplicationStrategy ps (CLI m) -> Member client ps -> Choreo ps (CLI m) ()+kvs ReplicationStrategy {setup, primary, handle} client = do+  rigging <- setup+  let go = do+        request <- (client, readRequest) -~> primary @@ nobody+        response <- handle rigging singleton request+        case response of+          Stopped -> return ()+          _ -> do+            client `_locally_` putOutput "Recieved:" response+            go+  go++naryReplicationStrategy ::+  (KnownSymbol primary, KnownSymbols backups, KnownSymbols ps, MonadIO m) =>+  Member primary ps ->+  Subset backups ps ->+  ReplicationStrategy ps m+naryReplicationStrategy primary backups =+  ReplicationStrategy+    { primary,+      setup = servers `_parallel` newIORef (Map.empty :: State),+      handle = \stateRef pHas request -> do+        request' <- (primary, (pHas, request)) ~> servers+        localResponse <-+          servers `parallel` \server un ->+            handleRequest (viewFacet un server stateRef) (un server request')+        responses <- gather servers (primary @@ nobody) localResponse+        response <-+          (primary @@ nobody) `congruently` \un ->+            case nub (toList $ un refl responses) of+              [r] -> r+              rs -> Desynchronization rs+        broadcast (primary, response)+    }+  where+    servers = primary @@ backups++data ReplicationStrategy ps m+  = forall primary rigging.+  (KnownSymbol primary) =>+  ReplicationStrategy+  { primary :: Member primary ps,+    setup :: Choreo ps m rigging,+    handle ::+      forall starts.+      rigging ->+      Member primary starts ->+      Located starts Request ->+      Choreo ps m Response+  }++data Request = Put String String | Get String | Stop deriving (Eq, Ord, Read, Show)++data Response = Found String | NotFound | Stopped | Desynchronization [Response]+  deriving (Eq, Ord, Read, Show)++-- | PUT returns the old stored value; GET returns whatever was stored.+handleRequest :: (MonadIO m) => IORef State -> Request -> m Response+handleRequest stateRef (Put key value) = mlookup key <$> modifyIORef stateRef (Map.insert key value)+handleRequest stateRef (Get key) = mlookup key <$> readIORef stateRef+handleRequest _ Stop = return Stopped++mlookup :: String -> State -> Response+mlookup key = maybe NotFound Found . Map.lookup key++type State = Map String String++newtype Args = Args [Request] deriving (Eq, Ord, Read, Show)++instance Arbitrary Args where+  arbitrary = do+    reqs <- pgs+    return . Args $ reqs ++ [Stop]+    where+      pgs =+        listOf $+          frequency+            [ (1, Put <$> arbitrary <*> arbitrary),+              (1, Get <$> arbitrary)+            ]++readRequest :: CLI m Request+readRequest = do+  line <- getstr "Command?"+  case line of+    [] -> return Stop+    _ -> case readMaybe line of+      Just t -> return t+      Nothing -> putNote "Invalid command" >> readRequest++-- | `nullReplicationStrategy` is a replication strategy that does not replicate the state.+nullReplicationStrategy ::+  (KnownSymbol primary, KnownSymbols ps, MonadIO m) =>+  Member primary ps ->+  ReplicationStrategy ps m+nullReplicationStrategy primary =+  ReplicationStrategy+    { primary,+      setup = primary `_locally` newIORef (Map.empty :: State),+      handle = \stateRef pHas request ->+        ( (primary, \un -> handleRequest (un singleton stateRef) (un pHas request)) ~~> refl+        )+          >>= naked refl+    }++naryHumans ::+  (KnownSymbol primary, KnownSymbols backups, KnownSymbols ps, MonadIO m) =>+  Member primary ps ->+  Subset backups ps ->+  ReplicationStrategy ps (CLI m)+naryHumans primary backups =+  ReplicationStrategy+    { primary,+      setup = primary `_locally` newIORef (Map.empty :: State),+      handle = \stateRef pHas request -> do+        request' <- (primary, (pHas, request)) ~> backups+        backupResponse <- backups `parallel` \server un -> readResponse (un server request')+        localResponse <- primary `locally` \un -> handleRequest (un singleton stateRef) (un pHas request)+        responses <- gather backups (primary @@ nobody) backupResponse+        response <-+          (primary @@ nobody) `congruently` \un ->+            case nub $ un refl localResponse : toList (un refl responses) of+              [r] -> r+              rs -> Desynchronization rs+        ((primary, response) ~> refl) >>= naked refl+    }+  where+    readResponse :: Request -> CLI m Response+    readResponse r = do+      line <- getstr $ show r ++ ": "+      case line of+        [] -> return NotFound+        _ -> return $ Found line++{-main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "client" -> runChoreography config primaryBackupChoreo "client"+    "primary" -> runChoreography config primaryBackupChoreo "primary"+    "backup1" -> runChoreography config primaryBackupChoreo "backup1"+    "backup2" -> runChoreography config primaryBackupChoreo "backup2"+    _ -> error "unknown party"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("primary", ("localhost", 4000)),+          ("backup1", ("localhost", 5000)),+          ("backup2", ("localhost", 6000))+        ]++-}
+ examples/KVS7SimplePoly.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++module KVS7SimplePoly where++-- # This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++import Choreography+import Data.IORef (IORef, newIORef, readIORef)++type Response = Int++type Key = String++type State = String++errorResponse :: Response+errorResponse = -1++data Request+  = Get Key+  | Put Key Int+  deriving (Eq, Read, Show)++handleGet :: IORef State -> Key -> IO Response+handleGet s k = do+  readIORef s >>= putStrLn+  return $ length k++handlePut :: IORef State -> Key -> Int -> IO Response+handlePut s k v = do+  readIORef s >>= putStrLn+  return . fromEnum $ v /= length k++isOk :: Response -> Bool+isOk = (== 0)++handleRequest ::+  forall backups.+  (KnownSymbols backups) =>+  Located '["primary"] Request ->+  (Located '["primary"] (IORef State), Faceted backups '[] (IORef State)) ->+  Choreo ("primary" ': backups) IO (Located '["primary"] Response)+handleRequest request (primaryStateRef, backupsStateRefs) =+  broadcast (primary, request) >>= \case+    Put key value -> do+      oks <- parallel backups \backup un ->+        handlePut (viewFacet un backup backupsStateRefs) key value+      gathered <- gather backups (primary @@ nobody) oks+      locally primary \un ->+        if all isOk (un primary gathered)+          then handlePut (un primary primaryStateRef) key value+          else return errorResponse+    Get key -> locally primary \un -> handleGet (un primary primaryStateRef) key+  where+    primary :: forall ps. Member "primary" ("primary" ': ps)+    primary = listedFirst+    backups = consSuper refl++kvs ::+  forall backups.+  (KnownSymbols backups) =>+  Located '["client"] Request ->+  (Located '["primary"] (IORef State), Faceted backups '[] (IORef State)) ->+  Choreo ("client" ': "primary" ': backups) IO (Located '["client"] Response)+kvs request stateRefs = do+  request' <- (client, request) ~> primary @@ nobody+  response <- enclave (primary @@ backups) (handleRequest request' stateRefs)+  (primary, flatten (First @@ nobody) (First @@ nobody) response) ~> client @@ nobody+  where+    client :: forall ps. Member "client" ("client" ': ps)+    primary :: forall ps p. Member "primary" (p ': "primary" ': ps)+    client = listedFirst+    primary = listedSecond+    backups = consSuper $ consSuper refl++mainChoreo :: (KnownSymbols backups) => Choreo ("client" ': "primary" ': backups) IO ()+mainChoreo = do+  stateRef <- primary `_locally` newIORef "I'm Primary"+  bStRefs <- parallel backups \p _ -> newIORef ("I'm " ++ toLocTm p)+  loop (stateRef, bStRefs)+  where+    primary :: forall ps p. Member "primary" (p ': "primary" ': ps)+    primary = listedSecond+    client :: forall ps. Member "client" ("client" ': ps)+    client = listedFirst+    backups = consSuper $ consSuper refl+    loop state = do+      request <- _locally client $ read @Request <$> getLine+      response <- kvs request state+      client `locally_` \un -> do putStrLn ("> " ++ show (un client response))+      loop state++main :: IO ()+main = runChoreo (mainChoreo @'["A", "B", "C", "D", "E", "F"])
+ examples/Karatsuba.hs view
@@ -0,0 +1,129 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++# Example: Karatsuba Fast Multiplication++## Overview++This example implements the three-way concurrent implementation of the Karatsuba fast multiplication algorithm shown in [Object-Oriented Choreographic Programming](https://arxiv.org/abs/2005.09520).++## Execution++The executable takes two integers as arguments and returns their product. It uses the local backend and distribute the computation over threads.++```bash+cabal run karatsuba 100 200+20000+```++`Reference.h` contains a single-threaded reference implementation of the algorithm.+-}++module Karatsuba where++import Choreography+import Choreography.Network.Local+import Control.Concurrent.Async (mapConcurrently_)+import GHC.TypeLits (KnownSymbol)+import System.Environment++reference :: Integer -> Integer -> Integer+reference n1 n2 =+  if n1 < 10 || n2 < 10+    then n1 * n2+    else result+  where+    log10 :: Integer -> Double+    log10 = logBase 10 . fromIntegral+    m = max (log10 n1) (log10 n2) + 1+    m2 :: Integer = floor (m / 2)+    splitter = 10 ^ m2+    h1 = n1 `div` splitter+    l1 = n1 `mod` splitter+    h2 = n2 `div` splitter+    l2 = n2 `mod` splitter+    z0 = reference l1 l2+    z2 = reference h1 h2+    z1 = reference (l1 + h1) (l2 + h2) - z2 - z0+    result = z2 * splitter * splitter + z1 * splitter + z0++$(mkLoc "primary")+$(mkLoc "worker1")+$(mkLoc "worker2")++type Participants = ["primary", "worker1", "worker2"]++data KaratsubaNums = KaratsubaNums+  { splitter :: Integer,+    h1 :: Integer,+    h2 :: Integer,+    l1 :: Integer,+    l2 :: Integer+  }++karatsuba ::+  (KnownSymbol a, KnownSymbol b, KnownSymbol c) =>+  Member a Participants ->+  Member b Participants ->+  Member c Participants ->+  Located '[a] Integer ->+  Located '[a] Integer ->+  Choreo Participants IO (Located '[a] Integer)+karatsuba a b c n1 n2 = do+  done <- a `locally` \un -> return $ un singleton n1 < 10 || un singleton n2 < 10+  broadcast (a, done)+    >>= \case+      True -> do+        a `locally` \un -> return $ un singleton n1 * un singleton n2+      False -> do+        x <- a `locally` \un -> return $ f (un singleton n1) (un singleton n2)+        l1' <- (a, \un -> return $ l1 (un singleton x)) ~~> b @@ nobody+        l2' <- (a, \un -> return $ l2 (un singleton x)) ~~> b @@ nobody+        h1' <- (a, \un -> return $ h1 (un singleton x)) ~~> c @@ nobody+        h2' <- (a, \un -> return $ h2 (un singleton x)) ~~> c @@ nobody+        z0' <- karatsuba b c a l1' l2'+        z0 <- (b, z0') ~> a @@ nobody+        z2' <- karatsuba c a b h1' h2'+        z2 <- (c, z2') ~> a @@ nobody+        s1 <- a `locally` \un -> return $ l1 (un singleton x) + h1 (un singleton x)+        s2 <- a `locally` \un -> return $ l2 (un singleton x) + h2 (un singleton x)+        z1' <- karatsuba a b c s1 s2+        z1 <- a `locally` \un -> return $ un singleton z1' - un singleton z2 - un singleton z0+        a `locally` \un ->+          return+            let s = splitter (un singleton x)+             in (un singleton z2 * s * s) + (un singleton z1 * s) + un singleton z0+        where+          f n1' n2' = KaratsubaNums {splitter = splitter, h1 = h1, l1 = l1, h2 = h2, l2 = l2}+            where+              log10 :: Integer -> Double+              log10 = logBase 10 . fromIntegral+              m = max (log10 n1') (log10 n2') + 1+              m2 :: Integer = floor (m / 2)+              splitter = 10 ^ m2+              h1 = n1' `div` splitter+              l1 = n1' `mod` splitter+              h2 = n2' `div` splitter+              l2 = n2' `mod` splitter++mainChoreo :: Integer -> Integer -> Choreo Participants IO ()+mainChoreo n1' n2' = do+  n1 <- primary `_locally` pure n1'+  n2 <- primary `_locally` pure n2'+  result <- karatsuba primary worker1 worker2 n1 n2+  primary `locally_` \un -> do+    print (un primary result)++main :: IO ()+main = do+  [n1, n2] <- map read <$> getArgs+  config <- mkLocalConfig locations+  mapConcurrently_ (runChoreography config (mainChoreo n1 n2)) locations+  return ()+  where+    locations = ["primary", "worker1", "worker2"]
+ examples/Lottery.hs view
@@ -0,0 +1,156 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}++module Lottery where++import CLI+import Choreography+import Choreography.Network.Http+import Control.Exception (Exception, throwIO)+import Control.Monad (unless)+import Control.Monad.Cont (MonadIO, liftIO)+import Crypto.Hash (Digest)+import Crypto.Hash qualified as Crypto+import Data (TestArgs, reference)+import Data.Bifunctor (first)+import Data.Binary qualified as Binary+import Data.ByteString (toStrict)+import Data.FiniteField (primeField)+import Data.Foldable (toList)+import GHC.TypeLits (KnownSymbol)+import System.Environment (getArgs)+import System.Random (Random, random, randomIO, randomR, randomRIO)+import Test.QuickCheck (Arbitrary, arbitrary, arbitraryBoundedEnum)++-- | Arbitrary "large" prime+newtype Fp = Fp $(primeField 999983) -- AFAICT the hint warning needs a newer version of hlint to go away:+  deriving (Bounded, Enum, Eq, Ord, Num) -- https://github.com/ndmitchell/hlint/issues/1226++instance Read Fp where+  readsPrec _ s = [(Fp (read s), "")]++instance Show Fp where+  show (Fp x) = show x++instance Random Fp where+  random g = toEnum `first` randomR (fromEnum @Fp minBound, fromEnum @Fp maxBound) g+  randomR (l, h) g = toEnum `first` randomR (fromEnum l, fromEnum h) g++instance Arbitrary Fp where+  arbitrary = arbitraryBoundedEnum++data LotteryError = CommitmentCheckFailed deriving (Show)++instance Exception LotteryError++data Args = Args+  { secrets :: (Fp, Fp, Fp, Fp, Fp), -- we lock our test to the case of five clients and three servers+    randomIs :: (Int, Int, Int)+  }+  deriving (Eq, Show, Read)++instance TestArgs Args Fp where+  reference Args {secrets = (c1, c2, c3, c4, c5), randomIs = (s1, s2, s3)} =+    let i = (s1 + s2 + s3) `mod` 5+     in [c1, c2, c3, c4, c5] !! i++instance Arbitrary Args where+  arbitrary =+    Args+      <$> ((,,,,) <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary)+      <*> ((,,) <$> arbitrary <*> arbitrary <*> arbitrary)++-- | Federated Lottery example from DPrio https://www.semanticscholar.org/paper/DPrio%3A-Efficient-Differential-Privacy-with-High-for-Keeler-Komlo/ae1b2a4e5beaaa850183ad37e0880bb70ae34f4e+lottery ::+  forall clients servers analyst census m _serv1 _serv2 _servTail _client1 _client2 _clientTail.+  ( KnownSymbols clients,+    KnownSymbols servers,+    KnownSymbol analyst,+    MonadIO m,+    (_serv1 ': _serv2 ': _servTail) ~ servers, -- There must be at least be two servers+    (_client1 ': _client2 ': _clientTail) ~ clients -- There must be at least be two clients+  ) =>+  Subset clients census ->+  Subset servers census ->+  Member analyst census ->+  Choreo census (CLI m) ()+lottery clients servers analyst = do+  secret <- _parallel clients (getInput @Fp "secret:")+  clientShares <-+    clients `parallel` \client un ->+      ( case tySpine @servers of+          TyCons -> do+            -- I guess this explains to GHC that we have KnownSymbols _servTail? IDK+            freeShares <- liftIO $ sequence $ pure $ randomIO @Fp+            return $ (viewFacet un client secret - sum freeShares) `qCons` freeShares+      )+  serverShares <-+    fanOut+      ( \server ->+          -- Probably I've already got a nicer way to write this on hand; idk.+          fanIn+            (inSuper servers server @@ nobody)+            ( \client -> do+                serverShare <-+                  inSuper clients client `locally` \un ->+                    pure $ viewFacet un client clientShares `getLeaf` server+                (inSuper clients client, serverShare) ~> inSuper servers server @@ nobody+            )+      )+  -- 1) Each server selects a random number; τ is some multiple of the number of clients.+  ρ <- _parallel servers (getInput "A random number from 1 to τ:")+  -- Salt value+  ψ <- _parallel servers (randomRIO (2 ^ (18 :: Int), 2 ^ (20 :: Int)))+  -- 2) Each server computes and publishes the hash α = H(ρ, ψ) to serve as a commitment+  α <- parallel servers \server un -> pure $ hash (viewFacet un server ψ) (viewFacet un server ρ)+  α' <- gather servers servers α+  -- 3) Every server opens their commitments by publishing their ψ and ρ to each other+  ψ' <- gather servers servers ψ+  ρ' <- gather servers servers ρ+  -- 4) All servers verify each other's commitment by checking α = H(ρ, ψ)+  parallel_+    servers+    ( \server un ->+        unless+          (un server α' == (hash <$> un server ψ' <*> un server ρ'))+          (liftIO $ throwIO CommitmentCheckFailed)+    )+  -- 5) If all the checks are successful, then sum random values to get the random index.+  ω <- servers `congruently` (\un -> sum (un refl ρ') `mod` length (toLocs clients))+  chosenShares <- servers `parallel` (\server un -> pure $ toList (viewFacet un server serverShares) !! un server ω)+  -- Servers forward shares to an analyist.+  allShares <- gather servers (analyst @@ nobody) chosenShares+  analyst `locally_` \un -> putOutput "The answer is:" $ sum $ un singleton allShares+  where+    hash :: Int -> Int -> Digest Crypto.SHA256+    hash ρ ψ = Crypto.hash $ toStrict (Binary.encode ρ <> Binary.encode ψ)++main :: IO ()+main = do+  [loc] <- getArgs+  let clientProof :: Subset '["client1", "client2"] '["client1", "client2", "server1", "server2", "analyst"]+      clientProof = explicitSubset+      serverProof :: Subset '["server1", "server2"] '["client1", "client2", "server1", "server2", "analyst"]+      serverProof = explicitSubset+      analystProof :: Member "analyst" '["client1", "client2", "server1", "server2", "analyst"]+      analystProof = explicitMember+  _ <- case loc of+    "client1" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "client1"+    "client2" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "client2"+    "server1" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "server1"+    "server2" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "server2"+    "analyst" -> runCLIIO $ runChoreography config (lottery clientProof serverProof analystProof) "analyst"+    _ -> error "unknown party"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client1", ("localhost", 5000)),+          ("client2", ("localhost", 5001)),+          ("server1", ("localhost", 5002)),+          ("server2", ("localhost", 5003)),+          ("analyst", ("localhost", 5004))+        ]
+ examples/MPCFake.hs view
@@ -0,0 +1,145 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++module MPCFake where++import CLI+import Choreography+import Control.Monad.IO.Class (MonadIO, liftIO)+import Data (TestArgs, reference)+import Data.Kind (Type)+import Data.Maybe (fromJust)+import GHC.TypeLits (KnownSymbol)+import System.Random+import Test.QuickCheck (Arbitrary, arbitrary, chooseInt, elements, getSize, oneof, resize)++$(mkLoc "trusted3rdParty")+$(mkLoc "p1")+$(mkLoc "p2")+$(mkLoc "p3")+$(mkLoc "p4")++xor :: (Foldable f) => f Bool -> Bool+xor = foldr1 (/=)++data Circuit :: [LocTy] -> Type where+  InputWire :: (KnownSymbol p) => Member p ps -> Circuit ps+  LitWire :: Bool -> Circuit ps+  AndGate :: Circuit ps -> Circuit ps -> Circuit ps+  XorGate :: Circuit ps -> Circuit ps -> Circuit ps++instance Show (Circuit ps) where+  show (InputWire p) = "InputWire<" ++ toLocTm p ++ ">"+  show (LitWire b) = "LitWire " ++ show b+  show (AndGate left right) = "(" ++ show left ++ ") AND (" ++ show right ++ ")"+  show (XorGate left right) = "(" ++ show left ++ ") XOR (" ++ show right ++ ")"++instance Arbitrary (Circuit '["p1", "p2", "p3", "p4"]) where+  arbitrary = do+    size <- getSize+    if 1 >= size+      then oneof $ (LitWire <$> arbitrary) : (return <$> [InputWire p1, InputWire p2, InputWire p3, InputWire p4])+      else do+        left <- chooseInt (1, size)+        a <- resize left arbitrary+        b <- resize (1 `max` (size - left)) arbitrary+        op <- elements [AndGate, XorGate]+        return $ a `op` b++data Args = Args+  { circuit :: Circuit '["p1", "p2", "p3", "p4"],+    p1in :: Bool, -- These should be lists, but consuming them would be a chore...+    p2in :: Bool,+    p3in :: Bool,+    p4in :: Bool+  }+  deriving (Show)++instance Arbitrary Args where+  arbitrary = Args <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary++instance TestArgs Args (Bool, Bool, Bool, Bool) where+  reference Args {circuit, p1in, p2in, p3in, p4in} = (answer, answer, answer, answer)+    where+      recurse c = case c of+        InputWire p -> fromJust $ toLocTm p `lookup` inputs+        LitWire b -> b+        AndGate left right -> recurse left && recurse right+        XorGate left right -> recurse left /= recurse right+      inputs = ["p1", "p2", "p3", "p4"] `zip` [p1in, p2in, p3in, p4in]+      answer = recurse circuit++secretShare ::+  forall p parties owners ps m.+  (KnownSymbols parties, KnownSymbol p, MonadIO m) =>+  Subset parties ps ->+  Member p ps ->+  (Member p owners, Located owners Bool) ->+  Choreo ps m (Faceted parties '[] Bool)+secretShare parties p (ownership, value) = do+  shares <- p `locally` \un -> genShares (un ownership value)+  PIndexed fs <- scatter p parties shares+  return $ PIndexed $ Facet . othersForget (First @@ nobody) . getFacet . fs+  where+    genShares x = case tySpine @parties of+      TyCons -> gs'+      TyNil -> error "Can't secret-share to zero people."+      where+        gs' :: forall q qs. (KnownSymbol q, KnownSymbols qs) => m (Quire (q ': qs) Bool)+        gs' = do+          freeShares <- sequence $ pure $ liftIO randomIO -- generate n-1 random shares+          return $ xor (qCons @q x freeShares) `qCons` freeShares++reveal ::+  forall ps m.+  (KnownSymbols ps) =>+  Faceted ps '[] Bool ->+  Choreo ps m Bool+reveal shares = do+  let ps = allOf @ps+  allShares <- gather ps ps shares+  value <- ps `congruently` \un -> xor $ un ps allShares+  naked ps value++computeWire ::+  (KnownSymbols ps, KnownSymbols parties, KnownSymbol trustedAnd, MonadIO m) =>+  Member trustedAnd ps ->+  Subset parties ps ->+  Circuit parties ->+  Choreo ps (CLI m) (Faceted parties '[] Bool)+computeWire trustedAnd parties circuit = case circuit of+  InputWire p -> do+    value <- inSuper parties p `_locally` getInput "Enter a secret input value:"+    secretShare parties (inSuper parties p) (singleton, value)+  LitWire b -> do+    let shares = partyNames `zip` (b : repeat False)+    fanOut \p -> inSuper parties p `_locally` return (fromJust $ toLocTm p `lookup` shares)+  AndGate l r -> do+    lResult <- compute l+    rResult <- compute r+    inputShares <- fanIn (trustedAnd @@ nobody) \p -> do+      (inSuper parties p, \un -> return (viewFacet un p lResult, viewFacet un p rResult)) ~~> trustedAnd @@ nobody+    outputVal <-+      (trustedAnd @@ nobody) `congruently` \un ->+        let ovs = un refl inputShares+         in xor (fst <$> ovs) && xor (snd <$> ovs)+    secretShare parties trustedAnd (singleton, outputVal)+  XorGate l r -> do+    lResult <- compute l+    rResult <- compute r+    parties `parallel` \p un -> pure (viewFacet un p lResult /= viewFacet un p rResult)+  where+    compute = computeWire trustedAnd parties+    partyNames = toLocs parties++mpc ::+  (KnownSymbols parties, MonadIO m) =>+  Circuit parties ->+  Choreo ("trusted3rdParty" ': parties) (CLI m) ()+mpc circuit = do+  let parties = consSuper refl+  outputWire <- computeWire trusted3rdParty parties circuit+  result <- enclave parties $ reveal outputWire+  parties `parallel_` \p un -> putOutput "The resulting bit:" $ un p result
+ examples/MergeSort.hs view
@@ -0,0 +1,141 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++# Example: merge sort++## Overview++This example implements the three-way concurrent implementation of merge sort shown in [Object-Oriented Choreographic Programming](https://arxiv.org/abs/2005.09520).++## Execution++This choreography will sort the list `[1, 6, 5, 3, 4, 2, 7, 8]`. It requires three locations: `primary`, `worker1`, and `worker2`.++```bash+# start two workers on separate terminals+cabal run mergesort worker1+cabal run mergesort worker2+# start primary on another terminal+cabal run mergesort primary+[1,2,3,4,5,6,7,8]+```+-}++module MergeSort where++import Choreography+import Choreography.Network.Http+import GHC.TypeLits (KnownSymbol)+import System.Environment++divide :: [a] -> ([a], [a])+divide xs = splitAt lhx xs+  where+    lhx = length xs `div` 2++$(mkLoc "primary")+$(mkLoc "worker1")+$(mkLoc "worker2")++type Participants = ["primary", "worker1", "worker2"]++sort ::+  ( KnownSymbol a,+    KnownSymbol c,+    KnownSymbol b,+    KnownSymbols ps+  ) =>+  Member a ps ->+  Member b ps ->+  Member c ps ->+  Located '[a] [Int] ->+  Choreo ps IO (Located '[a] [Int])+sort a b c lst = do+  condition <- a `locally` \un -> do return $ length (un singleton lst) > 1+  broadcast (a, condition) >>= \case+    True -> do+      _ <- a `locally` \un -> do return $ length (un singleton lst) `div` 2+      divided <- a `locally` \un -> do return $ divide (un singleton lst)+      l <- a `locally` \un -> do return $ fst (un singleton divided)+      r <- a `locally` \un -> do return $ snd (un singleton divided)+      l' <- (a, l) ~> b @@ nobody+      r' <- (a, r) ~> c @@ nobody+      ls' <- sort b c a l'+      rs' <- sort c a b r'+      merge a b c ls' rs'+    False -> do+      return lst++merge ::+  ( KnownSymbol a,+    KnownSymbol c,+    KnownSymbol b,+    KnownSymbols ps+  ) =>+  Member a ps ->+  Member b ps ->+  Member c ps ->+  Located '[b] [Int] ->+  Located '[c] [Int] ->+  Choreo ps IO (Located '[a] [Int])+merge a b c lhs rhs = do+  lhsHasElements <- b `locally` \un -> do return $ not (null (un singleton lhs))+  broadcast (b, lhsHasElements) >>= \case+    True -> do+      rhsHasElements <- c `locally` \un -> do return $ not (null (un singleton rhs))+      broadcast (c, rhsHasElements) >>= \case+        True -> do+          rhsHeadAtC <- c `locally` \un -> do return $ head (un singleton rhs)+          rhsHeadAtB <- (c, rhsHeadAtC) ~> b @@ nobody+          takeLhs <- b `locally` \un -> do return $ head (un singleton lhs) <= un singleton rhsHeadAtB+          broadcast (b, takeLhs) >>= \case+            True -> do+              -- take (head lhs) and merge the rest+              lhs' <- b `locally` \un -> do return $ tail (un singleton lhs)+              merged <- merge a b c lhs' rhs+              lhsHeadAtB <- b `locally` \un -> do return $ head (un singleton lhs)+              lhsHeadAtA <- (b, lhsHeadAtB) ~> a @@ nobody+              a `locally` \un -> do return $ un singleton lhsHeadAtA : un singleton merged+            False -> do+              -- take (head rhs) and merge the rest+              rhs' <- c `locally` \un -> do return $ tail (un singleton rhs)+              merged <- merge a b c lhs rhs'+              rhsHeadAtC' <- c `locally` \un -> do return $ head (un singleton rhs)+              rhsHeadAtA <- (c, rhsHeadAtC') ~> a @@ nobody+              a `locally` \un -> do return $ un singleton rhsHeadAtA : un singleton merged+        False -> do+          (b, lhs) ~> a @@ nobody+    False -> do+      (c, rhs) ~> a @@ nobody++mainChoreo :: Choreo Participants IO ()+mainChoreo = do+  lst <- primary `_locally` return [1, 6, 5, 3, 4, 2, 7, 8]+  sorted <- sort primary worker1 worker2 lst+  _ <-+    primary `locally` \un -> do+      print (un primary sorted)+      return ()+  return ()++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "primary" -> runChoreography config mainChoreo "primary"+    "worker1" -> runChoreography config mainChoreo "worker1"+    "worker2" -> runChoreography config mainChoreo "worker2"+    _ -> error "unknown worker"+  return ()+  where+    config =+      mkHttpConfig+        [ ("primary", ("localhost", 3000)),+          ("worker1", ("localhost", 4000)),+          ("worker2", ("localhost", 5000))+        ]
+ examples/ObliviousTransfer.hs view
@@ -0,0 +1,279 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++module ObliviousTransfer (ot2, ot4, main) where++import CLI+import Choreography+import Choreography.Network.Http+import Control.Monad.Cont (MonadIO, liftIO)+-- For cryptonite++import Crypto.Hash.Algorithms qualified as HASH+import Crypto.PubKey.RSA qualified as RSA+import Crypto.PubKey.RSA.OAEP qualified as OAEP+import Crypto.Random.Types qualified as CRT+import Data.Bits (shiftL)+import Data.ByteString qualified as BS+import Data.ByteString.Char8 (ByteString, pack)+import GHC.TypeLits (KnownSymbol)+import System.Environment++-- Helpers for RSA encryption+genKeyPair :: (CRT.MonadRandom m) => m (RSA.PublicKey, RSA.PrivateKey)+genKeyPair = RSA.generate 64 65537++encryptRSA :: (CRT.MonadRandom m) => RSA.PublicKey -> Bool -> m ByteString+encryptRSA p a = do+  let bs = boolToByteString a+  x <- OAEP.encrypt (OAEP.defaultOAEPParams HASH.SHA1) p bs+  case x of+    Left _ -> undefined+    Right b -> return b++decryptRSA :: (CRT.MonadRandom m) => RSA.PrivateKey -> ByteString -> m Bool+decryptRSA r bs = do+  x <- OAEP.decryptSafer (OAEP.defaultOAEPParams HASH.SHA1) r bs+  case x of+    Left _ -> undefined+    Right b -> return $ byteStringToBool b++boolToByteString :: Bool -> BS.StrictByteString+boolToByteString = pack . show++byteStringToBool :: BS.StrictByteString -> Bool+byteStringToBool bs+  | bs == pack (show True) = True+  | bs == pack (show False) = False+  | otherwise = undefined++generateFakePK :: (CRT.MonadRandom m) => m RSA.PublicKey+generateFakePK = do+  bytes <- CRT.getRandomBytes 64+  return $ RSA.PublicKey 64 (bytesToInteger bytes) 65537+  where+    bytesToInteger bs = foldl (\acc byte -> (acc `shiftL` 8) + fromIntegral byte) 0 (BS.unpack bs)++--------------------------------------------------+-- 1-out-of-2 Oblivious transfer+--------------------------------------------------+ot2Insecure ::+  forall sender receiver m.+  (KnownSymbol sender, KnownSymbol receiver, MonadIO m) =>+  Located '[sender] Bool ->+  Located '[sender] Bool ->+  Located '[receiver] Bool ->+  Choreo '[sender, receiver] (CLI m) (Located '[receiver] Bool)+ot2Insecure b1 b2 s = do+  let sender = listedFirst :: Member sender '[sender, receiver]+  let receiver = listedSecond :: Member receiver '[sender, receiver]+  sr <- (receiver, s) ~> sender @@ nobody+  (sender, \un -> return $ un singleton $ if un singleton sr then b1 else b2) ~~> receiver @@ nobody++genKeys :: (CRT.MonadRandom m) => Bool -> m (RSA.PublicKey, RSA.PublicKey, RSA.PrivateKey)+genKeys s = do+  -- Generate keys for OT. One key is real, and one is fake - select bit decides+  (pk, sk) <- genKeyPair+  fakePk <- generateFakePK+  return $ if s then (pk, fakePk, sk) else (fakePk, pk, sk)++encryptS ::+  (CRT.MonadRandom m) => -- Encryption based on select bit+  (RSA.PublicKey, RSA.PublicKey) ->+  Bool ->+  Bool ->+  m (ByteString, ByteString)+encryptS (pk1, pk2) b1 b2 = do c1 <- encryptRSA pk1 b1; c2 <- encryptRSA pk2 b2; return (c1, c2)++decryptS ::+  (CRT.MonadRandom m) => -- Decryption based on select bit+  (RSA.PublicKey, RSA.PublicKey, RSA.PrivateKey) ->+  Bool ->+  (ByteString, ByteString) ->+  m Bool+decryptS (_, _, sk) s (c1, c2) = if s then decryptRSA sk c1 else decryptRSA sk c2++-- One out of two OT+ot2 ::+  (KnownSymbol sender, KnownSymbol receiver, MonadIO m, CRT.MonadRandom m) =>+  Located '[sender] (Bool, Bool) ->+  Located '[receiver] Bool ->+  Choreo '[sender, receiver] (CLI m) (Located '[receiver] Bool)+ot2 bb s = do+  let sender = listedFirst :: Member sender '[sender, receiver]+  let receiver = listedSecond :: Member receiver '[sender, receiver]++  keys <- locally receiver \un -> liftIO $ genKeys $ un singleton s+  pks <-+    ( receiver,+      \un ->+        let (pk1, pk2, _) = un singleton keys+         in return (pk1, pk2)+      )+      ~~> sender+      @@ nobody+  encrypted <-+    ( sender,+      \un ->+        let (b1, b2) = un singleton bb+         in liftIO $ encryptS (un singleton pks) b1 b2+      )+      ~~> receiver+      @@ nobody+  locally receiver \un ->+    liftIO $+      decryptS+        (un singleton keys)+        (un singleton s)+        (un singleton encrypted)++--------------------------------------------------+-- 1-out-of-4 Oblivious transfer+--------------------------------------------------++select4 :: Bool -> Bool -> a -> a -> a -> a -> a+select4 s1 s2 v1 v2 v3 v4 = case (s1, s2) of+  (True, True) -> v1+  (True, False) -> v2+  (False, True) -> v3+  (False, False) -> v4++ot4Insecure ::+  forall sender receiver m.+  (KnownSymbol sender, KnownSymbol receiver, MonadIO m) =>+  Located '[sender] Bool -> -- sender+  Located '[sender] Bool -> -- sender+  Located '[sender] Bool -> -- sender+  Located '[sender] Bool -> -- sender+  Located '[receiver] Bool -> -- receiver+  Located '[receiver] Bool -> -- receiver+  Choreo '[sender, receiver] (CLI m) (Located '[receiver] Bool)+ot4Insecure b1 b2 b3 b4 s1 s2 = do+  let sender = listedFirst :: Member sender '[sender, receiver]+  let receiver = listedSecond :: Member receiver '[sender, receiver]++  s1r <- (receiver, s1) ~> sender @@ nobody+  s2r <- (receiver, s2) ~> sender @@ nobody+  (sender, \un -> return $ un singleton $ select4 (un singleton s1r) (un singleton s2r) b1 b2 b3 b4) ~~> receiver @@ nobody++-- Generate keys for OT, only one has a SK and the rest are fake+genKeys4 ::+  (CRT.MonadRandom m) =>+  Bool ->+  Bool ->+  m (RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PrivateKey)+genKeys4 s1 s2 = do+  (pk, sk) <- genKeyPair+  fakePk1 <- generateFakePK+  fakePk2 <- generateFakePK+  fakePk3 <- generateFakePK+  return $ case (s1, s2) of+    (True, True) -> (pk, fakePk1, fakePk2, fakePk3, sk)+    (True, False) -> (fakePk1, pk, fakePk2, fakePk3, sk)+    (False, True) -> (fakePk1, fakePk2, pk, fakePk3, sk)+    (False, False) -> (fakePk1, fakePk2, fakePk3, pk, sk)++-- Encryption based on select bit+enc4 ::+  (CRT.MonadRandom m) =>+  (RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PublicKey) ->+  Bool ->+  Bool ->+  Bool ->+  Bool ->+  m (ByteString, ByteString, ByteString, ByteString)+enc4 (pk1, pk2, pk3, pk4) b1 b2 b3 b4 = do+  c1 <- encryptRSA pk1 b1+  c2 <- encryptRSA pk2 b2+  c3 <- encryptRSA pk3 b3+  c4 <- encryptRSA pk4 b4+  return (c1, c2, c3, c4)++-- Decryption based on select bit+dec4 ::+  (CRT.MonadRandom m) =>+  (RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PublicKey, RSA.PrivateKey) ->+  Bool ->+  Bool ->+  (ByteString, ByteString, ByteString, ByteString) ->+  m Bool+dec4 (_, _, _, _, sk) s1 s2 (c1, c2, c3, c4) = decryptRSA sk $ select4 s1 s2 c1 c2 c3 c4++-- One out of two OT+ot4 ::+  (KnownSymbol sender, KnownSymbol receiver, MonadIO m, CRT.MonadRandom m) =>+  Located '[sender] Bool ->+  Located '[sender] Bool ->+  Located '[sender] Bool ->+  Located '[sender] Bool ->+  Located '[receiver] Bool ->+  Located '[receiver] Bool ->+  Choreo '[sender, receiver] (CLI m) (Located '[receiver] Bool)+ot4 b1 b2 b3 b4 s1 s2 = do+  let sender = listedFirst :: Member sender '[sender, receiver]+  let receiver = listedSecond :: Member receiver '[sender, receiver]++  keys <- receiver `locally` \un -> (liftIO $ genKeys4 (un singleton s1) (un singleton s2))+  pks <- (receiver, \un -> let (pk1, pk2, pk3, pk4, _) = (un singleton keys) in return (pk1, pk2, pk3, pk4)) ~~> sender @@ nobody+  encrypted <-+    ( sender,+      \un ->+        liftIO $+          enc4+            (un singleton pks)+            (un singleton b1)+            (un singleton b2)+            (un singleton b3)+            (un singleton b4)+      )+      ~~> receiver+      @@ nobody+  decrypted <-+    receiver `locally` \un ->+      liftIO $+        dec4+          (un singleton keys)+          (un singleton s1)+          (un singleton s2)+          (un singleton encrypted)+  return decrypted++-- Test function+otTest :: (KnownSymbol p1, KnownSymbol p2, MonadIO m, CRT.MonadRandom m) => Choreo '[p1, p2] (CLI m) ()+otTest = do+  let p1 = listedFirst :: Member p1 '[p1, p2]+  let p2 = listedSecond :: Member p2 '[p1, p2]+  bb <- p1 `_locally` return (False, True)+  b1 <- p1 `locally` \un -> pure . fst $ un singleton bb+  b2 <- p1 `locally` \un -> pure . snd $ un singleton bb+  s <- p2 `_locally` return False+  otResultI <- ot2Insecure b1 b2 s+  p2 `locally_` \un -> putOutput "OT2 insecure output:" $ un singleton otResultI+  otResult <- ot2 bb s+  p2 `locally_` \un -> putOutput "OT2 output:" $ un singleton otResult++  b3 <- p1 `_locally` return False+  b4 <- p1 `_locally` return True+  s2 <- p2 `_locally` return False+  otResultI4 <- ot4Insecure b1 b2 b3 b4 s s2+  p2 `locally_` \un -> putOutput "OT4 insecure output:" $ un singleton otResultI4+  otResult4 <- ot4 b1 b2 b3 b4 s s2+  p2 `locally_` \un -> putOutput "OT4 output:" $ un singleton otResult4++main :: IO ()+main = do+  [loc] <- getArgs+  delivery <- case loc of+    "client1" -> runCLIIO $ runChoreography cfg (otTest @"client1" @"client2") "client1"+    "client2" -> runCLIIO $ runChoreography cfg (otTest @"client1" @"client2") "client2"+    _ -> error "unknown party"+  print delivery+  where+    cfg =+      mkHttpConfig+        [ ("client1", ("localhost", 4242)),+          ("client2", ("localhost", 4343))+        ]
+ examples/QuickSort.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++# Example: Quicksort++## Overview++This example implements the three-way concurrent implementation of quicksort.++## Execution++This choreography will sort the list `[1, 6, 5, 3, 4, 2, 7, 8]`. It uses the local backend and distribute the computation over threads.++```bash+cabal run quicksort+[1,2,3,4,5,6,7,8]+```++`Reference.hs` contains a single-threaded reference implementation of the algorithm.+-}++module QuickSort where++import Choreography+import Choreography.Network.Local+import Control.Concurrent.Async (mapConcurrently_)+import GHC.TypeLits (KnownSymbol)++reference :: [Int] -> [Int]+reference [] = []+reference (x : xs) = smaller ++ [x] ++ bigger+  where+    smaller = reference [a | a <- xs, a <= x]+    bigger = reference [a | a <- xs, a > x]++$(mkLoc "primary")+$(mkLoc "worker1")+$(mkLoc "worker2")++type Participants = ["primary", "worker1", "worker2"]++quicksort ::+  (KnownSymbol a, KnownSymbol b, KnownSymbol c, KnownSymbols ps) =>+  Member a ps ->+  Member b ps ->+  Member c ps ->+  Located '[a] [Int] ->+  Choreo ps IO (Located '[a] [Int])+quicksort a b c lst = do+  isEmpty <- a `locally` \un -> pure (null (un singleton lst))+  broadcast (a, isEmpty) >>= \case+    True -> do+      a `_locally` pure []+    False -> do+      smaller <- (a, \un -> let x : xs = un singleton lst in pure [i | i <- xs, i <= x]) ~~> b @@ nobody+      smaller' <- quicksort b c a smaller+      smaller'' <- (b, smaller') ~> a @@ nobody+      bigger <- (a, \un -> let x : xs = un singleton lst in pure [i | i <- xs, i > x]) ~~> c @@ nobody+      bigger' <- quicksort c a b bigger+      bigger'' <- (c, bigger') ~> a @@ nobody+      a `locally` \un -> pure $ un singleton smaller'' ++ [head (un singleton lst)] ++ un singleton bigger''++mainChoreo :: Choreo Participants IO ()+mainChoreo = do+  lst <- primary `_locally` return [1, 6, 5, 3, 4, 2, 7, 8]+  sorted <- quicksort primary worker1 worker2 lst+  primary `locally_` \un -> do+    print (un primary sorted)+    return ()+  return ()++main :: IO ()+main = do+  config <- mkLocalConfig locations+  mapConcurrently_ (runChoreography config mainChoreo) locations+  return ()+  where+    locations = ["primary", "worker1", "worker2"]
+ examples/RingLeader.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++{-+# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.++# Ring leader election++Experinmental implementaion of ring leader election.+-}++module RingLeader where++import Choreography+import Choreography.Network.Http+import Control.Monad.Trans.Class+import Control.Monad.Trans.State+import GHC.TypeLits (KnownSymbol)+import System.Environment++-- an edge of the ring is represented as a tuple of two locaitons l and l' where+-- l is on the left of l'+data Edge g+  = forall l l'.+    (KnownSymbol l, KnownSymbol l') =>+    Edge (Member l g) (Member l' g)++-- a ring is a sequence of edges+type Ring g = [Edge g]++type Label = Int++ringLeader :: forall g. (KnownSymbols g) => Ring g -> Choreo g (StateT Label IO) () -- g for graph+ringLeader r = loop r+  where+    loop :: Ring g -> Choreo g (StateT Label IO) ()+    loop [] = loop r -- not very safe!+    loop (x : xs) = do+      finished <- talkToRight x+      if finished+        then return ()+        else loop xs++    talkToRight :: Edge g -> Choreo g (StateT Label IO) Bool+    talkToRight (Edge left right) = do+      ll <- left `_locally` get+      labelLeft <- (left, ll) ~> right @@ nobody+      labelRight <- right `_locally` get++      finished <-+        right `locally` \un ->+          return $ un singleton labelLeft == un singleton labelRight++      broadcast (right, finished) >>= \case+        True -> do+          right `_locally_` lift (putStrLn "I'm the leader")+          return True+        False -> do+          right `locally_` \un -> put (max (un singleton labelLeft) (un singleton labelRight))+          return False++$(mkLoc "nodeA")+$(mkLoc "nodeB")+$(mkLoc "nodeC")+$(mkLoc "nodeD")++type Participants = ["nodeA", "nodeB", "nodeC", "nodeD"]++ring :: Ring Participants+ring =+  [ Edge nodeA nodeB,+    Edge nodeB nodeC,+    Edge nodeC nodeD,+    Edge nodeD nodeA+  ]++main :: IO ()+main = do+  [loc] <- getArgs+  putStrLn "Please input a label:"+  label <- read <$> getLine+  _ <- runStateT (runChoreography config (ringLeader ring) loc) label+  return ()+  where+    config =+      mkHttpConfig+        [ ("nodeA", ("localhost", 4242)),+          ("nodeB", ("localhost", 4343)),+          ("nodeC", ("localhost", 4444)),+          ("nodeD", ("localhost", 4545))+        ]
+ examples/Tests.hs view
@@ -0,0 +1,625 @@+module Tests where++import Bank2PC qualified+import Bookseller0Network qualified+import Bookseller1Simple qualified+import Bookseller2HigherOrder qualified+import Bookseller3LocPoly qualified+import BooksellerFancy qualified+import CLI (runCLIStateful)+import CardGame qualified+import ChooseTeams qualified+import Choreography+import Choreography.Network.Local (mkLocalConfig)+import Control.Concurrent.Async (mapConcurrently)+import Data (BooksellerArgs (..), reference)+import Data.Maybe (maybeToList)+import DelegationFig20 qualified+import DiffieHellman qualified+import Distribution.TestSuite (Test)+import Distribution.TestSuite.QuickCheck+import GMWReal qualified+import KVS5Fig17 qualified+import KVS6SizePoly qualified+import Lottery qualified+import MPCFake qualified+import Test.QuickCheck+  ( Positive,+    Testable,+    getPositive,+    ioProperty,+    (===),+  )++tests :: IO [Test]+tests = return tests'++normalSettings :: TestArgs+normalSettings = stdTestArgs {verbosity = Verbose}++getNormalPT :: (Testable prop) => PropertyTest prop -> Test+getNormalPT = getPropertyTestWith normalSettings++tests' :: [Test]+tests' =+  [ getNormalPT+      PropertyTest+        { name = "tautology",+          tags = [],+          property = \i -> (===) @Int i i+        },+    getNormalPT+      PropertyTest+        { name = "bank-2pc",+          tags = [],+          property = \(args@(Bank2PC.Args txns) :: Bank2PC.Args "alice" "bob") -> ioProperty do+            let situation =+                  [ ("client", Bank2PC.render <$> txns),+                    ("coordinator", []),+                    ("alice", []),+                    ("bob", [])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            results <-+              mapConcurrently+                ( \(name, inputs) ->+                    fst+                      <$> runCLIStateful+                        inputs+                        (runChoreography config Bank2PC.startBank name)+                )+                situation+            return $ results === reference args+        },+    getNormalPT+      PropertyTest+        { name = "bookseller-0-network",+          tags = [],+          property = \args@BooksellerArgs {books, choice, budget} -> ioProperty do+            let situation =+                  [ ("seller", [show books], Bookseller0Network.seller),+                    ("buyer", [show budget, choice], Bookseller0Network.buyer)+                  ]+            config <- mkLocalConfig [l | (l, _, _) <- situation]+            [([], ()), (delivery, ())] <-+              mapConcurrently+                ( \(name, inputs, process) -> runCLIStateful inputs $ runNetwork config name process+                )+                situation+            return $ (read <$> delivery) === maybeToList (reference args)+        },+    getNormalPT+      PropertyTest+        { name = "bookseller-1-simple",+          tags = [],+          property = \args@BooksellerArgs {books, choice, budget} -> ioProperty do+            let situation =+                  [ ("seller", [show books]),+                    ("buyer", [show budget, choice])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [([], ()), (delivery, ())] <-+              mapConcurrently+                ( \(name, inputs) -> runCLIStateful inputs $ runChoreography config Bookseller1Simple.bookseller name+                )+                situation+            return $ (read <$> delivery) === maybeToList (reference args)+        },+    getNormalPT+      PropertyTest+        { name = "bookseller-1-prime",+          tags = [],+          property = \args@BooksellerArgs {books, choice, budget} -> ioProperty do+            let situation =+                  [ ("seller", [show books]),+                    ("buyer", [show budget, choice])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [([], ()), (delivery, ())] <-+              mapConcurrently+                ( \(name, inputs) ->+                    runCLIStateful inputs $+                      runChoreography config Bookseller1Simple.bookseller' name+                )+                situation+            return $ (read <$> delivery) === maybeToList (reference args)+        },+    getNormalPT+      PropertyTest+        { name = "bookseller-2-higher-order",+          tags = [],+          property = \args@(BooksellerArgs {books, choice, budget}, contrib :: Positive Int) -> ioProperty do+            let situation =+                  [ ("seller", [show books]),+                    ("buyer", [choice, show budget]),+                    ("buyer2", [show $ getPositive contrib])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [([], ()), (delivery, ()), ([], ())] <-+              mapConcurrently+                ( \(name, inputs) ->+                    runCLIStateful inputs $+                      runChoreography config (Bookseller2HigherOrder.bookseller Bookseller2HigherOrder.mkDecision2) name+                )+                situation+            return $ (read <$> delivery) === maybeToList (reference args)+        },+    getNormalPT+      PropertyTest+        { name = "bookseller-2-dummy",+          tags = [],+          property = \(args@BooksellerArgs {books, choice, budget}, contrib :: Positive Int) -> ioProperty do+            let situation =+                  [ ("seller", [show books]),+                    ("buyer", [choice, show budget]),+                    ("buyer2", [show $ getPositive contrib]) -- buyer2 doesn't get used+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [([], ()), (delivery, ()), ([], ())] <-+              mapConcurrently+                ( \(name, inputs) ->+                    runCLIStateful inputs $+                      runChoreography config (Bookseller2HigherOrder.bookseller Bookseller2HigherOrder.mkDecision1) name+                )+                situation+            return $ (read <$> delivery) === maybeToList (reference args)+        },+    getNormalPT+      PropertyTest+        { name = "bookseller-3-locpoly",+          tags = [],+          property = \args@BooksellerArgs {books, choice, budget} -> ioProperty do+            let situation =+                  [ ("seller", [show books]),+                    ("buyer", [show budget, choice])+                  ]+            let buyer :: Member "buyer" '["buyer"] = singleton+            config <- mkLocalConfig [l | (l, _) <- situation]+            [([], ()), (delivery, ())] <-+              mapConcurrently+                ( \(name, inputs) ->+                    runCLIStateful inputs $+                      runChoreography config (Bookseller3LocPoly.bookseller buyer) name+                )+                situation+            return $ (read <$> delivery) === maybeToList (reference args)+        },+    getNormalPT+      PropertyTest+        { name = "bookseller-fancy",+          tags = [],+          property = \args@(BooksellerArgs {books, choice, budget}, contrib :: Positive Int, contrib2 :: Positive Int, contrib3 :: Positive Int) -> ioProperty do+            let situation =+                  [ ("seller", [show books]),+                    ("buyer", [choice, show budget]),+                    ("buyer2", [show $ getPositive contrib]),+                    ("buyer3", [show $ getPositive contrib2]),+                    ("buyer4", [show $ getPositive contrib3])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [([], ()), (delivery, ()), ([], ()), ([], ()), ([], ())] <-+              mapConcurrently+                ( \(name, inputs) ->+                    runCLIStateful inputs $+                      runChoreography config (BooksellerFancy.bookseller @["buyer2", "buyer3", "buyer4"] BooksellerFancy.mkDecision2) name+                )+                situation+            return $ (read <$> delivery) === maybeToList (reference args)+        },+    getNormalPT+      PropertyTest+        { name = "card-game",+          tags = [],+          property = \args@(CardGame.Args deck (c1, c2, c3)) -> ioProperty do+            let situation =+                  [ ("dealer", show <$> cycle deck),+                    ("player1", [show c1]),+                    ("player2", [show c2]),+                    ("player3", [show c3])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [[], [r1], [r2], [r3]] <-+              mapConcurrently+                ( \(name, inputs) ->+                    fst+                      <$> runCLIStateful+                        inputs+                        (runChoreography config (CardGame.game @'["player1", "player2", "player3"]) name)+                )+                situation+            return $ (read r1, read r2, read r3) === reference args+        },+    getNormalPT+      PropertyTest+        { name = "choose-teams",+          tags = [],+          property = \args@(ChooseTeams.Args (c2, c4)) -> ioProperty do+            let situation =+                  [ ("player1", []),+                    ("player2", [show c2]),+                    ("player3", []),+                    ("player4", [show c4]),+                    ("player5", [])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            results <-+              mapConcurrently+                ( \(name, inputs) ->+                    fst+                      <$> runCLIStateful+                        inputs+                        (runChoreography config (ChooseTeams.game @'["player1", "player2", "player3", "player4", "player5"]) name)+                )+                situation+            let [r1, r2, r3, r4, r5] = [concatMap read r | r <- results]+            return $ (r1, r2, r3, r4, r5) === reference args+        },+    getNormalPT+      PropertyTest+        { name = "delegation-fig20",+          tags = [],+          property =+            \args@DelegationFig20.Args+               { DelegationFig20.choice = choice,+                 DelegationFig20.aliceQ = aliceQ,+                 DelegationFig20.bobQ = bobQ,+                 DelegationFig20.carrollF = carrollF+               } -> ioProperty do+                let situation =+                      [ ("alice", [show choice, aliceQ]),+                        ("bob", [bobQ]),+                        ("carroll", [carrollF])+                      ]+                config <- mkLocalConfig [l | (l, _) <- situation]+                [aliceR, bobR, carrollR] <-+                  mapConcurrently+                    ( \(name, inputs) ->+                        fst+                          <$> runCLIStateful+                            inputs+                            (runChoreography config DelegationFig20.mainCho name)+                    )+                    situation+                return $+                  DelegationFig20.Result+                    { DelegationFig20.aliceR = aliceR,+                      DelegationFig20.bobR = bobR,+                      DelegationFig20.carrollR = carrollR+                    }+                    === reference args+        },+    getNormalPT+      PropertyTest -- This test is kinda dumb, but I don't know how better to express "correctness" of DHKE.+        { name = "diffie-hellman",+          tags = [],+          property = \() -> ioProperty do+            let situation =+                  [ ("alice", [""]),+                    ("bob", [])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [[a], [b]] <-+              mapConcurrently+                ( \(name, inputs) ->+                    fst+                      <$> runCLIStateful+                        inputs+                        (runChoreography config DiffieHellman.diffieHellman name)+                )+                situation+            return $ read @Integer a === read @Integer b+        },+    getNormalPT+      PropertyTest+        { name = "kvs-5-fig17",+          tags = [],+          property =+            \args@KVS5Fig17.Args+               { KVS5Fig17.request = request,+                 KVS5Fig17.handler = handler+               } -> ioProperty do+                let situation =+                      [ ("client", [show request]),+                        ("primary", [handler]),+                        ("backup", [])+                      ]+                config <- mkLocalConfig [l | (l, _) <- situation]+                [[response], [], []] <-+                  mapConcurrently+                    ( \(name, inputs) ->+                        fst+                          <$> runCLIStateful+                            inputs+                            (runChoreography config KVS5Fig17.kvs name)+                    )+                    situation+                return $ read response === reference args+        },+    getNormalPT+      PropertyTest+        { name = "kvs-6-sizepoly",+          tags = [],+          property = \(KVS6SizePoly.Args requests) -> ioProperty do+            let situation =+                  [ ("clientAlice", show <$> requests),+                    ("primaryBob", []),+                    ("backup1", []),+                    ("backup2", []),+                    ("backup3", []),+                    ("backup4", []),+                    ("backup5", [])+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            let strategy1 =+                  KVS6SizePoly.naryReplicationStrategy+                    ( explicitMember ::+                        Member+                          "primaryBob"+                          '[ "clientAlice",+                             "primaryBob",+                             "backup1",+                             "backup2",+                             "backup3",+                             "backup4",+                             "backup5"+                           ]+                    )+                    (consSuper $ consSuper refl)+            let client :: Member "clientAlice" '["clientAlice", "primaryBob", "backup1", "backup2", "backup3", "backup4", "backup5"]+                client = explicitMember+            [responsesA, [], [], [], [], [], []] <-+              mapConcurrently+                ( \(name, inputs) ->+                    fst+                      <$> runCLIStateful+                        inputs+                        (runChoreography config (KVS6SizePoly.kvs strategy1 client) name)+                )+                situation+            let strategy2 =+                  KVS6SizePoly.nullReplicationStrategy+                    ( explicitMember ::+                        Member+                          "primaryBob"+                          '[ "clientAlice",+                             "primaryBob",+                             "backup1",+                             "backup2",+                             "backup3",+                             "backup4",+                             "backup5"+                           ]+                    )+            (responsesB, ()) <- runCLIStateful (show <$> requests) $ runChoreo (KVS6SizePoly.kvs strategy2 client)+            return $ responsesA === responsesB+        },+    getNormalPT+      PropertyTest+        { name = "lottery",+          tags = [],+          property =+            \args@Lottery.Args+               { Lottery.secrets = (c1, c2, c3, c4, c5),+                 Lottery.randomIs = (s1, s2, s3)+               } -> ioProperty do+                let clientProof ::+                      Subset+                        '["client1", "client2", "client3", "client4", "client5"]+                        '[ "client1",+                           "client2",+                           "client3",+                           "client4",+                           "client5",+                           "server1",+                           "server2",+                           "server3",+                           "analyst"+                         ]+                    clientProof = explicitSubset+                    serverProof ::+                      Subset+                        '["server1", "server2", "server3"]+                        '[ "client1",+                           "client2",+                           "client3",+                           "client4",+                           "client5",+                           "server1",+                           "server2",+                           "server3",+                           "analyst"+                         ]+                    serverProof = explicitSubset+                    analystProof ::+                      Member+                        "analyst"+                        '[ "client1",+                           "client2",+                           "client3",+                           "client4",+                           "client5",+                           "server1",+                           "server2",+                           "server3",+                           "analyst"+                         ]+                    analystProof = explicitMember+                let situation =+                      [ ("client1", [show c1]),+                        ("client2", [show c2]),+                        ("client3", [show c3]),+                        ("client4", [show c4]),+                        ("client5", [show c5]),+                        ("server1", [show s1]),+                        ("server2", [show s2]),+                        ("server3", [show s3]),+                        ("analyst", [])+                      ]+                config <- mkLocalConfig [l | (l, _) <- situation]+                [ [],+                  [],+                  [],+                  [],+                  [], -- clients return nothing+                  [],+                  [],+                  [], -- servers return nothing+                  [response]+                  ] <-+                  mapConcurrently+                    ( \(name, inputs) ->+                        fst+                          <$> runCLIStateful+                            inputs+                            (runChoreography config (Lottery.lottery clientProof serverProof analystProof) name)+                    )+                    situation+                return $ read @Lottery.Fp response === reference args+        },+    getNormalPT+      PropertyTest+        { name = "lottery-central-semantics", -- We don't have good controls over the sequencing of party-loops or operations in the central semantics;+        -- but at least it's deterministic and this will notice if it breaks!+          tags = [],+          property =+            \Lottery.Args+               { Lottery.secrets = (c1, c2, c3, c4, c5),+                 Lottery.randomIs = (s1, s2, s3)+               } -> ioProperty do+                let clientProof ::+                      Subset+                        '["client1", "client2", "client3", "client4", "client5"]+                        '[ "client1",+                           "client2",+                           "client3",+                           "client4",+                           "client5",+                           "server1",+                           "server2",+                           "server3",+                           "analyst"+                         ]+                    clientProof = explicitSubset+                    serverProof ::+                      Subset+                        '["server1", "server2", "server3"]+                        '[ "client1",+                           "client2",+                           "client3",+                           "client4",+                           "client5",+                           "server1",+                           "server2",+                           "server3",+                           "analyst"+                         ]+                    serverProof = explicitSubset+                    analystProof ::+                      Member+                        "analyst"+                        '[ "client1",+                           "client2",+                           "client3",+                           "client4",+                           "client5",+                           "server1",+                           "server2",+                           "server3",+                           "analyst"+                         ]+                    analystProof = explicitMember+                    lottery = Lottery.lottery clientProof serverProof analystProof+                let situation =+                      [ ("client1", [show c1]),+                        ("client2", [show c2]),+                        ("client3", [show c3]),+                        ("client4", [show c4]),+                        ("client5", [show c5]),+                        ("server1", [show s1]),+                        ("server2", [show s2]),+                        ("server3", [show s3]),+                        ("analyst", [])+                      ]+                config <- mkLocalConfig [l | (l, _) <- situation]+                [ [],+                  [],+                  [],+                  [],+                  [],+                  [],+                  [],+                  [],+                  [response]+                  ] <-+                  mapConcurrently+                    ( \(name, inputs) ->+                        fst+                          <$> runCLIStateful+                            inputs+                            (runChoreography config lottery name)+                    )+                    situation+                [centralSemanticsResponse] <-+                  fst+                    <$> runCLIStateful+                      [ show c1,+                        show c2,+                        show c3,+                        show c4,+                        show c5,+                        show s1,+                        show s2,+                        show s3+                      ]+                      (runChoreo lottery)+                return $ read @Lottery.Fp response === read centralSemanticsResponse+        },+    getNormalPT+      PropertyTest+        { name = "mpc-fake",+          tags = [],+          property = \args@(MPCFake.Args circuit p1in p2in p3in p4in) -> ioProperty do+            let situation =+                  [ ("trusted3rdParty", []),+                    ("p1", repeat $ show p1in),+                    ("p2", repeat $ show p2in),+                    ("p3", repeat $ show p3in),+                    ("p4", repeat $ show p4in)+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [[], [r1], [r2], [r3], [r4]] <-+              mapConcurrently+                ( \(name, inputs) ->+                    fst+                      <$> runCLIStateful+                        inputs+                        (runChoreography config (MPCFake.mpc circuit) name)+                )+                situation+            return $ (read r1, read r2, read r3, read r4) === reference args+        },+    getPropertyTestWith+      (stdTestArgs {verbosity = Verbose, maxSuccess = 100, maxSize = 10})+      PropertyTest+        { name = "gmw-real",+          tags = [],+          property = \args@(GMWReal.Args circuit p1in p2in p3in p4in) -> ioProperty do+            let situation =+                  [ ("p1", repeat $ show p1in),+                    ("p2", repeat $ show p2in),+                    ("p3", repeat $ show p3in),+                    ("p4", repeat $ show p4in)+                  ]+            config <- mkLocalConfig [l | (l, _) <- situation]+            [[r1], [r2], [r3], [r4]] <-+              mapConcurrently+                ( \(name, inputs) ->+                    fst+                      <$> runCLIStateful+                        inputs+                        (runChoreography config (GMWReal.mpc circuit) name)+                )+                situation+            return $ (read r1, read r2, read r3, read r4) === reference args+        }+  ]
+ src/Choreography.hs view
@@ -0,0 +1,28 @@+-- | This is just a wrapper module to allow more concise imports.+--     For documentation, you should probably start in "Choreography.Core".+module Choreography+  ( module Choreography.Core,+    module Choreography.Choreography,+    module Choreography.Choreography.Batteries,+    module Choreography.Locations,+    module Choreography.Locations.Batteries,+    module Choreography.Network,+    module Choreography.Polymorphism,++    -- * Running choreographies+    runChoreography,+  )+where++import Choreography.Choreography+import Choreography.Choreography.Batteries+import Choreography.Core+import Choreography.Locations+import Choreography.Locations.Batteries+import Choreography.Network+import Choreography.Polymorphism+import Control.Monad.IO.Class (MonadIO)++-- | Run a choreography with a message transport backend...+runChoreography :: (Backend config, MonadIO m, KnownSymbols ps) => config -> Choreo ps m a -> LocTm -> m a+runChoreography cfg choreo l = runNetwork cfg l (epp choreo l)
+ src/Choreography/Choreography.hs view
@@ -0,0 +1,119 @@+-- | Operations for writing choreographies.+module Choreography.Choreography where++import Choreography.Core+import Choreography.Locations+import Choreography.Locations.Batteries (ExplicitMember (..))+import GHC.TypeLits++-- * Computation /per se/++-- | Perform a local computation at a given location.+locally ::+  (KnownSymbol (l :: LocTy)) =>+  -- | Location performing the local computation.+  Member l ps ->+  -- | The local computation, which can use a constrained unwrap function.+  (Unwrap l -> m a) ->+  Choreo ps m (Located '[l] a)++infix 4 `locally`++locally l m = enclave (l @@ nobody) $ locally' m++-- | Perform the exact same pure computation in replicate at multiple locations.+--   The computation can not use anything local to an individual party, including their identity.+congruently ::+  forall ls a ps m.+  (KnownSymbols ls) =>+  Subset ls ps ->+  (Unwraps ls -> a) ->+  Choreo ps m (Located ls a)++infix 4 `congruently`++congruently ls a = enclave ls $ congruently' a++-- | Unwrap a value known to the entire census.+naked ::+  (KnownSymbols ps) =>+  Subset ps qs ->+  Located qs a ->+  Choreo ps m a+naked ownership a = congruently' (\un -> un ownership a)++-- * Communication++-- | Writing out the first argument to `~>` can be done a few different ways depending on context, represented by this class.+class (KnownSymbol loc) => CanSend struct loc val owners census | struct -> loc val owners census where+  presentToSend :: struct -> Member loc census+  ownsMessagePayload :: struct -> Member loc owners+  structMessagePayload :: struct -> Located owners val++instance (KnownSymbol l) => CanSend (Member l ps, (Member l ls, Located ls a)) l a ls ps where+  presentToSend = fst+  ownsMessagePayload = fst . snd+  structMessagePayload = snd . snd++instance (KnownSymbol l, ExplicitMember l ls) => CanSend (Member l ps, Located ls a) l a ls ps where+  presentToSend = fst+  ownsMessagePayload = const explicitMember+  structMessagePayload = snd++instance (KnownSymbol l) => CanSend (Member l ls, Subset ls ps, Located ls a) l a ls ps where+  presentToSend (m, s, _) = inSuper s m+  ownsMessagePayload (m, _, _) = m+  structMessagePayload (_, _, p) = p++-- | Send a value from one party to the entire census.+broadcast ::+  forall l a ps ls m s.+  (Show a, Read a, KnownSymbol l, KnownSymbols ps, CanSend s l a ls ps) =>+  s ->+  Choreo ps m a+broadcast s = broadcast' (presentToSend s) (ownsMessagePayload s, structMessagePayload s)++-- | Communication between a sender and a list of receivers.+(~>) ::+  (Show a, Read a, KnownSymbol l, KnownSymbols ls', CanSend s l a ls ps) =>+  -- | The message argument can take three forms:+  --+  --   >  (Member sender census, wrapped owners a) -- where sender is explicitly listed in owners+  --+  --   >  (Member sender owners, Subset owners census, wrapped owners a)+  --+  --   >  (Member sender census, (Member sender owners, wrapped owners a)+  s ->+  -- | The recipients.+  Subset ls' ps ->+  Choreo ps m (Located ls' a)++infix 4 ~>++s ~> rs = do+  x :: a <- enclave (presentToSend s @@ rs) $ broadcast' First (ownsMessagePayload s, structMessagePayload s)+  congruently rs (\un -> un consSet x)++-- * Enclaves++-- | Lift a choreography involving fewer parties into the larger party space.+--   This version, where the returned value is Located at the entire enclave, does not add a Located layer.+enclaveToAll :: forall ls a ps m. (KnownSymbols ls) => Subset ls ps -> Choreo ls m (Located ls a) -> Choreo ps m (Located ls a)++infix 4 `enclaveToAll`++enclaveToAll = (`enclaveTo` (refl @ls))++-- | Lift a choreography of involving fewer parties into the larger party space.+--   This version, where the returned value is already Located, does not add a Located layer.+enclaveTo ::+  forall ls a rs ps m.+  (KnownSymbols ls) =>+  Subset ls ps ->+  Subset rs ls ->+  Choreo ls m (Located rs a) ->+  Choreo ps m (Located rs a)++infix 4 `enclaveTo`++enclaveTo subcensus recipients ch = flatten recipients (refl @rs) <$> (subcensus `enclave` ch)
+ src/Choreography/Choreography/Batteries.hs view
@@ -0,0 +1,121 @@+-- | A zoo of helpful derived functions for writing choreographies.+module Choreography.Choreography.Batteries where++import Choreography.Choreography+import Choreography.Core+import Choreography.Locations+import Control.Monad (void)+import GHC.TypeLits++-- * Computation /per se/++-- | Perform a local computation, yielding nothing.+locally_ ::+  (KnownSymbol l) =>+  Member l ps ->+  (Unwrap l -> m ()) ->+  Choreo ps m ()++infix 4 `locally_`++locally_ l m = void $ locally l m++-- | Perform a local computation that doesn't need to unwrap any existing `Located` values.+_locally ::+  (KnownSymbol l) =>+  Member l ps ->+  m a ->+  Choreo ps m (Located '[l] a)++infix 4 `_locally`++_locally l m = locally l $ const m++-- | Perform a local computation that doesn't need to unwrap any existing `Located` values and yields nothing.+_locally_ :: (KnownSymbol l) => Member l ps -> m () -> Choreo ps m ()++infix 4 `_locally_`++_locally_ l m = void $ locally l (const m)++-- | Perform a pure computation at a single location.+purely ::+  forall l a ps m.+  (KnownSymbol l) =>+  Member l ps ->+  (Unwrap l -> a) ->+  Choreo ps m (Located '[l] a)++infix 4 `purely`++purely l a =+  congruently+    (Subset \First -> l)+    ( \un ->+        let un' :: Unwrap l -- There is definitley a nicer way to write this...+            un' mem = un (Subset \First -> mem)+         in a un'+    )++-- * Communication++-- | A variant of `~>` that sends the result of a local computation.+(~~>) ::+  forall a l ls' m ps.+  (Show a, Read a, KnownSymbol l, KnownSymbols ls') =>+  -- | A pair of a sender's location and a local computation.+  (Member l ps, Unwrap l -> m a) ->+  -- | A receiver's location.+  Subset ls' ps ->+  Choreo ps m (Located ls' a)++infix 4 ~~>++(~~>) (l, m) ls' = do+  x <- locally l m+  (l, x) ~> ls'++-- | A variant of `~>` that sends the result of a local action that doesn't use existing `Located` variables.+(-~>) ::+  forall a l ls' m ps.+  (Show a, Read a, KnownSymbol l, KnownSymbols ls') =>+  -- | A pair of a sender's location and a local computation.+  (Member l ps, m a) ->+  -- | A receiver's location.+  Subset ls' ps ->+  Choreo ps m (Located ls' a)++infix 4 -~>++(-~>) (l, m) ls' = do+  x <- l `_locally` m+  (l, x) ~> ls'++-- | A variant of `~>` that doesn't use the local monad.+(*~>) ::+  forall a l ls' m ps.+  (Show a, Read a, KnownSymbol l, KnownSymbols ls') =>+  -- | A pair of a sender's location and a local computation.+  (Member l ps, Unwrap l -> a) ->+  -- | A receiver's location.+  Subset ls' ps ->+  Choreo ps m (Located ls' a)++infix 4 *~>++(*~>) (l, m) ls' = do+  x <- l @@ nobody `congruently` \uns -> m $ uns . (@@ nobody)+  (l, x) ~> ls'++-- * Enclaves++-- | Conditionally execute choreographies based on a located value. Automatically enclaves.+cond ::+  (KnownSymbols ls) =>+  -- | Tuple: Proof all the parties involved know the branch-guard+  -- and are present, the branch guard+  (Subset ls ps, (Subset ls qs, Located qs a)) ->+  -- | The body of the conditional as a function from the unwrapped value.+  (a -> Choreo ls m b) ->+  Choreo ps m (Located ls b)+cond (ls, (owns, a)) c = enclave ls $ naked owns a >>= c
+ src/Choreography/Core.hs view
@@ -0,0 +1,198 @@+-- | This module defines `Choreo`, the monad for writing choreographies,+--   and the closely related `Located` data type.+--   Not everything here is user-friendly; this is were we declare the foundational concepts.+--   These get repackaged in more convienent ways in "Choreography.Choreography"+--   and "Choreography.Choreography.Batteries".+module Choreography.Core+  ( -- * The `Choreo` monad and its operators+    Choreo,+    broadcast',+    -- , ChoreoSig(..)  I can't think of any reasons why we _should_ export this, nor any reason why we shouldn't...+    locally',+    congruently',+    enclave,++    -- * Running choreographies+    epp,+    runChoreo,++    -- * Located values+    Located (),+    Unwrap,+    Unwraps,+    flatten,+    othersForget,+    wrap, -- consider renaming or removing.+  )+where++import Choreography.Locations+import Choreography.Network+import Control.Monad.Freer+import Data.List (delete)+import GHC.TypeLits++-- | A single value known to many parties.+data Located (ls :: [LocTy]) a+  = Wrap a+  | Empty++-- | Wrap a value as a located value.+--   This should be safe to export, while exporting the constuctor would enable pattern matching.+wrap :: a -> Located l a+wrap = Wrap++-- | Unwraps values known to the specified party.+--   You should not be able to build such a function in normal code;+--   these functions are afforded only for use in "local" computation.+type Unwrap (q :: LocTy) = forall ls a. Member q ls -> Located ls a -> a++-- | Unwraps values known to the specified list of parties.+--   You should not be able to build such a function in normal code;+--   these functions are afforded only for use in "local" computation.+--   (Could be dangerous if the list is empty,+--   but the API is designed so that no value of type `Unwraps '[]` will ever actually get evaluated.)+type Unwraps (qs :: [LocTy]) = forall ls a. Subset qs ls -> Located ls a -> a++-- | Unwrap a `Located` value.+--   Unwrapping a empty located value will throw an exception; THIS SHOULD NOT BE EXPORTED!+unwrap :: Unwrap q+unwrap _ (Wrap a) = a+unwrap _ Empty = error "Located: This should never happen for a well-typed choreography."++-- | Un-nest located values.+flatten :: Subset ls ms -> Subset ls ns -> Located ms (Located ns a) -> Located ls a++infix 3 `flatten`++flatten _ _ Empty = Empty+flatten _ _ (Wrap Empty) = Empty+flatten _ _ (Wrap (Wrap a)) = Wrap a++-- | Cast a `Located` value to a smaller ownership set; useful when working with functions whos arguments have explict ownership sets.+othersForget :: Subset ls owners -> Located owners a -> Located ls a+othersForget _ Empty = Empty+othersForget _ (Wrap a) = Wrap a++data ChoreoSig (ps :: [LocTy]) m a where+  Locally ::+    (KnownSymbol l) =>+    (Unwrap l -> m a) ->+    ChoreoSig '[l] m a+  Congruently ::+    (KnownSymbols ls) =>+    (Unwraps ls -> a) ->+    ChoreoSig ls m a+  Broadcast ::+    (Show a, Read a, KnownSymbol l) =>+    Member l ps -> -- from+    (Member l ls, Located ls a) -> -- value+    ChoreoSig ps m a+  Enclave ::+    (KnownSymbols ls) =>+    Subset ls ps ->+    Choreo ls m b ->+    ChoreoSig ps m (Located ls b)++-- | Monad for writing choreographies.+--     @ps@ is the "census", the list of parties who are present in (that part of) the choreography.+--     @m@ is the local monad afforded to parties by `locally'`.+type Choreo ps m = Freer (ChoreoSig ps m) -- Haddock will complain about not knowning where ChoreoSig is. IDK how to fix it; maybe we should just export++-- | Run a `Choreo` monad with centralized semantics.+--   This basically pretends that the choreography is a single-threaded program and runs it all at once,+--   ignoring all the location aspects.+runChoreo :: forall p ps b m. (Monad m) => Choreo (p ': ps) m b -> m b+runChoreo = interpFreer handler+  where+    handler :: (Monad m) => ChoreoSig (p ': ps) m a -> m a+    handler (Locally m) = m unwrap+    handler (Congruently f) =+      let unwraps :: forall c ls. Subset (p ': ps) ls -> Located ls c -> c+          unwraps = unwrap . (\(Subset mx) -> mx First) -- wish i could write this better.+       in pure . f $ unwraps+    handler (Broadcast _ (p, a)) = pure $ unwrap p a+    handler (Enclave (_ :: Subset ls (p ': ps)) c) = case tySpine @ls of+      TyNil -> pure Empty+      TyCons -> wrap <$> runChoreo c++-- | Endpoint projection.+epp ::+  forall ps b m.+  (Monad m, KnownSymbols ps) =>+  -- | A choreography+  Choreo ps m b ->+  -- | A `String` identifying a party.+  --   At present there is no enforcement that the party will actually be in the census of the choreography;+  --   some bugs may be possible if it is not.+  LocTm ->+  -- | Returns the implementation of the party's role in the choreography.+  Network m b+epp c l' = interpFreer handler c+  where+    handler :: ChoreoSig ps m a -> Network m a+    handler (Locally m) = run $ m unwrap+    handler (Congruently f) =+      let unwraps :: forall c ls. Subset ps ls -> Located ls c -> c+          unwraps = case tySpine @ps of+            TyNil -> error "Undefined projection: the census is empty."+            TyCons -> unwrap . (\(Subset mx) -> mx First) -- wish i could write this better.+       in pure . f $ unwraps+    handler (Broadcast s (l, a)) = do+      let sender = toLocTm s+      let otherRecipients = sender `delete` toLocs (refl :: Subset ps ps)+      if sender == l'+        then do+          send (unwrap l a) otherRecipients+          pure . unwrap l $ a+        else recv sender+    handler (Enclave proof ch)+      | l' `elem` toLocs proof = wrap <$> epp ch l'+      | otherwise = pure Empty++-- | Access to the inner "local" monad.+--   Since the type of `locally'` restricts the census to a single party, you'll usually want to use+--   `Choreography.Choreography.locally` instead.+locally' ::+  (KnownSymbol l) =>+  -- | The local action(s), which can use an unwraper function.+  (Unwrap l -> m a) ->+  Choreo '[l] m a+locally' m = toFreer (Locally m)++-- | Perform the exact same computation in replicate at all participating locations.+--   The computation can not use anything local to an individual party, including their identity.+congruently' ::+  (KnownSymbols ls) =>+  -- | The computation, which can use an unwraper function.+  (Unwraps ls -> a) ->+  Choreo ls m a++infix 4 `congruently'`++congruently' f = toFreer (Congruently f)++-- | Communicate a value to all present parties.+broadcast' ::+  (Show a, Read a, KnownSymbol l) =>+  -- | Proof the sender is present+  Member l ps ->+  -- | Proof the sender knows the value, the value.+  (Member l ls, Located ls a) ->+  Choreo ps m a++infix 4 `broadcast'`++broadcast' l a = toFreer (Broadcast l a)++-- | Lift a choreography of involving fewer parties into the larger party space.+--   Adds a `Located ls` layer to the return type.+enclave ::+  (KnownSymbols ls) =>+  Subset ls ps ->+  Choreo ls m a ->+  Choreo ps m (Located ls a)++infix 4 `enclave`++enclave proof ch = toFreer $ Enclave proof ch
+ src/Choreography/Locations.hs view
@@ -0,0 +1,123 @@+-- | This module defines locations (AKA parties)+--   and functions/relations pertaining to type-level lists of locations.+module Choreography.Locations where++import Data.Proxy (Proxy (..))+import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)++-- * Type aliases++-- | Term-level locations.+type LocTm = String++-- | Type-level locations.+type LocTy = Symbol++-- * Membership and Subset proofs++-- | A term-level proof that a `LocTy` is a member of a @[LocTy]@.+--   These are frequently used both for proofs /per se/ and to identify individuals in lists of locations.+--+--   For example: @player :: Member players census@ is a proof that the type-level `Symbol`, @player@, is in @census@,+--   and it can also be used as a __term-level__ identifier for the __type-level__ @player@,+--   similar to how a @proxy@ might be used.+--+--   Pattern matching on these values is like pattern matching on a successor-based @Nat@;+--   in this sense a @Member x xs@ is an index into @xs@ at which @x@ can be found.+data Member (x :: k) (xs :: [k]) where+  First :: forall xs x xs'. (xs ~ (x ': xs')) => Member x (x ': xs')+  Later :: Member x xs -> Member x (y ': xs)++-- | A term level proof that one type-level list represents a subset of another,+--   embodied by a total function from proof-of-membership in the sublist to proof-of-membership in the superlist.+--   (If you make one with a partial funciton, all bets are off.)+newtype Subset xs ys = Subset+  { -- | Convert a proof of membership in the sublist to a proof of membership in the superlist.+    -- Frequently used to show that a location is part of a larger set of locations.+    inSuper :: forall x. Member x xs -> Member x ys+  }++-- | The subset relation is reflexive.+refl :: Subset xs xs+refl = Subset id++-- | The sublist relation is transitive.+transitive :: Subset xs ys -> Subset ys zs -> Subset xs zs+transitive sxy syz = Subset $ inSuper syz . inSuper sxy++-- | The `[]` case of subset proofs.+-- Typlically used to build subset proofs using membership proofs using `@@`.+nobody :: Subset '[] ys+nobody = Subset \case {}++-- | Any lists is a subset of the list made by consing itself with any other item.+consSet :: forall xs x xs'. (xs ~ (x ': xs')) => Subset xs' (x ': xs')+consSet = Subset Later++-- | Cons an element to the superset in a `Subset` value.+consSuper :: forall xs ys y. Subset xs ys -> Subset xs (y ': ys)+consSuper sxy = transitive sxy consSet++-- | Cons an element to the subset in a `Subset` value;+--   requires proof that the new head element is already a member of the superset.+--   Used like ":" for subset proofs.+--   Suppose you have @(alice :: Member "Alice" census)@+--   and we want a /subset/ proof instead of membership; we can write:+--+--   >>> proof :: Subset '["Alice"] census = alice @@ nobody+(@@) :: Member x ys -> Subset xs ys -> Subset (x ': xs) ys++infixr 5 @@++mxy @@ sxy = Subset \case+  First -> mxy+  Later mxxs -> inSuper sxy mxxs++-- * Accessing parties' names++-- | Convert a proof-level location to a term-level location.+toLocTm ::+  forall (l :: LocTy) (ps :: [LocTy]).+  (KnownSymbol l) =>+  Member l ps ->+  LocTm+toLocTm _ = symbolVal (Proxy @l)++-- | Get the term-level list of names-as-strings for a proof-level list of parties.+toLocs :: forall (ls :: [LocTy]) (ps :: [LocTy]). (KnownSymbols ls) => Subset ls ps -> [LocTm]+toLocs _ = case tySpine @ls of -- this could be golfed by Quire, if that were defined here.+  TyNil -> []+  TyCons -> toLocTm (First @ls) : toLocs (consSet @ls)++-- * Handling type-level lists literals++-- $Handling+--+-- `KnownSymbols` constraints will often need to be declared in user code,+-- but using `tySpine` should only be necessary+-- when the behavior of the choreography depends on the structure of the type-level lists.+-- Most of the time the functions in "Choreography.Polymorphism" should do this for you.++-- | Term-level markers of the spine/structure of a type-level list.+--   Pattern matching on them recovers both the spine of the list and, if applicable,+--   `KnownSymbol`[@s@] instances for the head and tail.+data TySpine ps where+  -- | Denotes that the list has a head and tail, and exposes `KnownSymbol` and `KnownSymbols` constraints respectively.+  TyCons :: (KnownSymbol h, KnownSymbols ts) => TySpine (h ': ts)+  -- | Denotes that the list is empty.+  TyNil :: TySpine '[]++-- | The type-level-list version of `GHC.TypeList.KnownSymbol`.+--   Denotes that both the spine of the list and each of its elements is known at compile-time.+--   This knowlege is typically recovered by recursively pattern-matching on @tySpine \@ls@.+class KnownSymbols ls where+  -- | Pattern matching on @tySpine \@ls@ will normally have two cases, for when @ls@ is empty or not.+  --   Contextual knowledge may let one or the other case be skipped.+  --   Within those cases, the knowledge afforded by `tySpine`'s constructors can be used.+  tySpine :: TySpine ls++instance KnownSymbols '[] where+  tySpine = TyNil++instance (KnownSymbols ls, KnownSymbol l) => KnownSymbols (l ': ls) where+  tySpine = TyCons
+ src/Choreography/Locations/Batteries.hs view
@@ -0,0 +1,97 @@+-- | Additional functions/relations pertaining to locations and type-level lists of locations.+module Choreography.Locations.Batteries where++import Choreography.Locations+import GHC.TypeLits (KnownSymbol)+import Language.Haskell.TH++-- * Misc++-- | Quickly build membership proofs, when the membership can be directly observed by GHC.+class ExplicitMember (x :: k) (xs :: [k]) where+  explicitMember :: Member x xs++instance {-# OVERLAPPABLE #-} (ExplicitMember x xs) => ExplicitMember x (y ': xs) where+  explicitMember = inSuper consSet explicitMember++instance {-# OVERLAPS #-} ExplicitMember x (x ': xs) where+  explicitMember = First++-- | Quickly build subset proofs, when the subset relation can be directly observed by GHC.+class ExplicitSubset xs ys where+  explicitSubset :: Subset xs ys++instance {-# OVERLAPPABLE #-} (ExplicitSubset xs ys, ExplicitMember x ys) => ExplicitSubset (x ': xs) ys where+  explicitSubset = explicitMember @@ explicitSubset++instance {-# OVERLAPS #-} ExplicitSubset '[] ys where+  explicitSubset = nobody++-- | Alias `refl`. When used as an identifier, this is more descriptive.+allOf :: forall ps. Subset ps ps+allOf = refl++-- | Any element @p@ is a member of the list @'[p]@.+singleton :: forall p. Member p (p ': '[])+singleton = First++-- * Easy indexing with `Member` objects.++-- | A `Member` value for the first item in a list.+--   Note that type-applicaiton is different than with `First`, to which this is otherwise redundant.+listedFirst :: forall p1 ps. Member p1 (p1 ': ps) -- Can we replace all of these with something using off-the-shelf type-level Nats?+listedFirst = First++-- | A `Member` value for the second item in a list.+listedSecond :: forall p2 p1 ps. Member p2 (p1 ': p2 ': ps)+listedSecond = inSuper (consSuper refl) listedFirst++-- | A `Member` value for the third item in a list.+listedThird :: forall p3 p2 p1 ps. Member p3 (p1 ': p2 ': p3 ': ps)+listedThird = inSuper (consSuper refl) listedSecond++-- | A `Member` value for the forth item in a list.+listedForth :: forall p4 p3 p2 p1 ps. Member p4 (p1 ': p2 ': p3 ': p4 ': ps)+listedForth = inSuper (consSuper refl) listedThird++-- | A `Member` value for the fifth item in a list.+listedFifth :: forall p5 p4 p3 p2 p1 ps. Member p5 (p1 ': p2 ': p3 ': p4 ': p5 ': ps)+listedFifth = inSuper (consSuper refl) listedForth++-- | A `Member` value for the sixth item in a list.+listedSixth :: forall p6 p5 p4 p3 p2 p1 ps. Member p6 (p1 ': p2 ': p3 ': p4 ': p5 ': p6 ': ps)+listedSixth = inSuper (consSuper refl) listedFifth++-- * Context manipulation++-- | Use any membership proof to to safely call code that only works on a non-empy list.+quorum1 ::+  forall ps p a.+  (KnownSymbols ps) =>+  Member p ps ->+  (forall q qs. (KnownSymbol q, KnownSymbols qs, ps ~ q ': qs) => a) ->+  a+quorum1 p a = case (p, tySpine @ps) of+  (First, TyCons) -> a+  (Later _, TyCons) -> a++-- * Template Haskell++-- | Declare a proof-value with the given string as the variable name, proving that that string is a member of any list in which it explicitly apprears.+mkLoc :: String -> Q [Dec]+mkLoc loc = do+  let locName = mkName loc+  let tvar = mkName "xs"+  let m = mkName "Member"+  let eM = mkName "ExplicitMember"+  let em = mkName "explicitMember"+  pure+    [ SigD+        locName+        ( ForallT+            [PlainTV tvar SpecifiedSpec]+            [AppT (AppT (ConT eM) (LitT (StrTyLit loc))) (VarT tvar)]+            (AppT (AppT (ConT m) (LitT (StrTyLit loc))) (VarT tvar))+        ),+      ValD (VarP locName) (NormalB (VarE em)) []+    ]
+ src/Choreography/Network.hs view
@@ -0,0 +1,56 @@+-- | This module defines the `Network` monad, which represents programs run on+-- individual nodes in a distributed system with explicit sends and receives.+-- To run a `Network` program, we provide a `runNetwork` function that supports+-- multiple message transport backends.+-- Two such backends are provided in "Choreography.Network.Http" and "Choreography.Network.Local",+-- and there should be enough tools here for you to write more as needed.+module Choreography.Network where++import Choreography.Locations (LocTm)+import Control.Monad.Freer+import Control.Monad.IO.Class++-- * The Network monad++-- | Effect signature for the `Network` monad.+data NetworkSig m a where+  -- | Local computation.+  Run ::+    m a ->+    NetworkSig m a+  -- | Sending.+  Send ::+    (Show a) =>+    a ->+    [LocTm] ->+    NetworkSig m ()+  -- | Receiving.+  Recv ::+    (Read a) =>+    LocTm ->+    NetworkSig m a++-- | Monad that represents network programs.+type Network m = Freer (NetworkSig m)++-- * Network operations++-- | Perform a local computation.+run :: m a -> Network m a+run m = toFreer $ Run m++-- | Send a message to a receiver.+send :: (Show a) => a -> [LocTm] -> Network m ()+send a ls = toFreer $ Send a ls++-- | Receive a message from a sender.+recv :: (Read a) => LocTm -> Network m a+recv l = toFreer $ Recv l++-- * Message transport backends++-- | A message transport backend defines a /configuration/ of type @c@ that+-- carries necessary bookkeeping information, then defines @c@ as an instance+-- of `Backend` and provides a `runNetwork` function.+class Backend c where+  runNetwork :: (MonadIO m) => c -> LocTm -> Network m a -> m a
+ src/Choreography/Network/Http.hs view
@@ -0,0 +1,116 @@+-- | This module implments the HTTP message transport backend for the `Network`+-- monad.+module Choreography.Network.Http where++import Choreography.Locations+import Choreography.Network hiding (run, send)+import Control.Concurrent+import Control.Monad+import Control.Monad.Freer+import Control.Monad.IO.Class+import Data.Either (lefts)+import Data.HashMap.Strict (HashMap, (!))+import Data.HashMap.Strict qualified as HashMap+import Data.Proxy (Proxy (..))+import Network.HTTP.Client (Manager, defaultManagerSettings, newManager)+import Network.Wai.Handler.Warp (run)+import Servant.API+import Servant.Client (BaseUrl (..), ClientM, Scheme (..), client, mkClientEnv, runClientM)+import Servant.Server (Handler, Server, serve)++-- * Http configuration++-- | A backend for running `Network` behaviors over HTTP.+--   The configuration specifies how locations are mapped to network hosts and ports.+newtype HttpConfig = HttpConfig+  { locToUrl :: HashMap LocTm BaseUrl+  }++-- | The address of a party/location.+type Host = String++-- | The port of a party/location.+type Port = Int++-- | Create a HTTP backend configuration from a association list that maps+--   locations to network hosts and ports.+mkHttpConfig :: [(LocTm, (Host, Port))] -> HttpConfig+mkHttpConfig = HttpConfig . HashMap.fromList . fmap (fmap f)+  where+    f :: (Host, Port) -> BaseUrl+    f (host, port) =+      BaseUrl+        { baseUrlScheme = Http,+          baseUrlHost = host,+          baseUrlPort = port,+          baseUrlPath = ""+        }++-- | The list of locations known to a backend.+locs :: HttpConfig -> [LocTm]+locs = HashMap.keys . locToUrl++-- * Receiving channels++-- | The channels a location uses to recieve messages from various peers.+type RecvChans = HashMap LocTm (Chan String)++-- | Make the channels that will be used to recieve messages.+mkRecvChans :: HttpConfig -> IO RecvChans+mkRecvChans cfg = foldM f HashMap.empty (locs cfg)+  where+    f ::+      HashMap LocTm (Chan String) ->+      LocTm ->+      IO (HashMap LocTm (Chan String))+    f hm l = do+      c <- newChan+      pure $ HashMap.insert l c hm++-- * HTTP backend++-- | A "Servant.API" API.+type API = "send" :> Capture "from" LocTm :> ReqBody '[PlainText] String :> PostNoContent++-- | Run a `Network` behavior, using the provided HTTP backend.+runNetworkHttp :: (MonadIO m) => HttpConfig -> LocTm -> Network m a -> m a+runNetworkHttp cfg self prog = do+  mgr <- liftIO $ newManager defaultManagerSettings+  chans <- liftIO $ mkRecvChans cfg+  recvT <- liftIO $ forkIO (recvThread cfg chans)+  result <- runNetworkMain mgr chans prog+  liftIO $ threadDelay 1000000 -- wait until all outstanding requests to be completed+  liftIO $ killThread recvT+  pure result+  where+    runNetworkMain :: (MonadIO m) => Manager -> RecvChans -> Network m a -> m a+    runNetworkMain mgr chans = interpFreer handler+      where+        handler :: (MonadIO m) => NetworkSig m a -> m a+        handler (Run m) = m+        handler (Send a ls) = liftIO $ do+          res <- mapM (\l -> runClientM (send self $ show a) (mkClientEnv mgr (locToUrl cfg ! l))) ls+          case lefts res of+            [] -> pure ()+            errors -> putStrLn $ "Errors : " <> show errors+        handler (Recv l) = liftIO $ read <$> readChan (chans ! l)++    api :: Proxy API+    api = Proxy++    send :: LocTm -> String -> ClientM NoContent+    send = client api++    server :: RecvChans -> Server API+    server chans = handler+      where+        handler :: LocTm -> String -> Handler NoContent+        handler rmt msg = do+          liftIO $ writeChan (chans ! rmt) msg+          pure NoContent++    recvThread :: HttpConfig -> RecvChans -> IO ()+    recvThread cfg' chans = run (baseUrlPort $ locToUrl cfg' ! self) (serve api $ server chans)++instance Backend HttpConfig where+  runNetwork = runNetworkHttp
+ src/Choreography/Network/Local.hs view
@@ -0,0 +1,63 @@+-- | This module defines the multi-thread backend for the `Network` monad.+module Choreography.Network.Local where++import Choreography.Locations+import Choreography.Network+import Control.Concurrent+import Control.Monad+import Control.Monad.Freer+import Control.Monad.IO.Class+import Data.HashMap.Strict (HashMap, (!), (!?))+import Data.HashMap.Strict qualified as HashMap++-- | Each location is associated with a message buffer which stores messages sent+-- from other locations.+type MsgBuf = HashMap LocTm (Chan String)++-- | A backend for running choreographies using [Haskell threads](https://hackage.haskell.org/package/base/docs/Control-Concurrent.html)+--   as the locations and buffered `Control.Concurrent.Chan.Chan` channels for communication.+newtype LocalConfig = LocalConfig+  { locToBuf :: HashMap LocTm MsgBuf+  }++-- | Make a channel for each of the listed locations, on which messages from that location can be recieved.+newEmptyMsgBuf :: [LocTm] -> IO MsgBuf+newEmptyMsgBuf = foldM f HashMap.empty+  where+    f hash loc = do+      chan <- newChan+      pure (HashMap.insert loc chan hash)++-- | Make a local backend for the listed parties.+--   Make just the one backend and then have all your threads use the same one.+mkLocalConfig :: [LocTm] -> IO LocalConfig+mkLocalConfig ls = LocalConfig <$> foldM f HashMap.empty ls+  where+    f hash loc = do+      buf <- newEmptyMsgBuf ls+      pure (HashMap.insert loc buf hash)++-- | List the parties known to the backend.+locs :: LocalConfig -> [LocTm]+locs = HashMap.keys . locToBuf++-- | Run a `Network` behavior using the channels in a `LocalConfig` for communication.+--   Call this inside a concurrent thread.+runNetworkLocal :: (MonadIO m) => LocalConfig -> LocTm -> Network m a -> m a+runNetworkLocal cfg self = interpFreer handler+  where+    handler :: (MonadIO m) => NetworkSig m a -> m a+    handler (Run m) = m+    handler (Send a ls) = liftIO $ mapM_ (\l -> writeChan ((locToBuf cfg ! l) ! self) (show a)) ls+    handler (Recv l) = do+      let b = locToBuf cfg ! self+      let q = b !? l+      case q of+        Just q' -> liftIO $ read <$> readChan q'+        Nothing -> liftIO do+          print $ void b+          print l+          error $ "We don't know how to contact the party named \"" <> l <> "\"."++instance Backend LocalConfig where+  runNetwork = runNetworkLocal
+ src/Choreography/Polymorphism.hs view
@@ -0,0 +1,206 @@+-- | Types, functions, and structures for writing choreographies with variable numbers of participants.+module Choreography.Polymorphism where++import Choreography.Choreography+import Choreography.Choreography.Batteries ((*~>))+import Choreography.Core+import Choreography.Locations+import Control.Monad (void)+import Data.Foldable (toList)+import Data.Functor.Compose (Compose (Compose, getCompose))+import Data.Functor.Const (Const (Const, getConst))+import GHC.TypeLits++-- * The root abstraction++-- | A mapping, accessed by `Member` terms, from types (`Symbol`s) to values.+--   The types of the values depend on the indexing type; this relation is expressed by the type-level function @f@.+--   If the types of the values /don't/ depend on the index, use `Quire`.+--   If the types vary only in that they are `Located` at the indexing party, use `Faceted`.+--   `PIndexed` generalizes those two types in a way that's not usually necessary when writing choreographies.+newtype PIndexed ls f = PIndexed {pindex :: PIndex ls f}++-- | An impredicative quantified type. Wrapping it up in `PIndexed` wherever possible will avoid a lot of type errors and headache.+type PIndex ls f = forall l. (KnownSymbol l) => Member l ls -> f l++-- | Sequence computations indexed by parties.+--   Converts a `PIndexed` of computations into a computation yielding a `PIndexed`.+--   Strongly analogous to 'Data.Traversable.sequence'.+--   In most cases, the [choreographic functions](#g:choreographicfunctions) below will be easier to use+--   than messing around with `Data.Functor.Compose.Compose`.+sequenceP ::+  forall b (ls :: [LocTy]) m.+  (KnownSymbols ls, Monad m) =>+  PIndexed ls (Compose m b) ->+  m (PIndexed ls b)+sequenceP (PIndexed f) = case tySpine @ls of+  TyCons -> do+    b <- getCompose $ f First+    PIndexed fTail <- sequenceP (PIndexed $ f . Later)+    let retVal :: PIndex ls b+        retVal First = b+        retVal (Later ltr) = fTail ltr+    pure $ PIndexed retVal+  TyNil -> pure $ PIndexed \case {}++-- * A type-indexed vector type++-- | A collection of values, all of the same type, assigned to each element of the type-level list.+newtype Quire parties a = Quire {asPIndexed :: PIndexed parties (Const a)}++-- | Access a value in a `Quire` by its index.+getLeaf :: (KnownSymbol p) => Quire parties a -> Member p parties -> a+getLeaf (Quire (PIndexed q)) p = getConst $ q p++-- | Package a function as a `Quire`.+stackLeaves :: forall ps a. (forall p. (KnownSymbol p) => Member p ps -> a) -> Quire ps a+stackLeaves f = Quire . PIndexed $ Const . f++-- | Get the head item from a `Quire`.+qHead :: (KnownSymbol p) => Quire (p ': ps) a -> a+qHead (Quire (PIndexed f)) = getConst $ f First++-- | Get the tail of a `Quire`.+qTail :: Quire (p ': ps) a -> Quire ps a+qTail (Quire (PIndexed f)) = Quire . PIndexed $ f . Later++-- | Prepend a value to a `Quire`.+--   The corresponding `Symbol` to bind it to must be provided by type-application if it can't be infered.+qCons :: forall p ps a. a -> Quire ps a -> Quire (p ': ps) a+qCons a (Quire (PIndexed f)) = Quire . PIndexed $ \case+  First -> Const a+  Later mps -> f mps++-- | An empty `Quire`.+qNil :: Quire '[] a+qNil = Quire $ PIndexed \case {}++-- | Apply a function to a single item in a `Quire`.+qModify :: forall p ps a. (KnownSymbol p, KnownSymbols ps) => Member p ps -> (a -> a) -> Quire ps a -> Quire ps a+qModify First f q = f (qHead q) `qCons` qTail q+qModify (Later m) f q = case tySpine @ps of TyCons -> qHead q `qCons` qModify m f (qTail q)++instance forall parties. (KnownSymbols parties) => Functor (Quire parties) where+  fmap f q = case tySpine @parties of+    TyCons -> f (qHead q) `qCons` fmap f (qTail q)+    TyNil -> qNil++instance forall parties. (KnownSymbols parties) => Applicative (Quire parties) where+  pure a = Quire . PIndexed $ const (Const a)+  qf <*> qa = case tySpine @parties of+    TyCons -> qHead qf (qHead qa) `qCons` (qTail qf <*> qTail qa)+    TyNil -> qNil++instance forall parties. (KnownSymbols parties) => Foldable (Quire parties) where+  foldMap f q = case tySpine @parties of+    TyCons -> f (qHead q) <> foldMap f (qTail q)+    TyNil -> mempty++instance forall parties. (KnownSymbols parties) => Traversable (Quire parties) where+  sequenceA q = case tySpine @parties of+    TyCons -> qCons <$> qHead q <*> sequenceA (qTail q)+    TyNil -> pure qNil++instance forall parties a. (KnownSymbols parties, Eq a) => Eq (Quire parties a) where+  q1 == q2 = and $ (==) <$> q1 <*> q2++instance forall parties a. (KnownSymbols parties, Show a) => Show (Quire parties a) where+  show q = show $ toLocs (refl @parties) `zip` toList q++-- Many more instances are possible...++-- * Non-congruent parallel located values++-- | A unified representation of possibly-distinct homogeneous values owned by many parties.+type Faceted parties common a = PIndexed parties (Facet a common)++-- | Repackages `Located` with the type arguments correctly arranged for use with `PIndexed`.+newtype Facet a common p = Facet {getFacet :: Located (p ': common) a}++-- | Get a `Located` value of a `Faceted` at a given location.+localize :: (KnownSymbol l) => Member l ls -> Faceted ls common a -> Located (l ': common) a+localize l (PIndexed f) = getFacet $ f l++-- | In a context where unwrapping located values is possible, get the respective value stored in a `Faceted`.+viewFacet :: (KnownSymbol l) => Unwrap l -> Member l ls -> Faceted ls common a -> a+viewFacet un l = un First . localize l++{-+unsafeFacet :: [Maybe a] -> Member l ls -> Facet a common l -- providing this as a helper function is pretty sketchy, if we don't need it delete it.+unsafeFacet (Just a : _) First = Facet $ wrap a+unsafeFacet (Nothing : _) First = Empty+unsafeFacet (_ : as) (Later l) = unsafeFacet as l+unsafeFacet [] _ = error "The provided list isn't long enough to use as a Faceted over the intended parties."+-}++-- * #choreographicfunctions# Choreographic functions++-- | Perform a local computation at all of a list of parties, yielding a `Faceted`.+parallel ::+  forall ls a ps m.+  (KnownSymbols ls) =>+  -- | The parties who will do the computation must be present in the census.+  Subset ls ps ->+  -- | The local computation has access to the identity of the party in question,+  --   in additon to the usual unwrapper function.+  (forall l. (KnownSymbol l) => Member l ls -> Unwrap l -> m a) -> -- Could promote this to PIndexed too, but ergonomics might be worse?+  Choreo ps m (Faceted ls '[] a)+parallel ls m = fanOut \mls -> locally (inSuper ls mls) (m mls)++-- | Perform a local computation at all of a list of parties, yielding nothing.+parallel_ ::+  forall ls ps m.+  (KnownSymbols ls) =>+  Subset ls ps ->+  (forall l. (KnownSymbol l) => Member l ls -> Unwrap l -> m ()) ->+  Choreo ps m ()+parallel_ ls m = void $ parallel ls m++-- | Perform a local computation, that doesn't use any existing `Located` values and doesn't depend on the respective party's identity,+--   at all of a list of parties, yielding a `Faceted`.+_parallel :: forall ls a ps m. (KnownSymbols ls) => Subset ls ps -> m a -> Choreo ps m (Faceted ls '[] a)+_parallel ls m = parallel ls \_ _ -> m++-- | Perform a given choreography for each of several parties, giving each of them a return value that form a new `Faceted`.+fanOut ::+  (KnownSymbols qs) =>+  -- | The body.  -- kinda sketchy that rs might not be a subset of ps...+  (forall q. (KnownSymbol q) => Member q qs -> Choreo ps m (Located (q ': rs) a)) ->+  Choreo ps m (Faceted qs rs a)+fanOut body = sequenceP (PIndexed $ Compose . (Facet <$>) <$> body)++-- | Perform a given choreography for each of several parties; the return values are known to recipients but not necessarily to the loop-parties.+fanIn ::+  (KnownSymbols qs, KnownSymbols rs) =>+  -- | The recipients.+  Subset rs ps ->+  -- | The body.+  (forall q. (KnownSymbol q) => Member q qs -> Choreo ps m (Located rs a)) ->+  Choreo ps m (Located rs (Quire qs a))+fanIn rs body = do+  (PIndexed x) <- sequenceP (PIndexed $ Compose . (Const <$>) <$> body)+  rs `congruently` \un -> stackLeaves $ \q -> un refl (getConst $ x q)++-- | The owner of a `Quire` sends its elements to their respective parties, resulting in a `Faceted`.+--   This represents the "scatter" idea common in parallel computing contexts.+scatter ::+  forall census sender recipients a m.+  (KnownSymbol sender, KnownSymbols recipients, Show a, Read a) =>+  Member sender census ->+  Subset recipients census ->+  Located '[sender] (Quire recipients a) ->+  Choreo census m (Faceted recipients '[sender] a)+scatter sender recipients values = fanOut \r ->+  (sender, \un -> un First values `getLeaf` r) *~> inSuper recipients r @@ sender @@ nobody++-- | The many owners of a `Faceted` each send their respective values to a constant list of recipients, resulting in a `Quire`.+--   This represents the "gather" idea common in parallel computing contexts.+gather ::+  forall census recipients senders a dontcare m.+  (KnownSymbols senders, KnownSymbols recipients, Show a, Read a) =>+  Subset senders census ->+  Subset recipients census ->+  Faceted senders dontcare a ->+  Choreo census m (Located recipients (Quire senders a)) -- could be Faceted senders recipients instead...+gather senders recipients (PIndexed values) = fanIn recipients \s ->+  (inSuper senders s, getFacet $ values s) ~> recipients
+ src/Control/Monad/Freer.hs view
@@ -0,0 +1,46 @@+-- | This module defines the freer monad `Freer`, which allows manipulating+--   effectful computations algebraically.+--+--   It is unlikely you need this, except maybe to define your own backends or something.+--   We may hide/remove it in future versions.+module Control.Monad.Freer where++import Control.Monad ((>=>))++-- | Freer monads.+--+-- A freer monad @Freer f a@ represents an effectful computation that returns a+-- value of type @a@. The parameter @f :: * -> *@ is a effect signature that+-- defines the effectful operations allowed in the computation. @Freer f a@ is+-- called a freer monad in that it's a `Monad` given any @f@.+data Freer f a where+  -- | A pure computation.+  Return :: a -> Freer f a+  -- | An effectful computation where the first argument @f b@ is the effect+  -- to perform and returns a result of type @b@; the second argument+  -- @b -> Freer f a@ is a continuation that specifies the rest of the+  -- computation given the result of the performed effect.+  Do :: f b -> (b -> Freer f a) -> Freer f a++instance Functor (Freer f) where+  fmap f (Return a) = Return (f a)+  fmap f (Do eff k) = Do eff (fmap f . k)++instance Applicative (Freer f) where+  pure = Return++  (Return f) <*> a = fmap f a+  (Do eff k) <*> a = Do eff $ (<*> a) . k++instance Monad (Freer f) where+  (Return a) >>= f = f a+  (Do eff k) >>= f = Do eff (k >=> f)++-- | Lift an effect into the freer monad.+toFreer :: f a -> Freer f a+toFreer eff = Do eff Return++-- | Interpret the effects in a freer monad in terms of another monad.+interpFreer :: (Monad m) => (forall b. f b -> m b) -> Freer f a -> m a+interpFreer _ (Return a) = pure a+interpFreer handler (Do eff k) = handler eff >>= interpFreer handler . k