cloudchor (empty) → 0.1.0.0

raw patch · 35 files changed

+3549/−0 lines, 35 filesdep +asyncdep +basedep +cloudchor

Dependencies added: async, base, cloudchor, containers, http-client, mtl, random, servant, servant-client, servant-server, sop-core, split, template-haskell, time, transformers, unordered-containers, warp

Files

LICENSE-HasChor.txt +32/−0
LICENSE.txt +373/−0
README.md +21/−0
bench/Benchmark.hs +73/−0
bench/Choreos/Bookseller.hs +54/−0
bench/Choreos/CleanRoom.hs +160/−0
bench/Choreos/Kvs.hs +102/−0
bench/Main.hs +22/−0
cloudchor.cabal +290/−0
examples/HasChor/bank-2pc/Main.hs +105/−0
examples/HasChor/bookseller-0-network/Main.hs +55/−0
examples/HasChor/bookseller-1-simple/Main.hs +97/−0
examples/HasChor/bookseller-2-higher-order/Main.hs +93/−0
examples/HasChor/bookseller-3-loc-poly/Main.hs +69/−0
examples/HasChor/diffiehellman/Main.hs +91/−0
examples/HasChor/karatsuba/Main.hs +93/−0
examples/HasChor/kvs-1-simple/Main.hs +103/−0
examples/HasChor/kvs-2-primary-backup/Main.hs +125/−0
examples/HasChor/kvs-3-higher-order/Main.hs +156/−0
examples/HasChor/kvs-4-loc-poly/Main.hs +196/−0
examples/HasChor/mergesort/Main.hs +118/−0
examples/HasChor/playground/Main.hs +31/−0
examples/HasChor/quicksort/Main.hs +56/−0
examples/HasChor/ring-leader/Main.hs +82/−0
examples/clean-room/Main.hs +170/−0
examples/unsoundness/Main.hs +102/−0
src/Choreography.hs +43/−0
src/Choreography/Choreo.hs +190/−0
src/Choreography/Location.hs +44/−0
src/Choreography/Location/Multi.hs +79/−0
src/Choreography/Network.hs +61/−0
src/Choreography/Network/Http.hs +112/−0
src/Choreography/Network/Local.hs +51/−0
src/Choreography/Network/LocalMsgCount.hs +57/−0
src/Control/Monad/Freer.hs +43/−0

+ LICENSE-HasChor.txt view

@@ -0,0 +1,32 @@+MIT License++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.

+ LICENSE.txt view

@@ -0,0 +1,373 @@+Mozilla Public License Version 2.0+==================================++1. Definitions+--------------++1.1. "Contributor"+    means each individual or legal entity that creates, contributes to+    the creation of, or owns Covered Software.++1.2. "Contributor Version"+    means the combination of the Contributions of others (if any) used+    by a Contributor and that particular Contributor's Contribution.++1.3. "Contribution"+    means Covered Software of a particular Contributor.++1.4. "Covered Software"+    means Source Code Form to which the initial Contributor has attached+    the notice in Exhibit A, the Executable Form of such Source Code+    Form, and Modifications of such Source Code Form, in each case+    including portions thereof.++1.5. "Incompatible With Secondary Licenses"+    means++    (a) that the initial Contributor has attached the notice described+        in Exhibit B to the Covered Software; or++    (b) that the Covered Software was made available under the terms of+        version 1.1 or earlier of the License, but not also under the+        terms of a Secondary License.++1.6. "Executable Form"+    means any form of the work other than Source Code Form.++1.7. "Larger Work"+    means a work that combines Covered Software with other material, in+    a separate file or files, that is not Covered Software.++1.8. "License"+    means this document.++1.9. "Licensable"+    means having the right to grant, to the maximum extent possible,+    whether at the time of the initial grant or subsequently, any and+    all of the rights conveyed by this License.++1.10. "Modifications"+    means any of the following:++    (a) any file in Source Code Form that results from an addition to,+        deletion from, or modification of the contents of Covered+        Software; or++    (b) any new file in Source Code Form that contains any Covered+        Software.++1.11. "Patent Claims" of a Contributor+    means any patent claim(s), including without limitation, method,+    process, and apparatus claims, in any patent Licensable by such+    Contributor that would be infringed, but for the grant of the+    License, by the making, using, selling, offering for sale, having+    made, import, or transfer of either its Contributions or its+    Contributor Version.++1.12. "Secondary License"+    means either the GNU General Public License, Version 2.0, the GNU+    Lesser General Public License, Version 2.1, the GNU Affero General+    Public License, Version 3.0, or any later versions of those+    licenses.++1.13. "Source Code Form"+    means the form of the work preferred for making modifications.++1.14. "You" (or "Your")+    means an individual or a legal entity exercising rights under this+    License. For legal entities, "You" includes any entity that+    controls, is controlled by, or is under common control with You. For+    purposes of this definition, "control" means (a) the power, direct+    or indirect, to cause the direction or management of such entity,+    whether by contract or otherwise, or (b) ownership of more than+    fifty percent (50%) of the outstanding shares or beneficial+    ownership of such entity.++2. License Grants and Conditions+--------------------------------++2.1. Grants++Each Contributor hereby grants You a world-wide, royalty-free,+non-exclusive license:++(a) under intellectual property rights (other than patent or trademark)+    Licensable by such Contributor to use, reproduce, make available,+    modify, display, perform, distribute, and otherwise exploit its+    Contributions, either on an unmodified basis, with Modifications, or+    as part of a Larger Work; and++(b) under Patent Claims of such Contributor to make, use, sell, offer+    for sale, have made, import, and otherwise transfer either its+    Contributions or its Contributor Version.++2.2. Effective Date++The licenses granted in Section 2.1 with respect to any Contribution+become effective for each Contribution on the date the Contributor first+distributes such Contribution.++2.3. Limitations on Grant Scope++The licenses granted in this Section 2 are the only rights granted under+this License. No additional rights or licenses will be implied from the+distribution or licensing of Covered Software under this License.+Notwithstanding Section 2.1(b) above, no patent license is granted by a+Contributor:++(a) for any code that a Contributor has removed from Covered Software;+    or++(b) for infringements caused by: (i) Your and any other third party's+    modifications of Covered Software, or (ii) the combination of its+    Contributions with other software (except as part of its Contributor+    Version); or++(c) under Patent Claims infringed by Covered Software in the absence of+    its Contributions.++This License does not grant any rights in the trademarks, service marks,+or logos of any Contributor (except as may be necessary to comply with+the notice requirements in Section 3.4).++2.4. Subsequent Licenses++No Contributor makes additional grants as a result of Your choice to+distribute the Covered Software under a subsequent version of this+License (see Section 10.2) or under the terms of a Secondary License (if+permitted under the terms of Section 3.3).++2.5. Representation++Each Contributor represents that the Contributor believes its+Contributions are its original creation(s) or it has sufficient rights+to grant the rights to its Contributions conveyed by this License.++2.6. Fair Use++This License is not intended to limit any rights You have under+applicable copyright doctrines of fair use, fair dealing, or other+equivalents.++2.7. Conditions++Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted+in Section 2.1.++3. Responsibilities+-------------------++3.1. Distribution of Source Form++All distribution of Covered Software in Source Code Form, including any+Modifications that You create or to which You contribute, must be under+the terms of this License. You must inform recipients that the Source+Code Form of the Covered Software is governed by the terms of this+License, and how they can obtain a copy of this License. You may not+attempt to alter or restrict the recipients' rights in the Source Code+Form.++3.2. Distribution of Executable Form++If You distribute Covered Software in Executable Form then:++(a) such Covered Software must also be made available in Source Code+    Form, as described in Section 3.1, and You must inform recipients of+    the Executable Form how they can obtain a copy of such Source Code+    Form by reasonable means in a timely manner, at a charge no more+    than the cost of distribution to the recipient; and++(b) You may distribute such Executable Form under the terms of this+    License, or sublicense it under different terms, provided that the+    license for the Executable Form does not attempt to limit or alter+    the recipients' rights in the Source Code Form under this License.++3.3. Distribution of a Larger Work++You may create and distribute a Larger Work under terms of Your choice,+provided that You also comply with the requirements of this License for+the Covered Software. If the Larger Work is a combination of Covered+Software with a work governed by one or more Secondary Licenses, and the+Covered Software is not Incompatible With Secondary Licenses, this+License permits You to additionally distribute such Covered Software+under the terms of such Secondary License(s), so that the recipient of+the Larger Work may, at their option, further distribute the Covered+Software under the terms of either this License or such Secondary+License(s).++3.4. Notices++You may not remove or alter the substance of any license notices+(including copyright notices, patent notices, disclaimers of warranty,+or limitations of liability) contained within the Source Code Form of+the Covered Software, except that You may alter any license notices to+the extent required to remedy known factual inaccuracies.++3.5. Application of Additional Terms++You may choose to offer, and to charge a fee for, warranty, support,+indemnity or liability obligations to one or more recipients of Covered+Software. However, You may do so only on Your own behalf, and not on+behalf of any Contributor. You must make it absolutely clear that any+such warranty, support, indemnity, or liability obligation is offered by+You alone, and You hereby agree to indemnify every Contributor for any+liability incurred by such Contributor as a result of warranty, support,+indemnity or liability terms You offer. You may include additional+disclaimers of warranty and limitations of liability specific to any+jurisdiction.++4. Inability to Comply Due to Statute or Regulation+---------------------------------------------------++If it is impossible for You to comply with any of the terms of this+License with respect to some or all of the Covered Software due to+statute, judicial order, or regulation then You must: (a) comply with+the terms of this License to the maximum extent possible; and (b)+describe the limitations and the code they affect. Such description must+be placed in a text file included with all distributions of the Covered+Software under this License. Except to the extent prohibited by statute+or regulation, such description must be sufficiently detailed for a+recipient of ordinary skill to be able to understand it.++5. Termination+--------------++5.1. The rights granted under this License will terminate automatically+if You fail to comply with any of its terms. However, if You become+compliant, then the rights granted under this License from a particular+Contributor are reinstated (a) provisionally, unless and until such+Contributor explicitly and finally terminates Your grants, and (b) on an+ongoing basis, if such Contributor fails to notify You of the+non-compliance by some reasonable means prior to 60 days after You have+come back into compliance. Moreover, Your grants from a particular+Contributor are reinstated on an ongoing basis if such Contributor+notifies You of the non-compliance by some reasonable means, this is the+first time You have received notice of non-compliance with this License+from such Contributor, and You become compliant prior to 30 days after+Your receipt of the notice.++5.2. If You initiate litigation against any entity by asserting a patent+infringement claim (excluding declaratory judgment actions,+counter-claims, and cross-claims) alleging that a Contributor Version+directly or indirectly infringes any patent, then the rights granted to+You by any and all Contributors for the Covered Software under Section+2.1 of this License shall terminate.++5.3. In the event of termination under Sections 5.1 or 5.2 above, all+end user license agreements (excluding distributors and resellers) which+have been validly granted by You or Your distributors under this License+prior to termination shall survive termination.++************************************************************************+*                                                                      *+*  6. Disclaimer of Warranty                                           *+*  -------------------------                                           *+*                                                                      *+*  Covered Software is provided under this License on an "as is"       *+*  basis, without warranty of any kind, either expressed, implied, or  *+*  statutory, including, without limitation, warranties that the       *+*  Covered Software is free of defects, merchantable, fit for a        *+*  particular purpose or non-infringing. The entire risk as to the     *+*  quality and performance of the Covered Software is with You.        *+*  Should any Covered Software prove defective in any respect, You     *+*  (not any Contributor) assume the cost of any necessary servicing,   *+*  repair, or correction. This disclaimer of warranty constitutes an   *+*  essential part of this License. No use of any Covered Software is   *+*  authorized under this License except under this disclaimer.         *+*                                                                      *+************************************************************************++************************************************************************+*                                                                      *+*  7. Limitation of Liability                                          *+*  --------------------------                                          *+*                                                                      *+*  Under no circumstances and under no legal theory, whether tort      *+*  (including negligence), contract, or otherwise, shall any           *+*  Contributor, or anyone who distributes Covered Software as          *+*  permitted above, be liable to You for any direct, indirect,         *+*  special, incidental, or consequential damages of any character      *+*  including, without limitation, damages for lost profits, loss of    *+*  goodwill, work stoppage, computer failure or malfunction, or any    *+*  and all other commercial damages or losses, even if such party      *+*  shall have been informed of the possibility of such damages. This   *+*  limitation of liability shall not apply to liability for death or   *+*  personal injury resulting from such party's negligence to the       *+*  extent applicable law prohibits such limitation. Some               *+*  jurisdictions do not allow the exclusion or limitation of           *+*  incidental or consequential damages, so this exclusion and          *+*  limitation may not apply to You.                                    *+*                                                                      *+************************************************************************++8. Litigation+-------------++Any litigation relating to this License may be brought only in the+courts of a jurisdiction where the defendant maintains its principal+place of business and such litigation shall be governed by laws of that+jurisdiction, without reference to its conflict-of-law provisions.+Nothing in this Section shall prevent a party's ability to bring+cross-claims or counter-claims.++9. Miscellaneous+----------------++This License represents the complete agreement concerning the subject+matter hereof. If any provision of this License is held to be+unenforceable, such provision shall be reformed only to the extent+necessary to make it enforceable. Any law or regulation which provides+that the language of a contract shall be construed against the drafter+shall not be used to construe this License against a Contributor.++10. Versions of the License+---------------------------++10.1. New Versions++Mozilla Foundation is the license steward. Except as provided in Section+10.3, no one other than the license steward has the right to modify or+publish new versions of this License. Each version will be given a+distinguishing version number.++10.2. Effect of New Versions++You may distribute the Covered Software under the terms of the version+of the License under which You originally received the Covered Software,+or under the terms of any subsequent version published by the license+steward.++10.3. Modified Versions++If you create software not governed by this License, and you want to+create a new license for such software, you may create and use a+modified version of this License if you rename the license and remove+any references to the name of the license steward (except to note that+such modified license differs from this License).++10.4. Distributing Source Code Form that is Incompatible With Secondary+Licenses++If You choose to distribute Source Code Form that is Incompatible With+Secondary Licenses under the terms of this version of the License, the+notice described in Exhibit B of this License must be attached.++Exhibit A - Source Code Form License Notice+-------------------------------------------++  This Source Code Form is subject to the terms of the Mozilla Public+  License, v. 2.0. If a copy of the MPL was not distributed with this+  file, You can obtain one at https://mozilla.org/MPL/2.0/.++If it is not possible or desirable to put the notice in a particular+file, then You may include the notice in a location (such as a LICENSE+file in a relevant directory) where a recipient would be likely to look+for such a notice.++You may add additional accurate notices of copyright ownership.++Exhibit B - "Incompatible With Secondary Licenses" Notice+---------------------------------------------------------++  This Source Code Form is "Incompatible With Secondary Licenses", as+  defined by the Mozilla Public License, v. 2.0.

