Merge pull request #10 from ShapeOfMatter/better_example_monad

Better example monad

HasChor.cabal

@@ -49,7 +49,7 @@ library choreography
         Choreography.Network.Http
         Choreography.Network.Local
         Control.Monad.Freer
-        TTY
+        CLI
 
 common lib-dependent
     import: basic-config

examples/Bank2PC.hs

@@ -46,8 +46,15 @@ Bob's balance: 5
 module Bank2PC where
 
 import Choreography
+import CLI
+import Control.Monad (unless)
+import Data (TestArgs, reference)
+import Data.List (intercalate, transpose)
 import Data.List.Split (splitOn)
 import Data.Maybe (mapMaybe)
+import Data.Proxy (Proxy(Proxy))
+import GHC.TypeLits (KnownSymbol, symbolVal)
+import Test.QuickCheck (Arbitrary, arbitrary, elements, listOf, listOf1)
 import Text.Read (readMaybe)
 
 $(mkLoc "client")
@@ -62,13 +69,37 @@ type Action = (String, Int)
 
 type Transaction = [Action]
 
+newtype Args p q = Args [Transaction] deriving (Eq, Show, Read)
+instance (KnownSymbol p, KnownSymbol q) => TestArgs (Args p q) [[String]] where
+ reference (Args tx) = addCoordinator . transpose $ showAll <$> ref start tx
+   where start = (, 0) <$> [symbolVal (Proxy @p), symbolVal (Proxy @q)]
+         ref _ [] = []
+         ref state (t:ts) = let (s', r) = refAs state t
+                                s'' = if r then s' else state
+                            in (r, s'') : ref s'' ts
+         refAs state [] = (state, True)
+         refAs state (a:as) = let (s', r) = refA state a
+                              in if r then refAs s' as else (state, False)
+         refA state (name, amount) = let (otherL, (_, s):otherR) = ((== name) . fst) `break` state
+                                         s' = s + amount
+                                     in (otherL ++ ((name, s'):otherR), 0 <= s')
+         showAll :: (Bool, [(String, Int)]) -> [String]
+         showAll (clnt, servers) = show clnt : (show . snd <$> servers)
+         addCoordinator (clnt:servers) = clnt : [] : servers
+         addCoordinator _ = error "this can't happen, right? I could enforce it by types, but it's a core..."
+instance (KnownSymbol p, KnownSymbol q) => Arbitrary (Args p q) where
+  arbitrary = (Args . (++ [[]]) <$>) . listOf . listOf1 $ (,) <$> elements [symbolVal $ Proxy @p, symbolVal $ Proxy @q] <*> arbitrary
+
 -- | `validate` checks if a transaction can be executed while keeping balance >= 0
 -- returns if the transaction satisfies the property and the balance after the transaction
 validate :: String -> Int -> Transaction -> (Bool, Int)
 validate name balance tx = foldl (\(valid, i) (_, amount) -> (let next = i + amount in (valid && next >= 0, next))) (True, balance) actions
   where
     actions = filter (\(n, _) -> n == name) tx
 
+render :: Transaction -> String
+render txns = intercalate ";" $ (\(a,b) -> a ++ " " ++ show b) <$> txns
+
 -- | `parse` converts the user input into a transaction
 parse :: String -> Transaction
 parse s = tx
@@ -87,7 +118,10 @@ parse s = tx
 -- 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 Participants IO (Bool @ "coordinator", State)
+handleTransaction :: (Monad m) =>
+                     State ->
+                     Transaction @ "coordinator" ->
+                     Choreo Participants m (Bool @ "coordinator", State)
 handleTransaction (aliceBalance, bobBalance) tx = do
   -- Voting Phase
   txa <- (coordinator, tx) ~> alice
@@ -108,27 +142,24 @@ handleTransaction (aliceBalance, bobBalance) tx = do
       return (canCommit, (aliceBalance, bobBalance))
 
 -- | `bank` loops forever and handles transactions.
-bank :: State -> Choreo Participants IO ()
+bank :: State -> Choreo Participants (CLI m) ()
 bank state = do
-  client `locally_` \_ -> do
-    putStrLn "Command? (alice|bob {amount};)+"
-  tx <- (client, \_ -> do { parse <$> getLine }) ~~> coordinator
+  tx <- (client, \_ -> parse <$> getstr "Command? (alice|bob {amount};)+"
+        ) ~~> coordinator
   (committed, state') <- handleTransaction state tx
   committed' <- (coordinator, committed) ~> client
-  client `locally_` \un -> do
-    putStrLn if un committed' then "Committed" else "Not committed"
-  alice `locally_` \un -> do putStrLn ("Alice's balance: " ++ show (un (fst state')))
-  bob `locally_` \un -> do putStrLn ("Bob's balance: " ++ show (un (snd state')))
-  bank state' -- repeat
-  return ()
+  client `locally_` \un -> putOutput "Committed?" (un committed')
+  alice `locally_` \un -> putOutput "Alice's balance:" (un (fst state'))
+  bob `locally_` \un -> putOutput "Bob's balance:" (un (snd state'))
+  cond' (coordinator, \un -> return $ null $ un tx) (`unless` bank state') -- repeat
 
 -- | `startBank` is a choreography that initializes the states and starts the bank application.
-startBank :: Choreo Participants IO ()
+startBank :: Choreo Participants (CLI m) ()
 startBank = do
-  aliceBalance <- alice `locally` \_ -> do return 0
-  bobBalance <- bob `locally` \_ -> do return 0
+  aliceBalance <- alice `_locally` return 0
+  bobBalance <- bob `_locally` return 0
   bank (aliceBalance, bobBalance)
 
 main :: IO ()
 main = do
-  runChoreo startBank
+  runCLIIO $ runChoreo startBank

examples/Bookseller0Network.hs

@@ -15,46 +15,45 @@ Same as [`bookseller-1-simple`](../bookseller-1-simple) but with `cabal run book
 
 import Choreography.Network
 import Choreography.Network.Http
+import CLI
 import Data.Time
 import System.Environment
 
-import Data (Database, defaultBudget, deliveryDateOf, priceOf, textbooks)
+import Data (deliveryDateOf, priceOf)
 
-buyer :: Int -> String -> Network IO (Maybe Day)
-buyer budget title = do
+buyer :: Network (CLI m) ()
+buyer = do
+  budget <- run $ getInput @Int "Enter your total budget:"
+  title <- run $ getstr "Enter the title of the book to buy:"
   send title "seller"
   price <- recv "seller"
-  if price < budget
+  if price <= budget
   then do
     send True "seller"
     (deliveryDate :: Day) <- recv "seller"
-    return $ Just deliveryDate
+    run $ putOutput "The book will be delivered on:" deliveryDate
   else do
     send False "seller"
-    return Nothing
+    run $ putNote "The book's price is out of the budget"
 
-seller :: Database -> Network IO ()
-seller books = do
+seller :: Network (CLI m) ()
+seller = do
+  database <- run $ getInput "Enter the book database (for `Read`):"
   title <- recv "buyer"
-  send (priceOf books title) "buyer"
+  send (database `priceOf` title) "buyer"
   decision <- recv "buyer"
   if decision
   then do
-    send (deliveryDateOf books title) "buyer"
+    send (database `deliveryDateOf` title) "buyer"
   else do
     return ()
 
 main :: IO ()
 main = do
   [loc] <- getArgs
   case loc of
-    "buyer" -> do putStrLn "Enter the title of the book to buy:"
-                  title <- getLine
-                  result <- runNetwork cfg "buyer" $ buyer defaultBudget title
-                  case result of
-                    Nothing -> putStrLn "The book's price is out of the budget"
-                    Just day -> putStrLn ("The book will be delivered on " ++ show day)
-    "seller" -> runNetwork cfg "seller" $ seller textbooks
+    "buyer" -> runCLIIO $ runNetwork cfg "buyer" buyer
+    "seller" -> runCLIIO $ runNetwork cfg "seller" seller
     _ -> error "unknown party"
   return ()
   where

examples/Bookseller1Simple.hs

@@ -67,82 +67,57 @@ Homotopy Type Theory
 module Bookseller1Simple where
 
 import Choreography
-import Data.Time
 import System.Environment
 
-import Data (defaultBudget, deliveryDateOf, priceOf, textbooks)
+import Data (deliveryDateOf, priceOf)
+import CLI
 
 $(mkLoc "buyer")
 $(mkLoc "seller")
 type Participants = ["buyer", "seller"]
 
 -- | `bookseller` is a choreography that implements the bookseller protocol.
-bookseller :: String -> Choreo Participants IO (Maybe Day)
-bookseller userTitle = do
-  -- the buyer node prompts the user to enter the title of the book to buy
-  title <- buyer `locally` \_ -> return userTitle
-  -- the buyer sends the title to the seller
-  title' <- (buyer, title) ~> seller
+bookseller :: Choreo Participants (CLI m) ()
+bookseller = do
+  database <- seller `_locally` getInput "Enter the book database (for `Read`):"
+  buyer_budget <- buyer `_locally` getInput "Enter your total budget:"
+  title <- buyer `_locally` getstr "Enter the title of the book to buy:"
 
-  -- the seller checks the price of the book
-  price <- seller `locally` \un -> return $ priceOf textbooks (un title')
-  -- the seller sends back the price of the book to the buyer
+  title' <- (buyer, title) ~> seller
+  price <- seller `locally` \un -> return $ priceOf (un database) (un title')
   price' <- (seller, price) ~> buyer
+  decision <- buyer `locally` \un -> return $ un price' <= un buyer_budget
 
-  -- 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
-  delivery <- cond (buyer, decision) \case
+  cond (buyer, decision) \case
     True  -> do
-      deliveryDate  <- seller `locally` \un -> return $ deliveryDateOf textbooks (un title')
+      deliveryDate  <- seller `locally` \un -> return $ deliveryDateOf (un database) (un title')
       deliveryDate' <- (seller, deliveryDate) ~> buyer
-
-      buyer `locally` \un -> do
-        putStrLn $ "The book will be delivered on " ++ show (un deliveryDate')
-        return $ Just (un deliveryDate')
-
+      buyer `locally_` \un -> putOutput "The book will be delivered on " $ un deliveryDate'
     False -> do
-      buyer `locally` \_ -> do
-        putStrLn "The book's price is out of the budget"
-        return Nothing
-  reveal buyer delivery
+      buyer `_locally_` putNote "The book's price is out of the budget"
 
 -- `bookseller'` is a simplified version of `bookseller` that utilizes `~~>`
-bookseller' :: String -> Choreo Participants IO (Maybe Day)
-bookseller' userTitle = do
-  title <- (buyer, \_ -> do
-               return userTitle
-           )
-           ~~> seller
-
-  price <- (seller, \un -> return $ priceOf textbooks (un title)) ~~> buyer
-
-  delivery <- cond' (buyer, \un -> return $ un price < budget) \case
+bookseller' :: Choreo Participants (CLI m) ()
+bookseller' = do
+  database <- seller `_locally` getInput "Enter the book database (for `Read`):"
+  buyer_budget <- buyer `_locally` getInput "Enter your total budget:"
+  title <- (buyer, \_ -> getstr "Enter the title of the book to buy:") ~~> seller
+  price <- (seller, \un -> return $ priceOf (un database) (un title)) ~~> buyer
+
+  cond' (buyer, \un -> return $ un price <= un buyer_budget) \case
     True  -> do
-      deliveryDate <- (seller, \un -> return $ deliveryDateOf textbooks (un title)) ~~> buyer
-
-      buyer `locally` \un -> do
-        putStrLn $ "The book will be delivered on " ++ show (un deliveryDate)
-        return $ Just (un deliveryDate)
-
+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un database) (un title)) ~~> buyer
+      buyer `locally_` \un -> putOutput "The book will be delivered on:" $ un deliveryDate
     False -> do
-      buyer `locally` \_ -> do
-        putStrLn "The book's price is out of the budget"
-        return Nothing
-  reveal buyer delivery
+      buyer `_locally_` putNote "The book's price is out of the budget"
 
-budget :: Int
-budget = defaultBudget
 
 main :: IO ()
 main = do
   [loc] <- getArgs
-  putStrLn "Enter the title of the book to buy"
-  title <- getLine
   delivery <- case loc of
-    "buyer"  -> runChoreography cfg (bookseller' title) "buyer"
-    "seller" -> runChoreography cfg (bookseller' title) "seller"
+    "buyer"  -> runCLIIO $ runChoreography cfg bookseller' "buyer"
+    "seller" -> runCLIIO $ runChoreography cfg bookseller' "seller"
     _ -> error "unknown party"
   print delivery
   where

examples/Bookseller2HigherOrder.hs

@@ -53,13 +53,11 @@ but with buyer2's contribution, now it can.
 
 module Bookseller2HigherOrder where
 
-import Control.Monad.Cont (MonadIO(liftIO))
 import Choreography
-import Data.Time
 import System.Environment
 
-import TTY
-import Data
+import CLI
+import Data (deliveryDateOf, priceOf)
 
 $(mkLoc "buyer")
 $(mkLoc "seller")
@@ -69,62 +67,47 @@ type Participants = ["buyer", "seller", "buyer2"]
 
 -- | `bookseller` is a choreography that implements the bookseller protocol.
 -- This version takes a choreography `mkDecision` that implements the decision making process.
-bookseller :: (Int @ "buyer" -> Choreo Participants (TTY IO) (Bool @ "buyer")) -> Choreo Participants (TTY IO) (Maybe Day @ "buyer")
+bookseller :: (Int @ "buyer" -> Choreo Participants (CLI m) (Bool @ "buyer")) -> Choreo Participants (CLI m) ()
 bookseller mkDecision = do
-  -- the buyer reads the title of the book and sends it to the seller
-  title <- (buyer, \_ -> do
-               liftIO $ putStrLn "Enter the title of the book to buy"
-               getln
-           )
-           ~~> seller
+  database <- seller `_locally` getInput "Enter the book database (for `Read`):"
+  title <- (buyer, \_ -> getstr "Enter the title of the book to buy:") ~~> seller
 
   -- the seller checks the price of the book and sends it to the buyer
-  price <- (seller, \un -> return $ priceOf textbooks (un title)) ~~> buyer
+  price <- (seller, \un -> return $ priceOf (un database) (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 textbooks (un title)) ~~> buyer
-
-      buyer `locally` \un -> do
-        liftIO $ putStrLn "The book will be delivered on:"
-        putln $ show (un deliveryDate)
-        return $ Just (un deliveryDate)
+      deliveryDate <- (seller, \un -> return $ deliveryDateOf (un database) (un title)) ~~> buyer
+      buyer `locally_` \un -> putstr "The book will be delivered on:" $ show (un deliveryDate)
 
     False -> do
-      buyer `locally` \_ -> do
-        liftIO $ putStrLn "The book's price is out of the budget"
-        return Nothing
+      buyer `locally_` \_ -> putNote "The book's price is out of the budget"
 
 -- | `mkDecision1` checks if buyer's budget is greater than the price of the book
-mkDecision1 :: Int @ "buyer" -> Choreo Participants (TTY IO) (Bool @ "buyer")
+mkDecision1 :: Int @ "buyer" -> Choreo Participants (CLI m) (Bool @ "buyer")
 mkDecision1 price = do
-  buyer `locally` \un -> return $ un price < budget
+  budget <- buyer `_locally` getInput "What are you willing to pay?"
+  buyer `locally` \un -> return $ un price <= un 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 Participants (TTY IO) (Bool @ "buyer")
+mkDecision2 :: Int @ "buyer" -> Choreo Participants (CLI m) (Bool @ "buyer")
 mkDecision2 price = do
-  contrib <- (buyer2, \_ -> do
-                 liftIO $ putStrLn "How much you're willing to contribute?"
-                 read <$> getln
-             )
-             ~~> buyer
-  buyer `locally` \un -> return $ un price - un contrib <= budget
-
-budget :: Int
-budget = defaultBudget
+  contrib1 <- buyer `_locally` getInput "What are you willing to pay?"
+  contrib2 <- (buyer2, \_ -> getInput "How much you're willing to contribute?") ~~> buyer
+  buyer `locally` \un -> return $ un price - un contrib2 <= un contrib1
 
 main :: IO ()
 main = do
   [loc] <- getArgs
   _ <- case loc of
-    "buyer"  -> runTTYIO $ runChoreography cfg choreo "buyer"
-    "seller" -> runTTYIO $ runChoreography cfg choreo "seller"
-    "buyer2" -> runTTYIO $ runChoreography cfg choreo "buyer2"
+    "buyer"  -> runCLIIO $ runChoreography cfg choreo "buyer"
+    "seller" -> runCLIIO $ runChoreography cfg choreo "seller"
+    "buyer2" -> runCLIIO $ runChoreography cfg choreo "buyer2"
     _ -> error "unknown party"
   return ()
   where