Small rewrite of `HasChor` using `singletons`

Show and Tell
1

I’m a big fan of the HasChor library for functional choreographic programming. See the README of that repo for a detailed explanation.

One thing that stuck out to me is that the library uses type-level Symbols and term-level Strings (and Proxys) to represent the different parties (“locations”) in a choreography. This seems to me like a perfect use-case for singletons, so I forked HasChor and rewrote it. Why? Fun!

The interesting commit is this one: Use `singleton`s instead of `Symbol`s and `String`s · fpringle/HasChor@4013f8b · GitHub

The Choreo and Network signatures and the Backend class now have an extra type parameter k, which is a Kind. The user can now define an enum-like type, generate singletons for it using genSingletons, and use the generated kind, type, values and instances with the rest of the HasChor machinery. This helps define exactly which parties take part in a choreography.

I also rewrote the provided examples in this commit: Update examples to use singletons · fpringle/HasChor@ccd194e · GitHub
For a quick demo, take a look at quicksort:

{- | Define the parties (locations) that are allowed in our choreography.
 We need instances of Hashable, FromHttpApiData and ToHttpApiData to use the
 HttpConfig backend
-}
data Party = Primary | Worker1 | Worker2
  deriving (Show, Read, Eq, Generic, Hashable)

instance FromHttpApiData Party where parseUrlPiece = defParseUrlPiece

instance ToHttpApiData Party where toUrlPiece = defToUrlPiece

{- | This will generate:

- a GADT: SParty (p :: Party), with one constructor for each constructor of Party
- an instance SingKind Party
- instances of SingI for each constructor of Party
-}
genSingletons [''Party]

-- | This is basically the same as before, just using SParty instead of Proxy
quicksort ::
  SParty a ->
  SParty b ->
  SParty c ->
  [Int] @ a ->
  Choreo Party 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''

-- | This is basically the same as before, just using values of type SParty instead of Proxys
mainChoreo :: Choreo Party IO ()
mainChoreo = do
  lst <- SPrimary `locally` \_ -> do return [1, 6, 5, 3, 4, 2, 7, 8]
  sorted <- quicksort SPrimary SWorker1 SWorker2 lst
  SPrimary `locally` \unwrap -> do
    print (unwrap sorted)
    return ()
  return ()

main :: IO ()
main = do
  config <- mkLocalConfig locs
  mapConcurrently_ (runChoreography config mainChoreo) locs
  return ()
  where
    -- we now use Partys instead of Strings
    locs = [Primary, Worker1, Worker2]
6 Likes