+ README.md view

@@ -0,0 +1,21 @@+# CloudChor++CloudChor is a Haskell library for lighweight and efficient choreographic programming with multiply-located values.+It is an extension of the [HasChor](https://github.com/gshen42/HasChor) library.++For more details, see the PEPM '26 paper: [Towards Lightweight and Efficient Choreographic Cloud Services](https://doi.org/10.1145/3779209.3779537).++## Repository structure++* [`src/`](src/) contains the source code of the library.+  * [`Choreography.Location.Multi`](src/Choreography/Location/Multi.hs) is the module that implements multiply-located values.+* [`examples/`](examples/) includes example programs using the library.+  * [`clean-room`](examples/clean-room/): An implementation of a data clean room protocol as a choreography.+  * [`unsoundness`](examples/unsoundness): Two counter-examples showing how unrestricted IO can lead to unsoundness.+  * [`HasChor`](examples/HasChor): The original examples from the HasChor repository.+* [`bench/`](bench/) contains the setup for running benchmarks to compare `cond` vs. `cond_`.++## License++This repository is provided under the terms of the [Mozilla Public License 2.0](LICENSE.txt).+It is based on HasChor, which is provided under the [MIT License](LICENSE-HasChor.txt).

+ bench/Benchmark.hs view

@@ -0,0 +1,73 @@+{-# LANGUAGE BlockArguments     #-}+{-# LANGUAGE ParallelListComp   #-}+{-# LANGUAGE ImpredicativeTypes #-}++module Benchmark where++import Control.Concurrent+import Control.Monad(when)+import Data.Foldable(for_)+import Data.IORef+import Data.Proxy(Proxy(..))+import Data.Time+import Data.Traversable(for)+import GHC.TypeLits(KnownSymbol)++import Choreography hiding (cond, cond', cond_, cond_')+import Choreography qualified as C+import Choreography.Choreo+import Choreography.Network+import Choreography.Network.Local+import Choreography.Network.LocalMsgCount++-- Benchmarking infrastructure++-- The type of the `cond_'` function, to avoid writing it out multiple times.+-- NB: This is a more specific version of the original `cond'` function's type.+type Cond_' =+  forall m l a b+  . (Bounded a, Enum a, Show a, Read a, KnownSymbol l)+  => (Proxy l, Unwrap l -> m a)+  -> (a -> Choreo m (b @ l))+  -> Choreo m (b @ l)++httpConfig :: [LocTm] -> HttpConfig+httpConfig ls = mkHttpConfig [(l, ("localhost", port)) | l <- ls | port <- [3000..]]++data SomeBackend = forall b. Backend b => SomeBackend b++runWithBackend :: SomeBackend -> Choreo IO () -> LocTm -> IO ()+runWithBackend (SomeBackend b) = runChoreography b++mkBackendConfig :: String -> IORef Int -> [LocTm] -> IO SomeBackend+mkBackendConfig "http"  _ = pure . SomeBackend . httpConfig+mkBackendConfig "local" _ = fmap SomeBackend . mkLocalConfig+mkBackendConfig "count" msgCounter = fmap SomeBackend . mkLocalMsgCountConfig msgCounter+mkBackendConfig _ _ = error "Invalid backend"++timed :: IO () -> IO ()+timed io = do+  before <- getCurrentTime+  io+  after <- getCurrentTime+  print $ diffUTCTime after before++-- Run a choreography with both the original `cond'` and the non-broadcasting `cond_'` and report their execution time.+benchmarkChoreography :: String -> String -> [LocTm] -> (Cond_' -> Choreo IO ()) -> IO ()+benchmarkChoreography backend cond locs choreo = do+  let chor = choreo $ if cond == "full" then C.cond' else C.cond_'+  msgCounter <- newIORef 0+  someCfg <- mkBackendConfig backend msgCounter locs++  timed do+    mvars <- for locs \l -> do+      mvar <- newEmptyMVar++      forkFinally (runWithBackend someCfg chor l) \_ -> putMVar mvar ()+      pure mvar++    for_ mvars takeMVar++  when (backend == "count") do+    count <- readIORef msgCounter+    putStrLn $ "Sends: " <> show count

+ bench/Choreos/Bookseller.hs view

@@ -0,0 +1,54 @@+{-# LANGUAGE BlockArguments     #-}+{-# LANGUAGE DataKinds          #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase         #-}++-- This is a version of the `bookseller-1-simple` choreography, adapted for the benchmarking setup.+module Choreos.Bookseller where++import Data.Proxy+import Data.Time++import Benchmark+import Choreography hiding (cond, cond_, cond', cond_')++buyer :: Proxy "buyer"+buyer = Proxy++seller :: Proxy "seller"+seller = Proxy++-- `bookseller'` is a simplified version of `bookseller` that utilizes `~~>`+bookseller' :: Cond_' -> Choreo IO ()+bookseller' cond_' = do+  title <- (buyer, \_ -> pure "Types and Programming Languages") ~~> seller++  price <- (seller, \un -> return $ priceOf (un title)) ~~> buyer++  cond_' (buyer, \un -> return $ (un price) < budget) \case+    True  -> do+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un title)) ~~> buyer++      buyer `locally` \un -> do+        -- putStrLn $ "The book will be delivered on " ++ show (un deliveryDate)+        return $ Just (un deliveryDate)++    False -> do+      buyer `locally` \_ -> do+        -- putStrLn "The book's price is out of the budget"+        return Nothing++  pure ()++budget :: Int+budget = 100++priceOf :: String -> Int+priceOf "Types and Programming Languages" = 80+priceOf "Homotopy Type Theory"            = 120+priceOf _                                 = error "Unknown book"++deliveryDateOf :: String -> Day+deliveryDateOf "Types and Programming Languages" = fromGregorian 2022 12 19+deliveryDateOf "Homotopy Type Theory"            = fromGregorian 2023 01 01+deliveryDateOf _                                 = error "Unknown book"

+ bench/Choreos/CleanRoom.hs view

@@ -0,0 +1,160 @@+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++{-# LANGUAGE BlockArguments     #-}+{-# LANGUAGE DataKinds          #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GADTs              #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase         #-}++-- This is a version of the `clean-room` choreography, adapted for the benchmarking setup.+module Choreos.CleanRoom where++import Data.Function((&))+import Data.Proxy(Proxy(..))+import Data.SOP.BasicFunctors(mapKK, K (..))+import Data.SOP.Classes(HCollapse(..), hmap, hsequenceK)+import Data.SOP.Constraint(All)+import Data.SOP.NP(NP(..))+import GHC.TypeLits(KnownSymbol, SSymbol, withKnownSymbol, withSomeSSymbol)++import Benchmark+import Choreography hiding (cond, cond_, cond', cond_')+import Choreography.Location+import Choreography.Location.Multi++-- Schema and dataset handling (stubbed out)++data Schema = Schema+  deriving stock (Show, Read)++data Dataset = Dataset+  deriving stock (Show, Read)++data Query = Query+  deriving stock (Show, Read)++loadSchema :: KnownSymbol l => Proxy l -> IO Schema+loadSchema _ = pure Schema++mergeSchemas :: [Schema] -> Schema+mergeSchemas _ = Schema++conformsToSchema :: Schema -> Dataset -> IO Bool+conformsToSchema _ _ = pure True++emptyDataset :: Dataset+emptyDataset = Dataset++-- Simulate some I/O to load a dataset (e.g. from a file)+loadDataset :: KnownSymbol l => Proxy l -> IO Dataset+loadDataset _ = pure Dataset++mergeDatasets :: [Dataset] -> Dataset+mergeDatasets _ = Dataset++loadQuery :: KnownSymbol l => Proxy l -> Schema -> IO Query+loadQuery _ _ = pure Query++agreeWithQueries :: KnownSymbol l => Proxy l -> [Query] -> IO Bool+agreeWithQueries _ _ = pure True++runQuery :: Dataset -> Query -> IO Int+runQuery _ _ = pure 0++-- Error-handling (if datasets don't conform to schema)++getClientDataset :: (KnownSymbol server, KnownSymbol client) => Cond_' -> Int -> Int -> Schema @ server -> Proxy server -> Proxy client -> Choreo IO (Dataset @ server)+getClientDataset cond_' failures tries schema server client =+  if tries <= 0 then+    pure $ wrap emptyDataset+  else do+    dataset <- (client, \_ -> loadDataset client) ~~> server+    cond_'+      (server, \unwrap ->+        if failures > 0 then+          pure False -- Simulate a fixed number of failures for each client+        else+          conformsToSchema (unwrap schema) (unwrap dataset)+      )+      \case+        True -> pure dataset+        False -> getClientDataset cond_' (failures - 1) (tries - 1) schema server client++getClientDatasets :: (KnownSymbol server, All KnownSymbol clients) => Cond_' -> Int -> Int -> Schema @ server -> Proxy server -> NP Proxy clients -> Choreo IO (NP (K Dataset) clients @ server)+getClientDatasets _ _ _ _ _ Nil = pure $ wrap Nil+getClientDatasets cond_' failures tries schema server (client :* clients) = do+  dataset <- getClientDataset cond_' failures tries schema server client+  datasets <- getClientDatasets cond_' failures tries schema server clients+  locally server \unwrap -> pure $ K (unwrap dataset) :* unwrap datasets++-- Main choreography++cleanRoom :: (KnownSymbol server, All KnownSymbol clients) => Cond_' -> Int -> Proxy server -> NP Proxy clients -> Choreo IO ()+cleanRoom cond_' failures server clients = do+  -- Every client loads their data schema and sends it to the server+  schemas <- (clients, \c _ -> loadSchema c) *~~> server++  -- Server merges the schemas+  finalSchemaS <- locally server \unwrap -> pure $ mergeSchemas $ hcollapse $ unwrap schemas++  -- Server broadcasts the final schema+  finalSchema <- (server, finalSchemaS) ~>* clients++  -- Based on the final schema, each client computes what query it wants to run, and sends it back to the server+  queriesS <- (clients, \c unwrap -> loadQuery c $ unwrap finalSchema) *~~> server++  -- Server broadcasts the list of queries to all clients+  queries <- (server, \unwrap -> pure $ hcollapse $ unwrap queriesS) ~~>* clients++  -- Each client locally decides if they agree with everyone else's queries, and sends back a response+  agreements <- (clients, \c unwrap -> agreeWithQueries c $ unwrap queries) *~~> server++  -- Server branches on the responses+  cond_' (server, \unwrap -> pure $ and $ hcollapse $ unwrap agreements) \case+    False -> do -- Someone disagrees, end the protocol+      multilocally clients \_ _ -> pure () -- print "Disagreement"+      pure $ wrap ()+    True -> do -- Everyone agrees, proceed+      -- The amount of times the server will ask for a valid dataset+      let tries = 5++      -- Clients send their datasets to the server+      datasets <- getClientDatasets cond_' failures tries finalSchemaS server clients++      -- Server locally merges the datasets and runs all the queries+      resultsS <- locally server \unwrap -> do+        let aggregatedDataset = mergeDatasets $ hcollapse $ unwrap datasets+        hsequenceK $ hmap (mapKK $ runQuery aggregatedDataset) $ unwrap queriesS++      -- Server sends the result of each query "pointwise"+      results <- (server, resultsS) ~>. clients++      -- Clients consume the received query results+      multilocally clients \_ unwrap -> pure $ unwrap results+      pure $ wrap ()++  pure ()++-- Instantiating the choreography++withProxy :: String -> (forall s. KnownSymbol s => Proxy s -> a) -> a+withProxy s f = withSomeSSymbol s \(ss :: SSymbol s) -> withKnownSymbol ss $ f @s Proxy++withProxies :: [String] -> (forall ss. All KnownSymbol ss => NP Proxy ss -> a) -> a+withProxies [] f = f Nil+withProxies (s : ss) f =+  withProxy s \s ->+    withProxies ss \ss ->+      f $ s :* ss++cleanRoomLocs :: Int -> [LocTm]+cleanRoomLocs numClients = server : clients+  where+    server = "s"+    clients = fmap (\i -> "c" <> show i) [1..numClients]++mkCleanRoom :: Int -> [LocTm] -> Cond_' -> Choreo IO ()+mkCleanRoom numFailures (server : clients) cond_' =+  cleanRoom cond_' numFailures & withProxy server & withProxies clients+mkCleanRoom _ [] _ = error "Empty locs"

+ bench/Choreos/Kvs.hs view

@@ -0,0 +1,102 @@+{-# LANGUAGE BlockArguments      #-}+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE DerivingStrategies  #-}+{-# LANGUAGE ImpredicativeTypes  #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- This is a version of the `kvs-2-primary-backup` choreography, adapted for the benchmarking setup.+module Choreos.Kvs where++import Data.Foldable(for_)+import Data.IORef+import Data.Map (Map)+import Data.Map qualified as Map+import Data.Proxy++import Benchmark+import Choreography hiding (cond, cond_, cond', cond_')+import Choreography.Location(wrap)++client :: Proxy "client"+client = Proxy++primary :: Proxy "primary"+primary = Proxy++backup :: Proxy "backup"+backup = Proxy++type State = Map String String++data Request = Put String String | Get String deriving stock (Show, Read)++isPutRequest :: Request -> Bool+isPutRequest (Put _ _) = True+isPutRequest _ = False++requests :: [Request]+requests =+  [ Put "x" "a"+  , Put "y" "b"+  , Get "x"+  , Put "y" "c"+  , Get "y"+  ]++type Response = Maybe String++-- | `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 ::+  Cond_' ->+  Request @ "client" ->+  IORef State @ "primary" ->+  IORef State @ "backup" ->+  Choreo IO (Response @ "client")+kvs cond_' request primaryStateRef backupStateRef = do+  -- send request to the primary node+  request' <- (client, request) ~> primary++  -- branch on the request+  cond_' (primary, \unwrap -> pure $ isPutRequest $ unwrap request') \case+    -- if the request is a `PUT`, forward the request to the backup node+    True -> do+      request'' <- (primary, request') ~> backup+      ack <-+        backup `locally` \unwrap -> do+          handleRequest (unwrap request'') (unwrap backupStateRef)+      (backup, ack) ~> primary+      return $ wrap ()+    _ -> do+      return $ wrap ()++  -- process request on the primary node+  response <-+    primary `locally` \unwrap ->+      handleRequest (unwrap request') (unwrap primaryStateRef)++  -- send response to client+  (primary, response) ~> client++kvs' :: Cond_' -> Choreo IO ()+kvs' cond_' = do+  primaryStateRef <- primary `locally` \_ -> newIORef (Map.empty :: State)+  backupStateRef <- backup `locally` \_ -> newIORef (Map.empty :: State)+  for_ requests \request -> do+    -- Replaced the interactive prompt with a dummy `locally` to keep the choreography's structure,+    -- for testing the overhead of `cond_`'s static analysis.+    clientRequest <- client `locally` \_ -> pure request+    kvs cond_' clientRequest primaryStateRef backupStateRef+    client `locally` \_ -> pure () -- putStrLn ("> " ++ show (unwrap response)) -- Don't print during benchmarking+    pure ()

+ bench/Main.hs view

@@ -0,0 +1,22 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE ImpredicativeTypes #-}++module Main where++import System.Environment(getArgs)+import System.Exit(exitFailure)++import Benchmark+import Choreos.Bookseller+import Choreos.CleanRoom+import Choreos.Kvs++main :: IO ()+main = getArgs >>= \case+  [backend, cond, "bookseller"] -> benchmarkChoreography backend cond ["buyer", "seller"] bookseller'+  [backend, cond, "kvs"] -> benchmarkChoreography backend cond ["client", "primary", "backup"] kvs'+  [backend, cond, "clean-room", read -> numClients, read -> numFailures] ->+    let locs = cleanRoomLocs numClients+    in benchmarkChoreography backend cond locs $ mkCleanRoom numFailures locs+  _ -> putStrLn "Invalid args" *> exitFailure

+ cloudchor.cabal view

@@ -0,0 +1,290 @@+cabal-version: 3.8++name: cloudchor+version: 0.1.0.0+synopsis: Lightweight and efficient choreographic programming for cloud services+description: Please see the README on GitHub at <https://github.com/aionescu/cloudchor#readme>+category: Concurrency++homepage: https://github.com/aionescu/cloudchor+bug-reports: https://github.com/aionescu/cloudchor/issues++author: Alex Ionescu+maintainer: Alex Ionescu <hackage@ionescu.sh>+copyright: Copyright (C) 2025 Alex Ionescu++license: MPL-2.0+license-files:+  LICENSE.txt+  LICENSE-HasChor.txt++build-type: Simple+extra-doc-files: README.md++tested-with:+  GHC == 9.10.3+  GHC == 9.8.4++source-repository head+  type: git+  location: https://github.com/aionescu/cloudchor++common threaded+  ghc-options:+    -threaded+    -rtsopts+    -with-rtsopts=-N++common warnings+  ghc-options:+    -Wall+    -Wcompat+    -Widentities+    -Wmissing-deriving-strategies+    -Wno-name-shadowing+    -Wno-unused-do-bind+    -Wno-type-defaults+    -Wpartial-fields+    -Wprepositive-qualified-module+    -Wredundant-constraints+    -Wunused-packages++library+  import: warnings+  default-language: GHC2021+  hs-source-dirs: src++  exposed-modules:+    Choreography+    Choreography.Choreo+    Choreography.Location+    Choreography.Location.Multi+    Choreography.Network+    Choreography.Network.Http+    Choreography.Network.Local+    Choreography.Network.LocalMsgCount+    Control.Monad.Freer++  build-depends:+    base                   >= 4.16 && < 4.21+    , containers           >= 0.6  && < 0.7+    , http-client          >= 0.7  && < 0.8+    , mtl                  >= 2.3  && < 2.4+    , servant              >= 0.19 && < 0.21+    , servant-client       >= 0.19 && < 0.21+    , servant-server       >= 0.19 && < 0.21+    , sop-core             >= 0.5  && < 0.6+    , template-haskell     >= 2.18 && < 2.23+    , unordered-containers >= 0.2  && < 0.3+    , warp                 >= 3.3  && < 3.4++executable bench+  import: threaded, warnings+  default-language: GHC2021+  hs-source-dirs: bench+  main-is: Main.hs++  other-modules:+    Benchmark+    Choreos.Bookseller+    Choreos.CleanRoom+    Choreos.Kvs++  build-depends:+    base         >= 4.16 && < 4.21+    , containers >= 0.6  && < 0.7+    , sop-core   >= 0.5  && < 0.6+    , time       >= 1.11 && < 1.13+    , cloudchor++executable example-clean-room+  import: warnings+  default-language: GHC2021+  hs-source-dirs: examples/clean-room+  main-is: Main.hs++  build-depends:+    base         >= 4.16 && < 4.21+    , random     >= 1.2  && < 1.3+    , sop-core   >= 0.5  && < 0.6+    , cloudchor++executable example-unsoundness+  import: warnings+  default-language: GHC2021+  hs-source-dirs: examples/unsoundness+  main-is: Main.hs++  build-depends:+    base             >= 4.16 && < 4.21+    , http-client    >= 0.7  && < 0.8+    , servant        >= 0.19 && < 0.21+    , servant-client >= 0.19 && < 0.21+    , servant-server >= 0.19 && < 0.21+    , warp           >= 3.3  && < 3.4+    , cloudchor++executable example-HasChor-bank-2pc+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/bank-2pc+  main-is: Main.hs++  build-depends:+    base        >= 4.16 && < 4.21+    , split     >= 0.2  && < 0.3+    , time      >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-bookseller-0-network+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/bookseller-0-network+  main-is: Main.hs++  build-depends:+    base        >= 4.16 && < 4.21+    , time      >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-bookseller-1-simple+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/bookseller-1-simple+  main-is: Main.hs++  build-depends:+    base        >= 4.16 && < 4.21+    , time      >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-bookseller-2-higher-order+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/bookseller-2-higher-order+  main-is: Main.hs++  build-depends:+    base        >= 4.16 && < 4.21+    , time      >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-bookseller-3-loc-poly+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/bookseller-3-loc-poly+  main-is: Main.hs++  build-depends:+    base        >= 4.16 && < 4.21+    , time      >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-diffiehellman+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/diffiehellman+  main-is: Main.hs++  build-depends:+    base        >= 4.16 && < 4.21+    , random    >= 1.2  && < 1.3+    , time      >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-karatsuba+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/karatsuba+  main-is: Main.hs++  build-depends:+    base         >= 4.16 && < 4.21+    , async      >= 2.2  && < 2.3+    , containers >= 0.6  && < 0.7+    , cloudchor++executable example-HasChor-kvs1+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/kvs-1-simple+  main-is: Main.hs++  build-depends:+    base         >= 4.16 && < 4.21+    , containers >= 0.6  && < 0.7+    , time       >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-kvs2+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/kvs-2-primary-backup+  main-is: Main.hs++  build-depends:+    base         >= 4.16 && < 4.21+    , containers >= 0.6  && < 0.7+    , time       >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-kvs3+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/kvs-3-higher-order+  main-is: Main.hs++  build-depends:+    base         >= 4.16 && < 4.21+    , containers >= 0.6  && < 0.7+    , time       >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-kvs4+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/kvs-4-loc-poly+  main-is: Main.hs++  build-depends:+    base         >= 4.16 && < 4.21+    , containers >= 0.6  && < 0.7+    , time       >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-mergesort+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/mergesort+  main-is: Main.hs++  ghc-options:+    -Wno-x-partial++  build-depends:+    base         >= 4.16 && < 4.21+    , containers >= 0.6  && < 0.7+    , time       >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-quicksort+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/quicksort+  main-is: Main.hs++  ghc-options:+    -Wno-x-partial++  build-depends:+    base         >= 4.16 && < 4.21+    , async      >= 2.2  && < 2.3+    , containers >= 0.6  && < 0.7+    , time       >= 1.11 && < 1.13+    , cloudchor++executable example-HasChor-ring-leader+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/ring-leader+  main-is: Main.hs++  build-depends:+    base           >= 4.16 && < 4.21+    , transformers >= 0.5  && < 0.7+    , cloudchor++executable example-HasChor-playground+  default-language: GHC2021+  hs-source-dirs: examples/HasChor/playground+  main-is: Main.hs++  build-depends:+    base        >= 4.16 && < 4.21+    , cloudchor

+ examples/HasChor/bank-2pc/Main.hs view

@@ -0,0 +1,105 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Main where++import Choreography (runChoreography)+import Choreography.Choreo+import Choreography.Location+import Choreography.Network.Http+import Data.List.Split (splitOn)+import Data.Maybe (catMaybes, mapMaybe)+import Data.Proxy+import System.Environment+import Text.Read (readMaybe)++client :: Proxy "client"+client = Proxy++coordinator :: Proxy "coordinator"+coordinator = Proxy++alice :: Proxy "alice"+alice = Proxy++bob :: Proxy "bob"+bob = Proxy++type State = (Int @ "alice", Int @ "bob")++type Action = (String, Int)++type Transaction = [Action]++-- | `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++-- | `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 :: State -> Transaction @ "coordinator" -> Choreo IO (Bool @ "coordinator", State)+handleTransaction (aliceBalance, bobBalance) tx = do+  -- Voting Phase+  txa <- (coordinator, tx) ~> alice+  voteAlice <- (alice, \unwrap -> do { return $ fst $ validate "alice" (unwrap aliceBalance) (unwrap txa) }) ~~> coordinator+  txb <- (coordinator, tx) ~> bob+  voteBob <- (bob, \unwrap -> do { return $ fst $ validate "bob" (unwrap bobBalance) (unwrap txb) }) ~~> coordinator++  -- Check if the transaction can be committed+  canCommit <- coordinator `locally` \unwrap -> do return $ unwrap voteAlice && unwrap voteBob++  -- Commit Phase+  cond (coordinator, canCommit) \case+    True -> do+      aliceBalance' <- alice `locally` \unwrap -> do return $ snd $ validate "alice" (unwrap aliceBalance) (unwrap txa)+      bobBalance' <- bob `locally` \unwrap -> do return $ snd $ validate "bob" (unwrap bobBalance) (unwrap txb)+      return (canCommit, (aliceBalance', bobBalance'))+    False -> do+      return (canCommit, (aliceBalance, bobBalance))++-- | `bank` loops forever and handles transactions.+bank :: State -> Choreo IO ()+bank state = do+  client `locally` \_ -> do+    putStrLn "Command? (alice|bob {amount};)+"+  tx <- (client, \_ -> do { parse <$> getLine }) ~~> coordinator+  (committed, state') <- handleTransaction state tx+  committed' <- (coordinator, committed) ~> client+  client `locally` \unwrap -> do+    putStrLn if unwrap committed' then "Committed" else "Not committed"+  alice `locally` \unwrap -> do putStrLn ("Alice's balance: " ++ show (unwrap (fst state')))+  bob `locally` \unwrap -> do putStrLn ("Bob's balance: " ++ show (unwrap (snd state')))+  bank state' -- repeat+  return ()++-- | `startBank` is a choreography that initializes the states and starts the bank application.+startBank :: Choreo IO ()+startBank = do+  aliceBalance <- alice `locally` \_ -> do return 0+  bobBalance <- bob `locally` \_ -> do return 0+  bank (aliceBalance, bobBalance)++main :: IO ()+main = do+  runChoreo startBank

+ examples/HasChor/bookseller-0-network/Main.hs view

@@ -0,0 +1,55 @@+module Main where++import Choreography.Network+import Choreography.Network.Http+import Data.Time+import System.Environment++buyer :: Network IO ()+buyer = do+  run $ putStrLn "Enter the title of the book to buy:"+  title <- run getLine+  send title "seller"+  price <- recv "seller"+  if price < budget+  then do+    send True "seller"+    (deliveryDate :: Day) <- recv "seller"+    run $ putStrLn ("The book will be delivered on " ++ (show deliveryDate))+  else do+    send False "seller"+    run $ putStrLn "The book's price is out of the budget"++seller :: Network IO ()+seller = do+  title <- recv "buyer"+  send (priceOf title) "buyer"+  decision <- recv "buyer"+  if decision+  then do+    send (deliveryDateOf title) "buyer"+  else do+    return ()++budget :: Int+budget = 100++priceOf :: String -> Int+priceOf "Types and Programming Languages" = 80+priceOf "Homotopy Type Theory"            = 120++deliveryDateOf :: String -> Day+deliveryDateOf "Types and Programming Languages" = fromGregorian 2023 12 19+deliveryDateOf "Homotopy Type Theory"            = fromGregorian 2023 09 18++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "buyer" -> runNetwork cfg "buyer" buyer+    "seller" -> runNetwork cfg "seller" seller+  return ()+  where+    cfg = mkHttpConfig [ ("buyer",  ("localhost", 4242))+                       , ("seller", ("localhost", 4343))+                       ]

+ examples/HasChor/bookseller-1-simple/Main.hs view

@@ -0,0 +1,97 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE LambdaCase     #-}++module Main where++import Choreography+import Data.Proxy+import Data.Time+import System.Environment++buyer :: Proxy "buyer"+buyer = Proxy++seller :: Proxy "seller"+seller = Proxy++-- | `bookseller` is a choreography that implements the bookseller protocol.+bookseller :: Choreo IO (Maybe Day @ "buyer")+bookseller = do+  -- the buyer node prompts the user to enter the title of the book to buy+  title <-+    buyer `locally` \_ -> do+      putStrLn "Enter the title of the book to buy"+      getLine+  -- the buyer sends the title to the seller+  title' <- (buyer, title) ~> seller++  -- the seller checks the price of the book+  price <- seller `locally` \un -> return $ priceOf (un title')+  -- the seller sends back the price of the book to the buyer+  price' <- (seller, price) ~> buyer++  -- the buyer decides whether to buy the book or not+  decision <- buyer `locally` \un -> return $ (un price') < budget++  -- if the buyer decides to buy the book, the seller sends the delivery date to the buyer+  cond (buyer, decision) \case+    True  -> do+      deliveryDate  <- seller `locally` \un -> return $ deliveryDateOf (un title')+      deliveryDate' <- (seller, deliveryDate) ~> buyer++      buyer `locally` \un -> do+        putStrLn $ "The book will be delivered on " ++ show (un deliveryDate')+        return $ Just (un deliveryDate')++    False -> do+      buyer `locally` \_ -> do+        putStrLn "The book's price is out of the budget"+        return Nothing++-- `bookseller'` is a simplified version of `bookseller` that utilizes `~~>`+bookseller' :: Choreo IO (Maybe Day @ "buyer")+bookseller' = do+  title <- (buyer, \_ -> do+               putStrLn "Enter the title of the book to buy"+               getLine+           )+           ~~> seller++  price <- (seller, \un -> return $ priceOf (un title)) ~~> buyer++  cond' (buyer, \un -> return $ (un price) < budget) \case+    True  -> do+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un title)) ~~> buyer++      buyer `locally` \un -> do+        putStrLn $ "The book will be delivered on " ++ show (un deliveryDate)+        return $ Just (un deliveryDate)++    False -> do+      buyer `locally` \_ -> do+        putStrLn "The book's price is out of the budget"+        return Nothing++budget :: Int+budget = 100++priceOf :: String -> Int+priceOf "Types and Programming Languages" = 80+priceOf "Homotopy Type Theory"            = 120++deliveryDateOf :: String -> Day+deliveryDateOf "Types and Programming Languages" = fromGregorian 2022 12 19+deliveryDateOf "Homotopy Type Theory"            = fromGregorian 2023 01 01++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "buyer"  -> runChoreography cfg bookseller' "buyer"+    "seller" -> runChoreography cfg bookseller' "seller"+  return ()+  where+    cfg = mkHttpConfig [ ("buyer",  ("localhost", 4242))+                       , ("seller", ("localhost", 4343))+                       ]

+ examples/HasChor/bookseller-2-higher-order/Main.hs view

@@ -0,0 +1,93 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE LambdaCase     #-}++module Main where++import Choreography+import Data.Proxy+import Data.Time+import System.Environment++buyer :: Proxy "buyer"+buyer = Proxy++seller :: Proxy "seller"+seller = Proxy++buyer2 :: Proxy "buyer2"+buyer2 = Proxy++-- | `bookseller` is a choreography that implements the bookseller protocol.+-- This version takes a choreography `mkDecision` that implements the decision making process.+bookseller :: (Int @ "buyer" -> Choreo IO (Bool @ "buyer")) -> Choreo IO (Maybe Day @ "buyer")+bookseller mkDecision = do+  -- the buyer reads the title of the book and sends it to the seller+  title <- (buyer, \_ -> do+               putStrLn "Enter the title of the book to buy"+               getLine+           )+           ~~> seller++  -- the seller checks the price of the book and sends it to the buyer+  price <- (seller, \un -> return $ priceOf (un title)) ~~> buyer++  -- 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+  cond (buyer, decision) \case+    True  -> do+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un title)) ~~> buyer++      buyer `locally` \un -> do+        putStrLn $ "The book will be delivered on " ++ show (un deliveryDate)+        return $ Just (un deliveryDate)++    False -> do+      buyer `locally` \_ -> do+        putStrLn "The book's price is out of the budget"+        return Nothing++-- | `mkDecision1` checks if buyer's budget is greater than the price of the book+mkDecision1 :: Int @ "buyer" -> Choreo IO (Bool @ "buyer")+mkDecision1 price = do+  buyer `locally` \un -> return $ un price < 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 :: Int @ "buyer" -> Choreo IO (Bool @ "buyer")+mkDecision2 price = do+  contrib <- (buyer2, \_ -> do+                 putStrLn "How much you're willing to contribute?"+                 read <$> getLine+             )+             ~~> buyer+  buyer `locally` \un -> return $ un price - un contrib <= budget++budget :: Int+budget = 100++priceOf :: String -> Int+priceOf "Types and Programming Languages" = 80+priceOf "Homotopy Type Theory"            = 120++deliveryDateOf :: String -> Day+deliveryDateOf "Types and Programming Languages" = fromGregorian 2022 12 19+deliveryDateOf "Homotopy Type Theory"            = fromGregorian 2023 01 01++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "buyer"  -> runChoreography cfg choreo "buyer"+    "seller" -> runChoreography cfg choreo "seller"+    "buyer2" -> runChoreography cfg choreo "buyer2"+  return ()+  where+    choreo = bookseller mkDecision2++    cfg = mkHttpConfig [ ("buyer",  ("localhost", 4242))+                       , ("seller", ("localhost", 4343))+                       , ("buyer2", ("localhost", 4444))+                       ]

+ examples/HasChor/bookseller-3-loc-poly/Main.hs view

@@ -0,0 +1,69 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE LambdaCase     #-}++module Main where++import Choreography+import Data.Proxy+import Data.Time+import GHC.TypeLits+import System.Environment++buyer :: Proxy "buyer"+buyer = Proxy++seller :: Proxy "seller"+seller = Proxy++-- | `bookseller` is a choreography that implements the bookseller protocol.+-- This version takes the name of the buyer as a parameter (`someBuyer`).+bookseller :: KnownSymbol a => Proxy a -> Choreo IO (Maybe Day @ a)+bookseller someBuyer = do+  -- the buyer reads the title of the book and sends it to the seller+  title <- (buyer, \_ -> do+               putStrLn "Enter the title of the book to buy"+               getLine+           )+           ~~> seller++  -- the seller checks the price of the book and sends it to the buyer+  price <- (seller, \un -> return $ priceOf (un title)) ~~> someBuyer++  cond' (someBuyer, \un -> return $ (un price) < budget) \case+    True  -> do+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un title)) ~~> someBuyer++      someBuyer `locally` \un -> do+        putStrLn $ "The book will be delivered on " ++ show (un deliveryDate)+        return $ Just (un deliveryDate)++    False -> do+      someBuyer `locally` \_ -> do+        putStrLn "The book's price is out of the budget"+        return Nothing++budget :: Int+budget = 100++priceOf :: String -> Int+priceOf "Types and Programming Languages" = 80+priceOf "Homotopy Type Theory"            = 120++deliveryDateOf :: String -> Day+deliveryDateOf "Types and Programming Languages" = fromGregorian 2022 12 19+deliveryDateOf "Homotopy Type Theory"            = fromGregorian 2023 01 01++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "buyer"  -> runChoreography cfg choreo "buyer"+    "seller" -> runChoreography cfg choreo "seller"+  return ()+  where+    choreo = bookseller buyer+    +    cfg = mkHttpConfig [ ("buyer",  ("localhost", 4242))+                       , ("seller", ("localhost", 4343))+                       ]

+ examples/HasChor/diffiehellman/Main.hs view

@@ -0,0 +1,91 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}++module Main where++import Choreography (mkHttpConfig, runChoreography)+import Choreography.Choreo+import Choreography.Location+import Data.Proxy+import Data.Time+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]++-- set up proxies+alice :: Proxy "alice"+alice = Proxy++bob :: Proxy "bob"+bob = Proxy++diffieHellman :: Choreo IO (Integer @ "alice", Integer @ "bob")+diffieHellman = do+  -- wait for alice to initiate the process+  alice `locally` \unwrap -> do+    putStrLn "enter to start key exchange..."+    getLine+  bob `locally` \unwrap -> do+    putStrLn "waiting for alice to initiate key exchange"++  -- alice picks p and g and sends them to bob+  pa <-+    alice `locally` \unwrap -> do+      x <- randomRIO (200, 1000 :: Int)+      return $ primeNums !! x+  pb <- (alice, pa) ~> bob+  ga <- alice `locally` \unwrap -> do randomRIO (10, unwrap pa)+  gb <- (alice, ga) ~> bob++  -- alice and bob select secrets+  a <- alice `locally` \unwrap -> do randomRIO (200, 1000 :: Integer)+  b <- bob `locally` \unwrap -> do randomRIO (200, 1000 :: Integer)++  -- alice and bob computes numbers that they exchange+  a' <- alice `locally` \unwrap -> do return $ unwrap ga ^ unwrap a `mod` unwrap pa+  b' <- bob `locally` \unwrap -> do return $ unwrap gb ^ unwrap b `mod` unwrap pb++  -- exchange numbers+  a'' <- (alice, a') ~> bob+  b'' <- (bob, b') ~> alice++  -- compute shared key+  s1 <-+    alice `locally` \unwrap ->+      let s = unwrap b'' ^ unwrap a `mod` unwrap pa+       in do+            putStrLn ("alice's shared key: " ++ show s)+            return s+  s2 <-+    bob `locally` \unwrap ->+      let s = unwrap a'' ^ unwrap b `mod` unwrap pb+       in do+            putStrLn ("bob's shared key: " ++ show s)+            return s+  return (s1, s2)++main :: IO ()+main = do+  [loc] <- getArgs+  x <- case loc of+    "alice" -> runChoreography config diffieHellman "alice"+    "bob" -> runChoreography config diffieHellman "bob"+  return ()+  where+    config =+      mkHttpConfig+        [ ("alice", ("localhost", 5000)),+          ("bob", ("localhost", 5001))+        ]

