# Small rewrite of \`HasChor\` using \`singletons\`

**URL:** https://discourse.haskell.org/t/small-rewrite-of-haschor-using-singletons/13237
**Category:** Show and Tell
**Created:** [November 7, 2025, 12:21pm UTC](https://discourse.haskell.org/t/small-rewrite-of-haschor-using-singletons/13237 "2025-11-07T12:21:53Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![fpringle](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/fpringle/32/3433_2.png) [@fpringle](https://discourse.haskell.org/u/fpringle)
#### Post date: [November 7, 2025, 12:21pm UTC](https://discourse.haskell.org/t/small-rewrite-of-haschor-using-singletons/13237/1 "2025-11-07T12:21:53Z")

</div>

I’m a big fan of the [HasChor](https://github.com/gshen42/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 `Symbol`s and term-level `String`s (and `Proxy`s) to represent the different parties (“locations”) in a choreography. This seems to me like a perfect use-case for [singletons](https://hackage.haskell.org/package/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](https://github.com/fpringle/HasChor/commit/4013f8b900bc1cae4bd87abeede30c7ac340023a)

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](https://github.com/fpringle/HasChor/commit/ccd194e09651d776541f4aa3f2d3012e12ad6f23)  
For a quick demo, take a look at `quicksort`:

```haskell
{- | 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]

```