Known lists

MultiChor.cabal

@@ -1,6 +1,6 @@
 cabal-version:      3.0
 name:               MultiChor
-version:            1.1.0.0
+version:            2.0.0.0
 license-files:
     , LICENSE
     , LICENSE.inherited
@@ -28,6 +28,7 @@ common basic-config
         , base                 >= 4.16 && < 5
         , bytestring           >= 0.11 && < 0.13
         , http-client          >= 0.7  && < 0.8
+        , known-lists          >= 0.0
         , mtl                  >= 2.2.2 && < 3.0
         , servant              >= 0.19 && < 0.21
         , servant-client       >= 0.19 && < 0.21
@@ -51,6 +52,8 @@ common basic-config
                        ,LiberalTypeSynonyms
                        ,OverloadedLists
                        ,TypeFamilies
+                       ,UndecidableInstances
+
 
 library
     import: basic-config
@@ -60,8 +63,6 @@ library
         Choreography.Choreography
         Choreography.Choreography.Batteries
         Choreography.Core
-        Choreography.Locations
-        Choreography.Locations.Batteries
         Choreography.Network
         Choreography.Network.Http
         Choreography.Network.Local

README.md

@@ -45,7 +45,7 @@ Consider the choreography `game`:
 {- A simple black-jack-style game. The dealer gives everyone a card, face up. Each player may
  - request a second card. Then the dealer reveals one more card that applies to everyone. Each
  - player individually wins if the sum of their cards (modulo 21) is greater than 19.  -}