+ examples/HasChor/karatsuba/Main.hs view

@@ -0,0 +1,93 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}++module Main where++import Choreography (runChoreography)+import Choreography.Choreo+import Choreography.Location+import Choreography.Network.Local+import Control.Concurrent.Async (async, mapConcurrently_, wait)+import Data.Proxy+import GHC.TypeLits (KnownSymbol)+import System.Environment++primary :: Proxy "primary"+primary = Proxy++worker1 :: Proxy "worker1"+worker1 = Proxy++worker2 :: Proxy "worker2"+worker2 = Proxy++data KaratsubaNums = KaratsubaNums+  { splitter :: Integer,+    h1 :: Integer,+    h2 :: Integer,+    l1 :: Integer,+    l2 :: Integer+  }++karatsuba ::+  (KnownSymbol a, KnownSymbol b, KnownSymbol c) =>+  Proxy a ->+  Proxy b ->+  Proxy c ->+  (Integer @ a) ->+  (Integer @ a) ->+  Choreo IO (Integer @ a)+karatsuba a b c n1 n2 = do+  done <- a `locally` \unwrap -> return $ unwrap n1 < 10 || unwrap n2 < 10+  cond+    (a, done)+    \case+      True -> do+        a `locally` \unwrap -> return $ unwrap n1 * unwrap n2+      False -> do+        x <- a `locally` \unwrap -> return $ f (unwrap n1) (unwrap n2)+        l1' <- (a, \unwrap -> return $ l1 (unwrap x)) ~~> b+        l2' <- (a, \unwrap -> return $ l2 (unwrap x)) ~~> b+        h1' <- (a, \unwrap -> return $ h1 (unwrap x)) ~~> c+        h2' <- (a, \unwrap -> return $ h2 (unwrap x)) ~~> c+        z0' <- karatsuba b c a l1' l2'+        z0 <- (b, z0') ~> a+        z2' <- karatsuba c a b h1' h2'+        z2 <- (c, z2') ~> a+        s1 <- a `locally` \unwrap -> return $ l1 (unwrap x) + h1 (unwrap x)+        s2 <- a `locally` \unwrap -> return $ l2 (unwrap x) + h2 (unwrap x)+        z1' <- karatsuba a b c s1 s2+        z1 <- a `locally` \unwrap -> return $ unwrap z1' - unwrap z2 - unwrap z0+        a `locally` \unwrap -> return let s = splitter (unwrap x) in (unwrap z2 * s * s) + (unwrap z1 * s) + unwrap 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 = 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 IO ()+mainChoreo n1 n2 = do+  n1 <- primary `locally` \_ -> return n1+  n2 <- primary `locally` \_ -> return n2+  result <- karatsuba primary worker1 worker2 n1 n2+  primary `locally` \unwrap -> do+    print (unwrap result)+    return ()+  return ()++main :: IO ()+main = do+  [n1, n2] <- map read <$> getArgs+  config <- mkLocalConfig locs+  mapConcurrently_ (runChoreography config (mainChoreo n1 n2)) locs+  return ()+  where+    locs = ["primary", "worker1", "worker2"]

