MultiChor-1.0.0.0: examples/MergeSort.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}

{-
# This example was carried over from earlier work, likely HasChor. It doesn't yet have a unit test attached to it.

# Example: merge sort

## Overview

This example implements the three-way concurrent implementation of merge sort shown in [Object-Oriented Choreographic Programming](https://arxiv.org/abs/2005.09520).

## Execution

This choreography will sort the list `[1, 6, 5, 3, 4, 2, 7, 8]`. It requires three locations: `primary`, `worker1`, and `worker2`.

```bash
# start two workers on separate terminals
cabal run mergesort worker1
cabal run mergesort worker2
# start primary on another terminal
cabal run mergesort primary
[1,2,3,4,5,6,7,8]
```
-}

module MergeSort where

import Choreography
import Choreography.Network.Http
import GHC.TypeLits (KnownSymbol)
import System.Environment

divide :: [a] -> ([a], [a])
divide xs = splitAt lhx xs
  where
    lhx = length xs `div` 2

$(mkLoc "primary")
$(mkLoc "worker1")
$(mkLoc "worker2")

type Participants = ["primary", "worker1", "worker2"]

sort ::
  ( KnownSymbol a,
    KnownSymbol c,
    KnownSymbol b,
    KnownSymbols ps
  ) =>
  Member a ps ->
  Member b ps ->
  Member c ps ->
  Located '[a] [Int] ->
  Choreo ps IO (Located '[a] [Int])
sort a b c lst = do
  condition <- a `locally` \un -> do return $ length (un singleton lst) > 1
  broadcast (a, condition) >>= \case
    True -> do
      _ <- a `locally` \un -> do return $ length (un singleton lst) `div` 2
      divided <- a `locally` \un -> do return $ divide (un singleton lst)
      l <- a `locally` \un -> do return $ fst (un singleton divided)
      r <- a `locally` \un -> do return $ snd (un singleton divided)
      l' <- (a, l) ~> b @@ nobody
      r' <- (a, r) ~> c @@ nobody
      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,
    KnownSymbol c,
    KnownSymbol b,
    KnownSymbols ps
  ) =>
  Member a ps ->
  Member b ps ->
  Member c ps ->
  Located '[b] [Int] ->
  Located '[c] [Int] ->
  Choreo ps IO (Located '[a] [Int])
merge a b c lhs rhs = do
  lhsHasElements <- b `locally` \un -> do return $ not (null (un singleton lhs))
  broadcast (b, lhsHasElements) >>= \case
    True -> do
      rhsHasElements <- c `locally` \un -> do return $ not (null (un singleton rhs))
      broadcast (c, rhsHasElements) >>= \case
        True -> do
          rhsHeadAtC <- c `locally` \un -> do return $ head (un singleton rhs)
          rhsHeadAtB <- (c, rhsHeadAtC) ~> b @@ nobody
          takeLhs <- b `locally` \un -> do return $ head (un singleton lhs) <= un singleton rhsHeadAtB
          broadcast (b, takeLhs) >>= \case
            True -> do
              -- take (head lhs) and merge the rest
              lhs' <- b `locally` \un -> do return $ tail (un singleton lhs)
              merged <- merge a b c lhs' rhs
              lhsHeadAtB <- b `locally` \un -> do return $ head (un singleton lhs)
              lhsHeadAtA <- (b, lhsHeadAtB) ~> a @@ nobody
              a `locally` \un -> do return $ un singleton lhsHeadAtA : un singleton merged
            False -> do
              -- take (head rhs) and merge the rest
              rhs' <- c `locally` \un -> do return $ tail (un singleton rhs)
              merged <- merge a b c lhs rhs'
              rhsHeadAtC' <- c `locally` \un -> do return $ head (un singleton rhs)
              rhsHeadAtA <- (c, rhsHeadAtC') ~> a @@ nobody
              a `locally` \un -> do return $ un singleton rhsHeadAtA : un singleton merged
        False -> do
          (b, lhs) ~> a @@ nobody
    False -> do
      (c, rhs) ~> a @@ nobody

mainChoreo :: Choreo Participants IO ()
mainChoreo = do
  lst <- primary `_locally` return [1, 6, 5, 3, 4, 2, 7, 8]
  sorted <- sort primary worker1 worker2 lst
  _ <-
    primary `locally` \un -> do
      print (un primary 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"
    _ -> error "unknown worker"
  return ()
  where
    config =
      mkHttpConfig
        [ ("primary", ("localhost", 3000)),
          ("worker1", ("localhost", 4000)),
          ("worker2", ("localhost", 5000))
        ]