-game :: forall players m. (KnownSymbols players) => Choreo ("dealer" ': players) (CLI m) ()
+game :: forall players m. (Known [Party] players) => Choreo ("dealer" ': players) (CLI m) ()
 game = do
   let players = consSuper (refl @players)
       dealer = listedFirst @"dealer"

examples/Auction.hs

@@ -5,7 +5,10 @@ import Choreography
 import Data (TestArgs, reference, unsafeQuietHead)
 import Data.Foldable (toList)
 import Data.Function (on)
+import Data.Known.Knowable
 import Data.List (groupBy, sortBy)
+import Data.Known.Membership
+import Data.Known.TypeIndexed
 import EasyMain (easyMain)
 import System.Random (randomRIO)
 import Test.QuickCheck (Arbitrary, arbitrary)
@@ -34,7 +37,7 @@ auction = do
   submittedBids <- gather buyers (seller @@ proctor @@ nobody) ownBid
   orderedBids <- congruently (seller @@ proctor @@ nobody) \un ->
     let bids = un refl submittedBids
-        collated = stackLeaves \b -> (toLocTm b, getLeaf bids b)
+        collated = pack @Buyers \b -> (toValue b, bids ! b)
         sorter a b = compare (snd b) (snd a)
     in sortBy sorter $ toList collated
   winners <- conclaveTo (seller @@ proctor @@ nobody) (First @@ nobody) do
@@ -50,12 +53,12 @@ auction = do
           let winners = fst <$>
                           (unsafeQuietHead $ groupBy (on (==) snd) $ un listedSecond orderedBids)
           (winners !!) <$> randomRIO (0, length winners - 1)
-        winner <- broadcast (listedSecond @Proctor, (singleton @Proctor, winner'))
+        winner <- broadcast (listedSecond @Proctor, (alone @Proctor, winner'))
         purely First \un ->
           let ((a, bid) : (b, _) : _) = un First orderedBids
               second = if a == winner then b else a
           in ((winner, bid), (second, bid))
-  ((wName, _), (_, sBid)) <- broadcast (seller, (singleton @Seller, winners))
+  ((wName, _), (_, sBid)) <- broadcast (seller, (alone @Seller, winners))
   parallel_ allOf \_ _ -> putOutput "Result:" (wName, sBid)
 
 
@@ -71,7 +74,7 @@ data Args = Args
   }
   deriving (Eq, Show, Read)
 
-instance TestArgs Args ([LocTm], Bid) where
+instance TestArgs Args ([PartyName], Bid) where
   reference Args {b1, b2, b3, b4, b5} =
     let bids@((_, wBid) : (_, sBid) : _) =
             sortBy (on (flip compare) snd) $

examples/Bank2PC.hs

@@ -63,15 +63,20 @@ import Data (TestArgs, reference)
 import Data.List (intercalate, transpose)
 import Data.List.Split (splitOn)
 import Data.Maybe (mapMaybe)
+import Data.Known.Knowable
+import Data.Known.Membership
 import Data.Proxy (Proxy (Proxy))
-import GHC.TypeLits (KnownSymbol, symbolVal)
 import Test.QuickCheck (Arbitrary, arbitrary, elements, listOf, listOf1)
 import Text.Read (readMaybe)
 
-$(mkLoc "client")
-$(mkLoc "coordinator")
-$(mkLoc "alice")
-$(mkLoc "bob")
+client :: forall ps. ExplicitMember "client" ps => Member "client" ps
+client = explicitMember
+coordinator :: forall ps. ExplicitMember "coordinator" ps => Member "coordinator" ps
+coordinator = explicitMember
+alice :: forall ps. ExplicitMember "alice" ps => Member "alice" ps
+alice = explicitMember
+bob :: forall ps. ExplicitMember "bob" ps => Member "bob" ps
+bob = explicitMember
 
 type Participants = ["client", "coordinator", "alice", "bob"]
 
@@ -83,10 +88,10 @@ type Transaction = [Action]
 
 newtype Args p q = Args [Transaction] deriving (Eq, Show, Read)
 
-instance (KnownSymbol p, KnownSymbol q) => TestArgs (Args p q) [[String]] where
+instance (Known Party p, Known Party 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)]
+      start = (,0) <$> [toValue (Proxy @p), toValue (Proxy @q)]
       ref _ [] = []
       ref state (t : ts) =
         let (s', r) = refAs state t
@@ -105,8 +110,8 @@ instance (KnownSymbol p, KnownSymbol q) => TestArgs (Args p q) [[String]] where
       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
+instance (Known Party p, Known Party q) => Arbitrary (Args p q) where
+  arbitrary = (Args . (++ [[]]) <$>) . listOf . listOf1 $ (,) <$> elements [toValue $ Proxy @p, toValue $ 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

examples/Bookseller1Simple.hs

@@ -9,10 +9,13 @@ import CLI
 import Choreography
 import Choreography.Network.Http
 import Data (deliveryDateOf, priceOf)
+import Data.Known.Membership
 import System.Environment
 
-$(mkLoc "buyer")
-$(mkLoc "seller")
+buyer :: forall ps. ExplicitMember "buyer" ps => Member "buyer" ps
+buyer = explicitMember
+seller :: forall ps. ExplicitMember "seller" ps => Member "seller" ps
+seller = explicitMember
 
 type Participants = ["buyer", "seller"]
 

examples/Bookseller2HigherOrder.hs

@@ -57,13 +57,17 @@ import CLI
 import Choreography
 import Choreography.Network.Http
 import Data (deliveryDateOf, priceOf)
+import Data.Known.Membership
 import System.Environment
 
-$(mkLoc "buyer")
-$(mkLoc "seller")
-$(mkLoc "buyer2")
-
 type Participants = ["buyer", "seller", "buyer2"]
+buyer :: forall ps. ExplicitMember "buyer" ps => Member "buyer" ps
+buyer = explicitMember
+seller :: forall ps. ExplicitMember "seller" ps => Member "seller" ps
+seller = explicitMember
+buyer2 :: forall ps. ExplicitMember "buyer2" ps => Member "buyer2" ps
+buyer2 = explicitMember
+
 
 -- | `bookseller` is a choreography that implements the bookseller protocol.
 -- This version takes a choreography `mkDecision` that implements the decision making process.

examples/Bookseller3LocPoly.hs

@@ -22,17 +22,20 @@ import CLI
 import Choreography
 import Choreography.Network.Http
 import Data (deliveryDateOf, priceOf)
-import GHC.TypeLits
+import Data.Known.Knowable
+import Data.Known.Membership
 import System.Environment
 
-$(mkLoc "buyer")
-$(mkLoc "seller")
+buyer :: forall ps. ExplicitMember "buyer" ps => Member "buyer" ps
+buyer = explicitMember
+seller :: forall ps. ExplicitMember "seller" ps => Member "seller" ps
+seller = explicitMember
 
 -- type Participants = ["buyer", "seller"]
 
 -- | `bookseller` is a choreography that implements the bookseller protocol.
 -- This version takes the name of the buyer as a parameter (`someBuyer`).
-bookseller :: (KnownSymbol a, KnownSymbols ps) => Member a ps -> Choreo ("seller" ': ps) (CLI m) ()
+bookseller :: (Known Party a, Known [Party] ps) => Member a ps -> Choreo ("seller" ': ps) (CLI m) ()
 bookseller someBuyer = do
   let theBuyer = inSuper consSet someBuyer
   database <- seller `_locally` getInput "Enter the book database (for `Read`):"
@@ -42,12 +45,12 @@ bookseller someBuyer = do
   -- the seller checks the price of the book and sends it to the buyer
   price <- (seller, \un -> return $ priceOf (un seller database) (un seller title)) ~~> theBuyer @@ nobody
 
-  inBuyerBudget <- theBuyer `locally` (\un -> return $ un singleton price <= un singleton buyer_budget)
+  inBuyerBudget <- theBuyer `locally` (\un -> return $ un alone price <= un alone buyer_budget)
   broadcast (theBuyer, inBuyerBudget) >>= \case
     True -> do
       deliveryDate <- (seller, \un -> return $ deliveryDateOf (un seller database) (un seller title)) ~~> theBuyer @@ nobody
 
-      theBuyer `locally_` \un -> putOutput "The book will be delivered on:" $ un singleton deliveryDate
+      theBuyer `locally_` \un -> putOutput "The book will be delivered on:" $ un alone deliveryDate
     False -> do
       theBuyer `_locally_` putNote "The book's price is out of the budget"
 
@@ -60,7 +63,7 @@ main = do
     _ -> error "unknown party"
   return ()
   where
-    choreo = bookseller $ singleton @"buyer"
+    choreo = bookseller $ alone @"buyer"
 
     cfg =
       mkHttpConfig

examples/BooksellerFancy.hs

@@ -13,16 +13,20 @@ import CLI
 import Choreography
 import Choreography.Network.Http
 import Data (deliveryDateOf, priceOf)
+import Data.Known.Knowable
+import Data.Known.Membership
 import System.Environment
 
-$(mkLoc "buyer")
-$(mkLoc "seller")
+buyer :: forall ps. ExplicitMember "buyer" ps => Member "buyer" ps
+buyer = explicitMember
+seller :: forall ps. ExplicitMember "seller" ps => Member "seller" ps
+seller = explicitMember
 
 -- | `bookseller` is a choreography that implements the bookseller protocol.
 -- This version takes a choreography `mkDecision` that implements the decision making process.
 bookseller ::
   forall supporters {m}.
-  (KnownSymbols supporters) =>
+  (Known [Party] supporters) =>
   (Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool)) ->
   Choreo ("buyer" ': "seller" ': supporters) (CLI m) ()
 bookseller mkDecision = do
@@ -61,7 +65,7 @@ mkDecision1 price = do
 
 -- | `mkDecision2` asks supporters how much they're willing to contribute and checks
 -- if the buyer's budget is greater than the price of the book minus all supporters' contribution
-mkDecision2 :: forall supporters {m}. (KnownSymbols supporters) => Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool)
+mkDecision2 :: forall supporters {m}. (Known [Party] supporters) => Located '["buyer"] Int -> Choreo ("buyer" ': supporters) (CLI m) (Located '["buyer"] Bool)
 mkDecision2 price = do
   budget <- buyer `_locally` getInput "What are you willing to pay?"
 

examples/CardGame.hs

@@ -11,6 +11,9 @@ import Control.Concurrent.Async (mapConcurrently)
 import Control.Monad (void)
 import Data (TestArgs, unsafeQuietHead, unsafeQuietTail, reference)
 import Data.Foldable (forM_)
+import Data.Known.Knowable
+import Data.Known.Membership
+import Data.Known.TypeIndexed
 import Test.QuickCheck (Arbitrary, arbitrary, listOf1)
 
 _modulo :: Int -> Int
@@ -56,14 +59,14 @@ instance Arbitrary Args where
 {- A simple black-jack-style game. The dealer gives everyone a card, face up. Each player may
  - request a second card. Then the dealer reveals one more card that applies to everyone. Each
  - player individually wins if the sum of their cards (modulo 21) is greater than 19.  -}
-game :: forall players m. (KnownSymbols players) => Choreo ("dealer" ': players) (CLI m) ()
+game :: forall players m. (Known [Party] players) => Choreo ("dealer" ': players) (CLI m) ()
 game = do
   let players = consSuper (refl @players)
       dealer = listedFirst @"dealer" -- listedFirst is just First with the type-arguments rearranged.
       everyone = refl @("dealer" ': players)
   hand1 <-
     ( fanIn everyone \(player :: Member player players) -> do
-        card1 <- locally dealer (\_ -> getInput ("Enter random card for " ++ toLocTm player))
+        card1 <- locally dealer (\_ -> getInput ("Enter random card for " ++ toValue player))
         (dealer, card1) ~> everyone
       )
       >>= naked everyone
@@ -76,10 +79,10 @@ game = do
       choice <- broadcast (listedFirst @player, localize player wantsNextCard)
       if choice
         then do
-          cd2 <- locally dealer' (\_ -> getInput (toLocTm player ++ "'s second card:"))
+          cd2 <- locally dealer' (\_ -> getInput (toValue player ++ "'s second card:"))
           card2 <- broadcast (dealer', cd2)
-          return [getLeaf hand1 player, card2]
-        else return [getLeaf hand1 player]
+          return [hand1 ! player, card2]
+        else return [hand1 ! player]
   tblCrd <- locally dealer (\_ -> getInput "Enter a single card for everyone:")
   tableCard <- (dealer, tblCrd) ~> players
   void $ parallel players \player un -> do

examples/ChooseTeams.hs

@@ -9,7 +9,9 @@ import Choreography
 import Control.Monad (when)
 import Data (TestArgs, reference)
 import Data.Foldable (toList)
+import Data.Known.Knowable
 import Data.Maybe (catMaybes)
+import Data.Known.Membership
 import Test.QuickCheck (Arbitrary, arbitrary)
 
 newtype Args = Args
@@ -23,23 +25,23 @@ instance TestArgs Args ([Int], [Int], [Int], [Int], [Int]) where
 instance Arbitrary Args where
   arbitrary = Args <$> arbitrary
 
-chooseTeams :: [LocTm] -> ([LocTm], [LocTm]) -- Probably could find it off-the-shelf somewhere...
+chooseTeams :: [PartyName] -> ([PartyName], [PartyName]) -- Probably could find it off-the-shelf somewhere...
 chooseTeams [] = ([], [])
 chooseTeams (a : as) =
   let (t1, t2) = chooseTeams as
    in (t2, a : t1)
 
 -- the game is just red-team sending numbers to blue team.
-game :: forall players m. (KnownSymbols players) => Choreo players (CLI m) ()
+game :: forall players m. (Known [Party] players) => Choreo players (CLI m) ()
 game = do
   let players = allOf @players
-  let (red, blue) = chooseTeams $ toLocs players
+  let (red, blue) = chooseTeams $ toValue players
   numbers <- fanIn players \p ->
-    if toLocTm p `elem` red
+    if toValue p `elem` red
       then (p, Just <$> getInput @Int "A number to send:") -~> players
       else conclave players $ return Nothing
   parallel_ players \p un ->
-    when (toLocTm p `elem` blue) $
+    when (toValue p `elem` blue) $
       putOutput "Numbers received:" $
         catMaybes . toList $
           un p numbers

examples/DelegationFig20.hs

@@ -23,11 +23,15 @@ import Choreography
 import Data (TestArgs, reference)
 import Data.List (sort)
 import Data.Maybe (fromMaybe)
+import Data.Known.Membership
 import Test.QuickCheck (Arbitrary, arbitrary, arbitraryPrintableChar, elements, listOf1)
 
-$(mkLoc "alice")
-$(mkLoc "bob")
-$(mkLoc "carroll")
+alice :: forall ps. ExplicitMember "alice" ps => Member "alice" ps
+alice = explicitMember
+bob :: forall ps. ExplicitMember "bob" ps => Member "bob" ps
+bob = explicitMember
+carroll :: forall ps. ExplicitMember "carroll" ps => Member "carroll" ps
+carroll = explicitMember
 
 type Participants = ["alice", "bob", "carroll"]
 

examples/DiffieHellman.hs

@@ -45,6 +45,7 @@ import CLI
 import Choreography
 import Choreography.Network.Http
 import Control.Monad.IO.Class (MonadIO)
+import Data.Known.Membership
 import System.Environment
 import System.Random
 
@@ -60,10 +61,11 @@ isPrime x = divisors x == [1, x]
 primeNums :: [Integer]
 primeNums = [x | x <- [2 ..], isPrime x]
 
-$(mkLoc "alice")
-$(mkLoc "bob")
-
 type Participants = ["alice", "bob"]
+alice :: forall ps. ExplicitMember "alice" ps => Member "alice" ps
+alice = explicitMember
+bob :: forall ps. ExplicitMember "bob" ps => Member "bob" ps
+bob = explicitMember
 
 diffieHellman ::
   (MonadIO m) =>