+ examples/HasChor/kvs-1-simple/Main.hs view

@@ -0,0 +1,103 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Main where++import Choreography (runChoreography)+import Choreography.Choreo+import Choreography.Location+import Choreography.Network.Http+import Control.Concurrent (threadDelay)+import Control.Monad+import Data.IORef+import Data.Map (Map, (!))+import Data.Map qualified as Map+import Data.Maybe (fromMaybe, isJust)+import Data.Proxy+import GHC.IORef (IORef (IORef))+import GHC.TypeLits (KnownSymbol)+import System.Environment++client :: Proxy "client"+client = Proxy++server :: Proxy "server"+server = Proxy++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 ::+  Request @ "client" ->+  IORef State @ "server" ->+  Choreo IO (Response @ "client")+kvs request stateRef = do+  -- send the request to the server+  request' <- (client, request) ~> server+  -- the server handles the response and creates a response+  response <-+    server `locally` \unwrap ->+      handleRequest (unwrap request') (unwrap stateRef)+  -- send the response back to the client+  (server, response) ~> client++-- | `mainChoreo` is a choreography that serves as the entry point of the program.+-- It initializes the state and loops forever.+mainChoreo :: Choreo IO ()+mainChoreo = do+  stateRef <- server `locally` \_ -> newIORef (Map.empty :: State)+  loop stateRef+  where+    loop :: IORef State @ "server" -> Choreo IO ()+    loop stateRef = do+      request <- client `locally` \_ -> readRequest+      response <- kvs request stateRef+      client `locally` \unwrap -> do putStrLn ("> " ++ (show (unwrap response)))+      loop stateRef++main :: IO ()+main = do+  [loc] <- getArgs+  case loc of+    "client" -> runChoreography config mainChoreo "client"+    "server" -> runChoreography config mainChoreo "server"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("server", ("localhost", 4000))+        ]

+ examples/HasChor/kvs-2-primary-backup/Main.hs view

@@ -0,0 +1,125 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Main where++import Choreography (runChoreography)+import Choreography.Choreo+import Choreography.Location+import Choreography.Network.Http+import Control.Concurrent (threadDelay)+import Control.Monad+import Data.IORef+import Data.Map (Map, (!))+import Data.Map qualified as Map+import Data.Maybe (fromMaybe, isJust)+import Data.Proxy+import GHC.IORef (IORef (IORef))+import GHC.TypeLits (KnownSymbol)+import System.Environment++client :: Proxy "client"+client = Proxy++primary :: Proxy "primary"+primary = Proxy++backup :: Proxy "backup"+backup = Proxy++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 ::+  Request @ "client" ->+  (IORef State @ "primary", IORef State @ "backup") ->+  Choreo IO (Response @ "client")+kvs request (primaryStateRef, backupStateRef) = do+  -- send request to the primary node+  request' <- (client, request) ~> primary++  -- branch on the request+  cond (primary, request') \case+    -- if the request is a `PUT`, forward the request to the backup node+    Put key value -> do+      request'' <- (primary, request') ~> backup+      ack <-+        backup `locally` \unwrap -> do+          handleRequest (unwrap request'') (unwrap backupStateRef)+      (backup, ack) ~> primary+      return ()+    _ -> do+      return ()++  -- process request on the primary node+  response <-+    primary `locally` \unwrap ->+      handleRequest (unwrap request') (unwrap primaryStateRef)++  -- send response to client+  (primary, response) ~> client++-- | `mainChoreo` is a choreography that serves as the entry point of the program.+-- It initializes the state and loops forever.+mainChoreo :: Choreo IO ()+mainChoreo = do+  primaryStateRef <- primary `locally` \_ -> newIORef (Map.empty :: State)+  backupStateRef <- backup `locally` \_ -> newIORef (Map.empty :: State)+  loop (primaryStateRef, backupStateRef)+  where+    loop :: (IORef State @ "primary", IORef State @ "backup") -> Choreo IO ()+    loop stateRefs = do+      request <- client `locally` \_ -> readRequest+      response <- kvs request stateRefs+      client `locally` \unwrap -> do putStrLn ("> " ++ show (unwrap 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"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("primary", ("localhost", 4000)),+          ("backup", ("localhost", 5000))+        ]

+ examples/HasChor/kvs-3-higher-order/Main.hs view

@@ -0,0 +1,156 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Main where++import Choreography (runChoreography)+import Choreography.Choreo+import Choreography.Location+import Choreography.Network.Http+import Control.Concurrent (threadDelay)+import Control.Monad+import Data.IORef+import Data.Map (Map, (!))+import Data.Map qualified as Map+import Data.Maybe (fromMaybe, isJust)+import Data.Proxy+import GHC.IORef (IORef (IORef))+import GHC.TypeLits (KnownSymbol)+import System.Environment++client :: Proxy "client"+client = Proxy++primary :: Proxy "primary"+primary = Proxy++backup :: Proxy "backup"+backup = Proxy++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 =+  Request @ "primary" -> a -> Choreo IO (Response @ "primary")++-- | `nullReplicationStrategy` is a replication strategy that does not replicate the state.+nullReplicationStrategy :: ReplicationStrategy (IORef State @ "primary")+nullReplicationStrategy request stateRef = do+  primary `locally` \unwrap ->+    handleRequest (unwrap request) (unwrap stateRef)++-- | `primaryBackupReplicationStrategy` is a replication strategy that replicates the state to a backup server.+primaryBackupReplicationStrategy ::+  ReplicationStrategy (IORef State @ "primary", IORef State @ "backup")+primaryBackupReplicationStrategy request (primaryStateRef, backupStateRef) = do+  -- relay request to backup if it is mutating (= PUT)+  cond (primary, request) \case+    Put _ _ -> do+      request' <- (primary, request) ~> backup+      ( backup,+        \unwrap ->+          handleRequest (unwrap request') (unwrap backupStateRef)+        )+        ~~> primary+      return ()+    _ -> do+      return ()++  -- process request on primary+  primary `locally` \unwrap ->+    handleRequest (unwrap request) (unwrap 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.+  Request @ "client" ->+  a ->+  ReplicationStrategy a ->+  Choreo IO (Response @ "client")+kvs request stateRefs replicationStrategy = do+  request' <- (client, request) ~> primary++  -- call the provided replication strategy+  response <- replicationStrategy request' stateRefs++  -- send response to client+  (primary, response) ~> client++-- | `nullReplicationChoreo` is a choreography that uses `nullReplicationStrategy`.+nullReplicationChoreo :: Choreo IO ()+nullReplicationChoreo = do+  stateRef <- primary `locally` \_ -> newIORef (Map.empty :: State)+  loop stateRef+  where+    loop :: IORef State @ "primary" -> Choreo IO ()+    loop stateRef = do+      request <- client `locally` \_ -> readRequest+      response <- kvs request stateRef nullReplicationStrategy+      client `locally` \unwrap -> do putStrLn (show (unwrap response))+      loop stateRef++-- | `primaryBackupChoreo` is a choreography that uses `primaryBackupReplicationStrategy`.+primaryBackupChoreo :: Choreo IO ()+primaryBackupChoreo = do+  primaryStateRef <- primary `locally` \_ -> newIORef (Map.empty :: State)+  backupStateRef <- backup `locally` \_ -> newIORef (Map.empty :: State)+  loop (primaryStateRef, backupStateRef)+  where+    loop :: (IORef State @ "primary", IORef State @ "backup") -> Choreo IO ()+    loop stateRefs = do+      request <- client `locally` \_ -> readRequest+      response <- kvs request stateRefs primaryBackupReplicationStrategy+      client `locally` \unwrap -> do putStrLn ("> " ++ show (unwrap 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"+  return ()+  where+    mainChoreo = primaryBackupChoreo -- or `nullReplicationChoreo`+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("primary", ("localhost", 4000)),+          ("backup", ("localhost", 5000))+        ]

+ examples/HasChor/kvs-4-loc-poly/Main.hs view

@@ -0,0 +1,196 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Main where++import Choreography (runChoreography)+import Choreography.Choreo+import Choreography.Location+import Choreography.Network.Http+import Control.Concurrent (threadDelay)+import Control.Monad+import Data.IORef+import Data.Map (Map, (!))+import Data.Map qualified as Map+import Data.Maybe (fromMaybe, isJust)+import Data.Proxy+import GHC.IORef (IORef (IORef))+import GHC.TypeLits (KnownSymbol)+import System.Environment++client :: Proxy "client"+client = Proxy++primary :: Proxy "primary"+primary = Proxy++backup1 :: Proxy "backup1"+backup1 = Proxy++backup2 :: Proxy "backup2"+backup2 = Proxy++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 = Request @ "primary" -> a -> Choreo IO (Response @ "primary")++-- | `nullReplicationStrategy` is a replication strategy that does not replicate the state.+nullReplicationStrategy :: ReplicationStrategy (IORef State @ "primary")+nullReplicationStrategy request stateRef = do+  primary `locally` \unwrap -> case unwrap request of+    Put key value -> do+      modifyIORef (unwrap stateRef) (Map.insert key value)+      return (Just value)+    Get key -> do+      state <- readIORef (unwrap stateRef)+      return (Map.lookup key state)++-- | `doBackup` relays a mutating request to a backup location.+doBackup ::+  KnownSymbol a =>+  KnownSymbol b =>+  Proxy a ->+  Proxy b ->+  Request @ a ->+  IORef State @ b ->+  Choreo IO ()+doBackup locA locB request stateRef = do+  cond (locA, request) \case+    Put _ _ -> do+      request' <- (locA, request) ~> locB+      (locB, \unwrap -> handleRequest (unwrap request') (unwrap stateRef))+        ~~> locA+      return ()+    _ -> do+      return ()++-- | `primaryBackupReplicationStrategy` is a replication strategy that replicates the state to a backup server.+primaryBackupReplicationStrategy :: ReplicationStrategy (IORef State @ "primary", IORef State @ "backup1")+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` \unwrap -> handleRequest (unwrap request) (unwrap primaryStateRef)++-- | `doubleBackupReplicationStrategy` is a replication strategy that replicates the state to two backup servers.+doubleBackupReplicationStrategy ::+  ReplicationStrategy+    (IORef State @ "primary", IORef State @ "backup1", IORef State @ "backup2")+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` \unwrap ->+      handleRequest (unwrap request) (unwrap 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 :: Request @ "client" -> a -> ReplicationStrategy a -> Choreo IO (Response @ "client")+kvs request stateRefs replicationStrategy = do+  request' <- (client, request) ~> primary++  -- call the provided replication strategy+  response <- replicationStrategy request' stateRefs++  -- send response to client+  (primary, response) ~> client++-- | `nullReplicationChoreo` is a choreography that uses `nullReplicationStrategy`.+nullReplicationChoreo :: Choreo IO ()+nullReplicationChoreo = do+  stateRef <- primary `locally` \_ -> newIORef (Map.empty :: State)+  loop stateRef+  where+    loop :: IORef State @ "primary" -> Choreo IO ()+    loop stateRef = do+      request <- client `locally` \_ -> readRequest+      response <- kvs request stateRef nullReplicationStrategy+      client `locally` \unwrap -> do putStrLn (show (unwrap response))+      loop stateRef++-- | `primaryBackupChoreo` is a choreography that uses `primaryBackupReplicationStrategy`.+primaryBackupChoreo :: Choreo IO ()+primaryBackupChoreo = do+  primaryStateRef <- primary `locally` \_ -> newIORef (Map.empty :: State)+  backupStateRef <- backup1 `locally` \_ -> newIORef (Map.empty :: State)+  loop (primaryStateRef, backupStateRef)+  where+    loop :: (IORef State @ "primary", IORef State @ "backup1") -> Choreo IO ()+    loop stateRefs = do+      request <- client `locally` \_ -> readRequest+      response <- kvs request stateRefs primaryBackupReplicationStrategy+      client `locally` \unwrap -> do putStrLn (show (unwrap response))+      loop stateRefs++-- | `doubleBackupChoreo` is a choreography that uses `doubleBackupReplicationStrategy`.+doubleBackupChoreo :: Choreo 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 :: (IORef State @ "primary", IORef State @ "backup1", IORef State @ "backup2") -> Choreo IO ()+    loop stateRefs = do+      request <- client `locally` \_ -> readRequest+      response <- kvs request stateRefs doubleBackupReplicationStrategy+      client `locally` \unwrap -> do putStrLn ("> " ++ show (unwrap 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"+  return ()+  where+    config =+      mkHttpConfig+        [ ("client", ("localhost", 3000)),+          ("primary", ("localhost", 4000)),+          ("backup1", ("localhost", 5000)),+          ("backup2", ("localhost", 6000))+        ]

+ examples/HasChor/mergesort/Main.hs view

@@ -0,0 +1,118 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}++module Main where++import Choreography (runChoreography)+import Choreography.Choreo+import Choreography.Location+import Choreography.Network.Http+import Data.Proxy+import Data.Time+import GHC.TypeLits (KnownSymbol)+import System.Environment++divide :: [a] -> ([a], [a])+divide xs = splitAt lhx xs+  where+    lhx = length xs `div` 2++primary :: Proxy "primary"+primary = Proxy++worker1 :: Proxy "worker1"+worker1 = Proxy++worker2 :: Proxy "worker2"+worker2 = Proxy++sort ::+  KnownSymbol a =>+  Proxy a ->+  KnownSymbol b =>+  Proxy b ->+  KnownSymbol c =>+  Proxy c ->+  ([Int] @ a) ->+  Choreo IO ([Int] @ a)+sort a b c lst = do+  condition <- a `locally` \unwrap -> do return $ length (unwrap lst) > 1+  cond (a, condition) \case+    True -> do+      pivot <- a `locally` \unwrap -> do return $ length (unwrap lst) `div` 2+      divided <- a `locally` \unwrap -> do return $ divide (unwrap lst)+      l <- a `locally` \unwrap -> do return $ fst (unwrap divided)+      r <- a `locally` \unwrap -> do return $ snd (unwrap divided)+      l' <- (a, l) ~> b+      r' <- (a, r) ~> c+      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 =>+  Proxy a ->+  KnownSymbol b =>+  Proxy b ->+  KnownSymbol c =>+  Proxy c ->+  [Int] @ b ->+  [Int] @ c ->+  Choreo IO ([Int] @ a)+merge a b c lhs rhs = do+  lhsHasElements <- b `locally` \unwrap -> do return $ not (null (unwrap lhs))+  cond (b, lhsHasElements) \case+    True -> do+      rhsHasElements <- c `locally` \unwrap -> do return $ not (null (unwrap rhs))+      cond (c, rhsHasElements) \case+        True -> do+          rhsHeadAtC <- c `locally` \unwrap -> do return $ head (unwrap rhs)+          rhsHeadAtB <- (c, rhsHeadAtC) ~> b+          takeLhs <- b `locally` \unwrap -> do return $ head (unwrap lhs) <= unwrap rhsHeadAtB+          cond (b, takeLhs) \case+            True -> do+              -- take (head lhs) and merge the rest+              lhs' <- b `locally` \unwrap -> do return $ tail (unwrap lhs)+              merged <- merge a b c lhs' rhs+              lhsHeadAtB <- b `locally` \unwrap -> do return $ head (unwrap lhs)+              lhsHeadAtA <- (b, lhsHeadAtB) ~> a+              a `locally` \unwrap -> do return $ unwrap lhsHeadAtA : unwrap merged+            False -> do+              -- take (head rhs) and merge the rest+              rhs' <- c `locally` \unwrap -> do return $ tail (unwrap rhs)+              merged <- merge a b c lhs rhs'+              rhsHeadAtC <- c `locally` \unwrap -> do return $ head (unwrap rhs)+              rhsHeadAtA <- (c, rhsHeadAtC) ~> a+              a `locally` \unwrap -> do return $ unwrap rhsHeadAtA : unwrap merged+        False -> do+          (b, lhs) ~> a+    False -> do+      (c, rhs) ~> a++mainChoreo :: Choreo IO ()+mainChoreo = do+  lst <- primary `locally` \unwrap -> do return [1, 6, 5, 3, 4, 2, 7, 8]+  sorted <- sort primary worker1 worker2 lst+  primary `locally` \unwrap -> do+    print (unwrap 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"+  return ()+  where+    config =+      mkHttpConfig+        [ ("primary", ("localhost", 3000)),+          ("worker1", ("localhost", 4000)),+          ("worker2", ("localhost", 5000))+        ]

+ examples/HasChor/playground/Main.hs view

@@ -0,0 +1,31 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE LambdaCase     #-}++module Main where++import Choreography+import Control.Monad+import Data.Proxy+import System.Environment++-- Step 1: Defining locations+alice :: Proxy "alice"+alice = Proxy++-- Step 2: Writing a choreography+choreography :: Choreo IO (() @ "alice")+choreography = do+  alice `locally` \_ -> putStrLn "Hello, world!"++-- Step 3: Projecting and running the chreography+main :: IO ()+main = do+  args <- getArgs+  case args of+    [loc] -> void $ runChoreography cfg choreography loc+    _     -> error "wrong usage: must provide exactly one location"+  where+    -- Step 4: Mapping locations to HTTP ports+    cfg = mkHttpConfig [ ("alice", ("localhost", 4242))+                       ]

+ examples/HasChor/quicksort/Main.hs view

@@ -0,0 +1,56 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}++module Main where++import Choreography (runChoreography)+import Choreography.Choreo+import Choreography.Location+import Choreography.Network.Local+import Control.Concurrent.Async (async, mapConcurrently_, wait)+import Data.Proxy+import Data.Time+import GHC.TypeLits (KnownSymbol)+import System.Environment++primary :: Proxy "primary"+primary = Proxy++worker1 :: Proxy "worker1"+worker1 = Proxy++worker2 :: Proxy "worker2"+worker2 = Proxy++quicksort :: (KnownSymbol a, KnownSymbol b, KnownSymbol c) => Proxy a -> Proxy b -> Proxy c -> [Int] @ a -> Choreo IO ([Int] @ a)+quicksort a b c lst = do+  isEmpty <- a `locally` \unwrap -> pure (null (unwrap lst))+  cond (a, isEmpty) \case+    True -> do+      a `locally` \_ -> pure []+    False -> do+      smaller <- (a, \unwrap -> let x : xs = unwrap lst in pure [i | i <- xs, i <= x]) ~~> b+      smaller' <- quicksort b c a smaller+      smaller'' <- (b, smaller') ~> a+      bigger <- (a, \unwrap -> let x : xs = unwrap lst in pure [i | i <- xs, i > x]) ~~> c+      bigger' <- quicksort c a b bigger+      bigger'' <- (c, bigger') ~> a+      a `locally` \unwrap -> pure $ unwrap smaller'' ++ [head (unwrap lst)] ++ unwrap bigger''++mainChoreo :: Choreo IO ()+mainChoreo = do+  lst <- primary `locally` \unwrap -> do return [1, 6, 5, 3, 4, 2, 7, 8]+  sorted <- quicksort primary worker1 worker2 lst+  primary `locally` \unwrap -> do+    print (unwrap sorted)+    return ()+  return ()++main :: IO ()+main = do+  config <- mkLocalConfig locs+  mapConcurrently_ (runChoreography config mainChoreo) locs+  return ()+  where+    locs = ["primary", "worker1", "worker2"]

+ examples/HasChor/ring-leader/Main.hs view

@@ -0,0 +1,82 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE LambdaCase     #-}++module Main where++import Choreography+import Data.Proxy+import GHC.TypeLits (KnownSymbol)+import Control.Monad+import Control.Monad.Trans.Class+import Control.Monad.Trans.State+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 = forall l l'.+  (KnownSymbol l, KnownSymbol l') => Edge (Proxy l) (Proxy l')++-- a ring is a sequence of edges+type Ring = [Edge]++type Label = Int++ringLeader :: Ring -> Choreo (StateT Label IO) ()+ringLeader ring = loop ring+  where+    loop :: Ring -> Choreo (StateT Label IO) ()+    loop []     = loop ring+    loop (x:xs) = do+      finished <- talkToRight x+      if finished+      then return ()+      else loop xs++    talkToRight :: Edge -> Choreo (StateT Label IO) Bool+    talkToRight (Edge left right) = do+      labelLeft  <- (left, \_ -> get) ~~> right+      labelRight <- right `locally` \_ -> get++      finished <- right `locally` \un ->+        return $ un labelLeft == un labelRight++      cond (right, finished) \case+        True  -> do+          right `locally` \_ -> lift $ putStrLn "I'm the leader"+          return True+        False -> do+          right `locally` \un -> put (max (un labelLeft) (un labelRight))+          return False++nodeA :: Proxy "A"+nodeA = Proxy++nodeB :: Proxy "B"+nodeB = Proxy++nodeC :: Proxy "C"+nodeC = Proxy++nodeD :: Proxy "D"+nodeD = Proxy++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 [ ("A", ("localhost", 4242))+                          , ("B", ("localhost", 4343))+                          , ("C", ("localhost", 4444))+                          , ("D", ("localhost", 4545))+                          ]

+ examples/clean-room/Main.hs view

@@ -0,0 +1,170 @@+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++{-# LANGUAGE BlockArguments     #-}+{-# LANGUAGE DataKinds          #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GADTs              #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase         #-}+{-# LANGUAGE ParallelListComp   #-}++module Main where++import Control.Monad(replicateM)+import Data.Foldable(fold)+import Data.Function((&))+import Data.Proxy(Proxy(..))+import Data.SOP.BasicFunctors(mapKK, K (..))+import Data.SOP.Classes(HCollapse(..), hmap, hsequenceK)+import Data.SOP.Constraint(All)+import Data.SOP.NP(NP(..))+import GHC.TypeLits(KnownSymbol, SSymbol, withKnownSymbol, withSomeSSymbol)+import System.Environment(getArgs)+import System.Random(randomIO, randomRIO)++import Choreography+import Choreography.Location+import Choreography.Location.Multi++-- Schema and dataset handling (illustrative)++-- For simplicity, all datasets follow the same trivial schema: a list of numbers+data Schema = Schema+  deriving stock (Show, Read)++newtype Dataset = Dataset [Int]+  deriving stock (Show, Read)+  deriving newtype (Semigroup, Monoid)++data Query+  = Len+  | Sum+  | Avg+  | Min+  | Max+  deriving stock (Eq, Ord, Show, Read, Enum, Bounded)++loadSchema :: KnownSymbol l => Proxy l -> IO Schema+loadSchema _ = pure Schema++mergeSchemas :: [Schema] -> Schema+mergeSchemas _ = Schema++conformsToSchema :: Schema -> Dataset -> IO Bool+conformsToSchema _ _ = randomIO -- To simulate failures++emptyDataset :: Dataset+emptyDataset = Dataset []++-- Simulate some I/O to load a dataset (e.g. from a file)+loadDataset :: KnownSymbol l => Proxy l -> IO Dataset+loadDataset _ = do+  n <- randomRIO (5, 10)+  Dataset <$> replicateM n (randomRIO (-100, 100))++mergeDatasets :: [Dataset] -> Dataset+mergeDatasets = fold++-- Simulate the selection of a query (by picking one randomly)+loadQuery :: KnownSymbol l => Proxy l -> Schema -> IO Query+loadQuery _ _ = toEnum <$> randomRIO (fromEnum @Query minBound, fromEnum @Query maxBound)++agreeWithQueries :: KnownSymbol l => Proxy l -> [Query] -> IO Bool+agreeWithQueries _ _ = pure True++runQuery :: Dataset -> Query -> IO Int+runQuery (Dataset ds) q =+  pure $+    case q of+      Len -> length ds+      Sum -> sum ds+      Avg -> sum ds `quot` length ds+      Min -> minimum ds+      Max -> maximum ds++-- Error-handling (if datasets don't conform to schema)++getClientDataset :: (KnownSymbol server, KnownSymbol client) => Int -> Schema @ server -> Proxy server -> Proxy client -> Choreo IO (Dataset @ server)+getClientDataset tries schema server client =+  if tries <= 0 then+    pure $ wrap emptyDataset+  else do+    dataset <- (client, \_ -> loadDataset client) ~~> server+    cond_' (server, \unwrap -> conformsToSchema (unwrap schema) (unwrap dataset)) \case+      True -> pure dataset+      False -> getClientDataset (tries - 1) schema server client++getClientDatasets :: (KnownSymbol server, All KnownSymbol clients) => Int -> Schema @ server -> Proxy server -> NP Proxy clients -> Choreo IO (NP (K Dataset) clients @ server)+getClientDatasets _ _ _ Nil = pure $ wrap Nil+getClientDatasets tries schema server (client :* clients) = do+  dataset <- getClientDataset tries schema server client+  datasets <- getClientDatasets tries schema server clients+  locally server \unwrap -> pure $ K (unwrap dataset) :* unwrap datasets++-- Main choreography++cleanRoom :: (KnownSymbol server, All KnownSymbol clients) => Proxy server -> NP Proxy clients -> Choreo IO ()+cleanRoom server clients = do+  -- Every client loads their data schema and sends it to the server+  schemas <- (clients, \c _ -> loadSchema c) *~~> server++  -- Server merges the schemas+  finalSchemaS <- locally server \unwrap -> pure $ mergeSchemas $ hcollapse $ unwrap schemas++  -- Server broadcasts the final schema+  finalSchema <- (server, finalSchemaS) ~>* clients++  -- Based on the final schema, each client computes what query it wants to run, and sends it back to the server+  queriesS <- (clients, \c unwrap -> loadQuery c $ unwrap finalSchema) *~~> server++  -- Server broadcasts the list of queries to all clients+  queries <- (server, \unwrap -> pure $ hcollapse $ unwrap queriesS) ~~>* clients++  -- Each client locally decides if they agree with everyone else's queries, and sends back a response+  agreements <- (clients, \c unwrap -> agreeWithQueries c $ unwrap queries) *~~> server++  -- Server branches on the responses+  cond_' (server, \unwrap -> pure $ and $ hcollapse $ unwrap agreements) \case+    False -> do -- Someone disagrees, end the protocol+      multilocally clients \_ _ -> print "Disagreement"+      pure $ wrap ()+    True -> do -- Everyone agrees, proceed+      -- The amount of times the server will ask for a valid dataset+      let tries = 5++      -- Clients send their datasets to the server+      datasets <- getClientDatasets tries finalSchemaS server clients++      -- Server locally merges the datasets and runs all the queries+      resultsS <- locally server \unwrap -> do+        let aggregatedDataset = mergeDatasets $ hcollapse $ unwrap datasets+        hsequenceK $ hmap (mapKK $ runQuery aggregatedDataset) $ unwrap queriesS++      -- Server sends the result of each query "pointwise"+      results <- (server, resultsS) ~>. clients++      -- Clients consume the received query results+      multilocally clients \_ unwrap -> print $ unwrap results+      pure $ wrap ()++  pure ()++-- Running the choreography++withProxy :: String -> (forall s. KnownSymbol s => Proxy s -> a) -> a+withProxy s f = withSomeSSymbol s \(ss :: SSymbol s) -> withKnownSymbol ss $ f @s Proxy++withProxies :: [String] -> (forall ss. All KnownSymbol ss => NP Proxy ss -> a) -> a+withProxies [] f = f Nil+withProxies (s : ss) f =+  withProxy s \s ->+    withProxies ss \ss ->+      f $ s :* ss++httpConfig :: [String] -> HttpConfig+httpConfig ls = mkHttpConfig [(l, ("localhost", port)) | l <- ls | port <- [3000..]]++main :: IO ()+main = do+  self : ls@(server : clients) <- getArgs+  runChoreography (httpConfig ls) (cleanRoom & withProxy server & withProxies clients) self

+ examples/unsoundness/Main.hs view

@@ -0,0 +1,102 @@+{-# LANGUAGE BlockArguments     #-}+{-# LANGUAGE DataKinds          #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GADTs              #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE ParallelListComp   #-}+{-# LANGUAGE LambdaCase         #-}+{-# LANGUAGE ViewPatterns       #-}++module Main where++import Data.Proxy(Proxy(..))+import Data.IORef (newIORef, readIORef, writeIORef)+import Control.Concurrent (forkIO, killThread, threadDelay)+import Control.Monad.IO.Class (MonadIO(..))+import System.Environment(getArgs)++import Servant.API+import Servant.Server (serve)+import Network.Wai.Handler.Warp (run)+import Network.HTTP.Client (defaultManagerSettings, newManager)+import Servant.Client (client, runClientM, BaseUrl(..), mkClientEnv, Scheme(..))++import Choreography+import Choreography.Location+import System.Exit (exitSuccess)++a :: Proxy "a"+a = Proxy++b :: Proxy "b"+b = Proxy++c :: Proxy "c"+c = Proxy++type API = "send" :> Capture "from" LocTm :> ReqBody '[PlainText] String :> PostNoContent++httpSend :: Show a => LocTm -> Int -> a -> IO ()+httpSend sender targetPort a = liftIO $ do+    mgr <- newManager defaultManagerSettings+    res <- runClientM (client @API Proxy sender $ show a) $ mkClientEnv mgr $ BaseUrl Http "localhost" targetPort ""++    case res of+      Left err -> putStrLn $ "Error: " <> show err+      Right _  -> pure ()++    threadDelay 1000000++httpRecv :: Int -> IO (Maybe String)+httpRecv port = do+  ref <- newIORef Nothing++  recvThread <- forkIO do+    run port $ serve @API Proxy \_ msg -> do+      NoContent <$ liftIO (writeIORef ref $ Just msg)++  threadDelay 1000000+  killThread recvThread++  readIORef ref++-- "Frontrun" choreographic communication by sending data to the same port.+frontrun :: Choreo IO ()+frontrun = do+  locally a \_ -> do+    httpSend "a" 3001 False+    exitSuccess++  cond (a, wrap True) \case+    False -> pure ()+    True -> do+      (b, wrap 2) ~> c+      pure ()++-- Open an an "under-the-table" HTTP connecion between `a` and `b` to exfiltrate data from `c`.+collusion :: Choreo IO ()+collusion = do+  locally a \_ -> do+    v <- httpRecv 2999+    print v++  vb <- (c, wrap 2) ~> b++  locally b \unwrap -> do+    httpSend "b" 2999 $ unwrap vb++  pure ()++-- Helpers for running the choreographies++choreos :: [Choreo IO ()]+choreos = [frontrun, collusion]++-- Assigns different ports to each choreography so they can be run in parallel.+httpConfig :: Int -> [LocTm] -> HttpConfig+httpConfig choreo ls = mkHttpConfig [(l, ("localhost", port)) | l <- ls | port <- [3000 + 1000 * choreo..]]++main :: IO ()+main = do+  [read -> choreo, self] <- getArgs+  runChoreography (httpConfig choreo ["a", "b", "c"]) (choreos !! choreo) self

+ src/Choreography.hs view

@@ -0,0 +1,43 @@+{-# LANGUAGE ExplicitNamespaces #-}++-- | This module defines the interface to HasChor. The client of the library is+-- highly recommended to only use constructs exported by this module.+module Choreography (+  -- * Locations and Located Values+  LocTm,+  LocTy,+  type (@),+  mkLoc,++  -- * The Choreo monad+  Choreo,+  -- ** Choreo operations+  locally,+  (~>),+  (~~>),+  cond,+  cond',+  cond_,+  cond_',++  -- * Message transport backends+  -- ** The HTTP backend+  Host,+  Port,+  HttpConfig,+  mkHttpConfig,++  -- * Running choreographies+  runChoreo,+  runChoreography+  ) where++import Choreography.Location+import Choreography.Choreo+import Choreography.Network+import Choreography.Network.Http+import Control.Monad.IO.Class++-- | Run a choreography with a message transport backend.+runChoreography :: (Backend config, MonadIO m) => config -> Choreo m a -> LocTm -> m a+runChoreography cfg choreo l = runNetwork cfg l (epp (locs cfg) choreo l)

+ src/Choreography/Choreo.hs view

@@ -0,0 +1,190 @@+{-# LANGUAGE BlockArguments     #-}+{-# LANGUAGE GADTs              #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LambdaCase         #-}++-- | This module defines `Choreo`, the monad for writing choreographies.+module Choreography.Choreo where++import Control.Applicative(empty)+import Control.Monad.State.Strict(StateT, execStateT, modify')+import Data.Foldable(foldMap')+import Data.Functor(($>))+import Data.List(delete)+import Data.Maybe(fromMaybe)+import Data.Proxy(Proxy(..))+import Data.Set(Set)+import Data.Set qualified as S+import GHC.TypeLits(KnownSymbol)++import Choreography.Location+import Choreography.Network+import Control.Monad.Freer++-- * The Choreo monad++-- | A constrained version of `unwrap` that only unwraps values located at a+-- specific location.+type Unwrap l = forall a. a @ l -> a++-- | Effect signature for the `Choreo` monad. @m@ is a monad that represents+-- local computations.+data ChoreoSig m a where+  Local :: (KnownSymbol l)+        => Proxy l+        -> (Unwrap l -> m a)+        -> ChoreoSig m (a @ l)++  Comm :: (Show a, Read a, KnownSymbol l, KnownSymbol l')+       => Proxy l+       -> a @ l+       -> Proxy l'+       -> ChoreoSig m (a @ l')++  Cond :: (Show a, Read a, KnownSymbol l)+       => Proxy l+       -> a @ l+       -> (a -> Choreo m b)+       -> ChoreoSig m b++  Cond_ :: (Bounded a, Enum a, Show a, Read a, KnownSymbol l)+        => Proxy l+        -> a @ l+        -> (a -> Choreo m (b @ l))+        -> ChoreoSig m (b @ l)++-- | Monad for writing choreographies.+type Choreo m = Freer (ChoreoSig m)++-- | Run a `Choreo` monad directly.+runChoreo :: Monad m => Choreo m a -> m a+runChoreo = interpFreer handler+  where+    handler :: Monad m => ChoreoSig m a -> m a+    handler (Local _ m)   = wrap <$> m unwrap+    handler (Comm _ a _)  = return $ (wrap . unwrap) a+    handler (Cond _ a c)  = runChoreo $ c (unwrap a)+    handler (Cond_ _ a c) = runChoreo $ c (unwrap a)++-- Static analysis++insertLoc :: KnownSymbol l => Proxy l -> Set LocTm -> Set LocTm+insertLoc = S.insert . toLocTm++insertLocs :: [LocTm] -> Set LocTm -> Set LocTm+insertLocs = S.union . S.fromList++-- | Apply function `f` to every possible value of type `a`, and collect all the resulting `participants`.+enumerate :: (Bounded a, Enum a) => [LocTm] -> (a -> Choreo m b) -> Set LocTm+enumerate ls f = foldMap' (participants ls . f) [minBound ..]++-- | Compute the set of locations participating in this choreography.+participants :: [LocTm] -> Choreo m a -> Set LocTm+participants ls = fromMaybe (S.fromList ls) . (`execStateT` S.empty) . interpFreer handler+  where+    handler :: ChoreoSig m a -> StateT (Set LocTm) Maybe a+    handler = \case+      Local l _   -> modify' (insertLoc l)                $> Empty+      Comm l _ l' -> modify' (insertLoc l . insertLoc l') $> Empty+      Cond _ _ _  -> modify' (insertLocs ls)              *> empty+      Cond_ l _ f -> modify' (insertLoc l . S.union (enumerate ls f)) $> Empty++-- | Endpoint projection.+epp :: [LocTm] -> Choreo m a -> LocTm -> Network m a+epp ls c l' = interpFreer handler c+  where+    handler :: ChoreoSig m a -> Network m a+    handler (Local l m)+      | toLocTm l == l' = wrap <$> run (m unwrap)+      | otherwise       = return Empty+    handler (Comm s a r)+      | l' == s' && s' == r' = return $ wrap (unwrap a)+      | s' == l'             = send (unwrap a) r' >> return Empty+      | r' == l'             = wrap <$> recv s'+      | otherwise            = return Empty+      where+        s' = toLocTm s+        r' = toLocTm r+    handler (Cond l a c)+      | toLocTm l == l' = broadcast (unwrap a) (delete l' ls) >> epp ls (c (unwrap a)) l'+      | otherwise       = recv (toLocTm l) >>= \x -> epp ls (c x) l'+    handler (Cond_ pl a c)+      | l == l'         = broadcast (unwrap a) (S.toList $ S.delete l ls') >> epp ls (c (unwrap a)) l'+      | S.member l' ls' = recv l >>= \x -> epp ls (c x) l'+      | otherwise       = pure Empty+      where+        l = toLocTm pl+        ls' = enumerate ls c++-- * Choreo operations++-- | Perform a local computation at a given location.+locally :: KnownSymbol l+        => Proxy l           -- ^ Location performing the local computation.+        -> (Unwrap l -> m a) -- ^ The local computation given a constrained+                             -- unwrap funciton.+        -> Choreo m (a @ l)+locally l m = toFreer (Local l m)++-- | Communication between a sender and a receiver.+(~>) :: (Show a, Read a, KnownSymbol l, KnownSymbol l')+     => (Proxy l, a @ l)  -- ^ A pair of a sender's location and a value located+                          -- at the sender+     -> Proxy l'          -- ^ A receiver's location.+     -> Choreo m (a @ l')+(~>) (l, a) l' = toFreer (Comm l a l')++-- | Conditionally execute choreographies based on a located value.+cond :: (Show a, Read a, KnownSymbol l)+     => (Proxy l, a @ l)  -- ^ A pair of a location and a scrutinee located on+                          -- it.+     -> (a -> Choreo m b) -- ^ A function that describes the follow-up+                          -- choreographies based on the value of scrutinee.+     -> Choreo m b+cond (l, a) c = toFreer (Cond l a c)++-- | Conditionally execute choreographies at participating locations,+-- based on a located value.+cond_ :: (Bounded a, Enum a, Show a, Read a, KnownSymbol l)+      => (Proxy l, a @ l)        -- ^ A pair of a location and a scrutinee located on+                                 -- it.+      -> (a -> Choreo m (b @ l)) -- ^ A function that describes the follow-up+                                 -- choreographies based on the value of scrutinee.+      -> Choreo m (b @ l)+cond_ (l, a) c = toFreer (Cond_ l a c)++-- | A variant of `~>` that sends the result of a local computation.+(~~>) :: (Show a, Read a, KnownSymbol l, KnownSymbol l')+      => (Proxy l, Unwrap l -> m a) -- ^ A pair of a sender's location and a local+                                    -- computation.+      -> Proxy l'                   -- ^ A receiver's location.+      -> Choreo m (a @ l')+(~~>) (l, m) l' = do+  x <- l `locally` m+  (l, x) ~> l'++-- | A variant of `cond` that conditonally executes choregraphies based on the+-- result of a local computation.+cond' :: (Show a, Read a, KnownSymbol l)+      => (Proxy l, Unwrap l -> m a) -- ^ A pair of a location and a local+                                    -- computation.+      -> (a -> Choreo m b)          -- ^ A function that describes the follow-up+                                    -- choreographies based on the result of the+                                    -- local computation.+      -> Choreo m b+cond' (l, m) c = do+  x <- l `locally` m+  cond (l, x) c++-- | A variant of `cond_` that conditonally executes choregraphies at participating locations,+-- based on the result of a local computation.+cond_' :: (Bounded a, Enum a, Show a, Read a, KnownSymbol l)+       => (Proxy l, Unwrap l -> m a) -- ^ A pair of a location and a local+                                     -- computation.+       -> (a -> Choreo m (b @ l))    -- ^ A function that describes the follow-up+                                     -- choreographies based on the result of the+                                     -- local computation.+       -> Choreo m (b @ l)+cond_' (l, m) c = do+  x <- l `locally` m+  cond_ (l, x) c

+ src/Choreography/Location.hs view

@@ -0,0 +1,44 @@+{-# LANGUAGE DataKinds #-}++-- | This module defines locations and located values.+module Choreography.Location where++import Data.Proxy+import GHC.TypeLits+import Language.Haskell.TH++-- | Term-level locations.+type LocTm = String++-- | Type-level locations.+type LocTy = Symbol++-- | Convert a type-level location to a term-level location.+toLocTm :: forall (l :: LocTy). KnownSymbol l => Proxy l -> LocTm+toLocTm = symbolVal++-- | Located values.+--+-- @a \@ l@ represents a value of type @a@ at location @l@.+data a @ (l :: LocTy)+  = Wrap a -- ^ A located value @a \@ l@ from location @l@'s perspective.+  | Empty  -- ^ A located value @a \@ l@ from locations other than @l@'s+           -- perspective.++-- | Wrap a value as a located value.+wrap :: a -> a @ l+wrap = Wrap++-- | Unwrap a located value.+--+-- /Note:/ Unwrapping a empty located value will throw an exception.+unwrap :: a @ l-> a+unwrap (Wrap a) = a+unwrap Empty    = error "this should never happen for a well-typed choreography"++-- | Define a location at both type and term levels.+mkLoc :: String -> Q [Dec]+mkLoc loc = do+  let locName = mkName loc+  let p = mkName "Data.Proxy.Proxy"+  pure [SigD locName (AppT (ConT p) (LitT (StrTyLit loc))),ValD (VarP locName) (NormalB (ConE p)) []]

+ src/Choreography/Location/Multi.hs view

@@ -0,0 +1,79 @@+{-# LANGUAGE AllowAmbiguousTypes   #-}+{-# LANGUAGE BlockArguments        #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE ImpredicativeTypes    #-}+{-# LANGUAGE PartialTypeSignatures #-}+{-# LANGUAGE TypeFamilies          #-}++-- | This module defines multiply-located values and combinators for manipulating them.+module Choreography.Location.Multi where++import GHC.TypeLits(KnownSymbol)+import Data.Proxy(Proxy(..))+import Data.SOP.BasicFunctors(K(..), mapKK, unK)+import Data.SOP.Classes(HSequence(..), hmap)+import Data.SOP.Constraint(All)+import Data.SOP.NP(NP(..), hd, tl)++import Choreography.Choreo+import Choreography.Location++-- | The type of multiply-located values.+type a @@ ls = NP ((@) a) ls++-- | "scatter": Send a located value from a single location to many others.+(~>*) :: (KnownSymbol l, All KnownSymbol ls, Show a, Read a) => (Proxy l, a @ l) -> NP Proxy ls -> Choreo m (a @@ ls)+(l, a) ~>* ls = hctraverse' (Proxy @KnownSymbol) ((l, a) ~>) ls++infix 4 ~>*++-- | "gather": Send a multiply-located value from many locations to one.+(*~>) :: (KnownSymbol l, All KnownSymbol ls, Applicative m, Show a, Read a) => a @@ ls -> Proxy l -> Choreo m (NP (K a) ls @ l)+as *~> l = do+  as' <- hctraverse' (Proxy @KnownSymbol) (\a -> K <$> ((Proxy, a) ~> l)) as+  locally l \unwrap -> pure $ hmap (mapKK unwrap) as'++infix 4 *~>++-- | Send a list of values from one location to many others "pointwise" (i.e. each target gets one value).+(~>.) :: (KnownSymbol l, All KnownSymbol ls, Applicative m, Show a, Read a) => (Proxy l, NP (K a) ls @ l) -> NP Proxy ls -> Choreo m (a @@ ls)+_       ~>. Nil = pure Nil+(l, as) ~>. (l' :* ls') = do+  a <- locally l \unwrap -> pure $ unK $ hd $ unwrap as+  as' <- locally l \unwrap -> pure $ tl $ unwrap as+  (:*) <$> ((l, a) ~> l') <*> ((l, as') ~>. ls')++infix 4 ~>.++-- | Multiply-located version of `Unwrap`.+type Unwraps ls = forall a. a @@ ls -> a++-- | The type of a (multi)local computation.+type LocalComp ls m a = forall l. KnownSymbol l => Proxy l -> Unwraps ls -> m a++-- | Multiply-located version of `locally`.+multilocally :: forall ls m a. All KnownSymbol ls => NP Proxy ls -> LocalComp ls m a -> Choreo m (a @@ ls)+multilocally ls f = go ls id+  where+    go :: forall ls'. All KnownSymbol ls' => NP Proxy ls' -> (forall a. a @@ ls -> a @@ ls') -> Choreo m (a @@ ls')+    go Nil _pick = pure Nil+    go (l :* ls) pick = do+      a <- locally l \unwrap -> f l $ unwrap . hd . pick+      (a :*) <$> go ls (tl . pick)++-- | A variant of `~>*` that sends the result of a local computation.+(~~>*) :: (KnownSymbol l, All KnownSymbol ls, Show a, Read a) => (Proxy l, Unwrap l -> m a) -> NP Proxy ls -> Choreo m (a @@ ls)+(l, f) ~~>* ls = do+  a <- locally l f+  (l, a) ~>* ls++infix 4 ~~>*++-- | A variant of `*~>` that sends the result of a local computation.+(*~~>) :: (KnownSymbol l, All KnownSymbol ls, Applicative m, Show a, Read a) => (NP Proxy ls, LocalComp ls m a) -> Proxy l -> Choreo m (NP (K a) ls @ l)+(ls, f) *~~> l = do+  a <- multilocally ls f+  a *~> l++infix 4 *~~>

+ src/Choreography/Network.hs view

@@ -0,0 +1,61 @@+-- | 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.+module Choreography.Network where++import Choreography.Location+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+  -- | Broadcasting.+  BCast :: Show a+        => a+        -> [LocTm]+        -> NetworkSig m ()++-- | 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 l = toFreer $ Send a l++-- | Receive a message from a sender.+recv :: Read a => LocTm -> Network m a+recv l = toFreer $ Recv l++-- | Broadcast a message to all participants.+broadcast :: Show a => a -> [LocTm] -> Network m ()+broadcast a ls = toFreer $ BCast a ls++-- * 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+  locs :: c -> [LocTm]+  runNetwork :: MonadIO m => c -> LocTm -> Network m a -> m a

+ src/Choreography/Network/Http.hs view

@@ -0,0 +1,112 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs     #-}++-- | This module implments the HTTP message transport backend for the `Network`+-- monad.+module Choreography.Network.Http where++import Choreography.Location+import Choreography.Network hiding (run)+import Data.Proxy (Proxy(..))+import Data.HashMap.Strict (HashMap, (!))+import Data.HashMap.Strict qualified as HashMap+import Network.HTTP.Client (Manager, defaultManagerSettings, newManager)+import Servant.API hiding (Host)+import Servant.Client (ClientM, client, runClientM, BaseUrl(..), mkClientEnv, Scheme(..))+import Servant.Server (Handler, Server, serve)+import Control.Concurrent+import Control.Monad+import Control.Monad.Freer+import Control.Monad.IO.Class+import Network.Wai.Handler.Warp (run)++-- * Servant API++type API = "send" :> Capture "from" LocTm :> ReqBody '[PlainText] String :> PostNoContent++-- * Http configuration++-- | The HTTP backend configuration specifies how locations are mapped to+-- network hosts and ports.+newtype HttpConfig = HttpConfig+  { locToUrl :: HashMap LocTm BaseUrl+  }++type Host = String+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 = ""+      }++locsHttp :: HttpConfig -> [LocTm]+locsHttp = HashMap.keys . locToUrl++-- * Receiving channels++type RecvChans = HashMap LocTm (Chan String)++mkRecvChans :: HttpConfig -> IO RecvChans+mkRecvChans cfg = foldM f HashMap.empty (locsHttp cfg)+  where+    f :: HashMap LocTm (Chan String) -> LocTm+      -> IO (HashMap LocTm (Chan String))+    f hm l = do+      c <- newChan+      return $ HashMap.insert l c hm++-- * 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+  return 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 l)   = liftIO $ do+          res <- runClientM (send self $ show a) (mkClientEnv mgr (locToUrl cfg ! l))+          case res of+            Left err -> putStrLn $ "Error : " ++ show err+            Right _  -> return ()+        handler (Recv l)     = liftIO $ read <$> readChan (chans ! l)+     -- handler (Recv l)     = liftIO $ putStrLn ("Recv from " <> l) *> (read <$> readChan (chans ! l))+        handler (BCast a ls) = mapM_ handler $ fmap (Send a) ls++    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+          return NoContent++    recvThread :: HttpConfig -> RecvChans -> IO ()+    recvThread cfg chans = run (baseUrlPort $ locToUrl cfg ! self ) (serve api $ server chans)++instance Backend HttpConfig where+  locs = locsHttp+  runNetwork = runNetworkHttp

+ src/Choreography/Network/Local.hs view

@@ -0,0 +1,51 @@+{-# LANGUAGE GADTs #-}++-- | This module defines the multi-thread backend for the `Network` monad.+module Choreography.Network.Local where++import Choreography.Location+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)++newtype LocalConfig = LocalConfig+  { locToBuf :: HashMap LocTm MsgBuf+  }++newEmptyMsgBuf :: [LocTm] -> IO MsgBuf+newEmptyMsgBuf = foldM f HashMap.empty+  where+    f hash loc = do+      chan <- newChan+      return (HashMap.insert loc chan hash)++mkLocalConfig :: [LocTm] -> IO LocalConfig+mkLocalConfig locs = LocalConfig <$> foldM f HashMap.empty locs+  where+    f hash loc = do+      buf <- newEmptyMsgBuf locs+      return (HashMap.insert loc buf hash)++locsLocal :: LocalConfig -> [LocTm]+locsLocal = HashMap.keys . locToBuf++runNetworkLocal :: MonadIO m => LocalConfig -> LocTm -> Network m a -> m a+runNetworkLocal cfg self prog = interpFreer handler prog+  where+    handler :: MonadIO m => NetworkSig m a -> m a+    handler (Run m)      = m+    handler (Send a l)   = liftIO $ writeChan ((locToBuf cfg ! l) ! self) (show a)+    handler (Recv l)     = liftIO $ read <$> readChan ((locToBuf cfg ! self) ! l)+    handler (BCast a ls) = mapM_ handler $ fmap (Send a) ls++instance Backend LocalConfig where+  locs = locsLocal+  runNetwork = runNetworkLocal

+ src/Choreography/Network/LocalMsgCount.hs view

@@ -0,0 +1,57 @@+{-# LANGUAGE GADTs #-}++-- | This module defines an instrumented version of the `Local` backend,+-- which counts how many `Send` operations are performed during execution of the choreography.+-- It is used by the benchmarks in `bench/`.+module Choreography.Network.LocalMsgCount where++import Choreography.Location+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+import Data.IORef++-- | Each location is associated with a message buffer which stores messages sent+-- from other locations.+type MsgBuf = HashMap LocTm (Chan String)++data LocalMsgCountConfig = LocalMsgCountConfig+  { msgCounter :: IORef Int+  , locToBuf :: HashMap LocTm MsgBuf+  }++newEmptyMsgBuf :: [LocTm] -> IO MsgBuf+newEmptyMsgBuf = foldM f HashMap.empty+  where+    f hash loc = do+      chan <- newChan+      return (HashMap.insert loc chan hash)++mkLocalMsgCountConfig :: IORef Int -> [LocTm] -> IO LocalMsgCountConfig+mkLocalMsgCountConfig msgCounter locs = LocalMsgCountConfig msgCounter <$> foldM f HashMap.empty locs+  where+    f hash loc = do+      buf <- newEmptyMsgBuf locs+      return (HashMap.insert loc buf hash)++locsLocalMsgCount :: LocalMsgCountConfig -> [LocTm]+locsLocalMsgCount = HashMap.keys . locToBuf++runNetworkLocalMsgCount :: MonadIO m => LocalMsgCountConfig -> LocTm -> Network m a -> m a+runNetworkLocalMsgCount cfg self prog = interpFreer handler prog+  where+    handler :: MonadIO m => NetworkSig m a -> m a+    handler (Run m)      = m+    handler (Send a l)   = liftIO $ do+      atomicModifyIORef' (msgCounter cfg) (\c -> (c + 1, ()))+      writeChan ((locToBuf cfg ! l) ! self) (show a)+    handler (Recv l)     = liftIO $ read <$> readChan ((locToBuf cfg ! self) ! l)+    handler (BCast a ls) = mapM_ handler $ fmap (Send a) ls++instance Backend LocalMsgCountConfig where+  locs = locsLocalMsgCount+  runNetwork = runNetworkLocalMsgCount

+ src/Control/Monad/Freer.hs view

@@ -0,0 +1,43 @@+-- | This module defines the freer monad `Freer`, which allows manipulating+-- effectful computations algebraically.+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 a. f a -> m a) -> Freer f a -> m a+interpFreer _handler (Return a) = return a+interpFreer handler (Do eff k) = handler eff >>= interpFreer handler . k