Skip to content

Commit 7c1c3ad

Browse files
gshen42gshen42
committed
init commit
0 parents  commit 7c1c3ad

File tree

5 files changed

+309
-0
lines changed

5 files changed

+309
-0
lines changed

‎.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
.zed
2+
dist-newstyle

‎CSD.cabal

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
cabal-version: 3.0
2+
name: CSD
3+
version: 0.1.0.0
4+
license: BSD-3-Clause
5+
license-file: LICENSE
6+
author: Gan Shen
7+
maintainer: [email protected]
8+
build-type: Simple
9+
10+
common warnings
11+
ghc-options: -Wall
12+
13+
library
14+
import: warnings
15+
default-language: GHC2021
16+
hs-source-dirs: src
17+
exposed-modules:
18+
Control.CSD
19+
-- other-modules:
20+
build-depends:
21+
base ^>=4.17.2.1,
22+
async ^>=2.2.5,
23+
24+
executable CSD-test
25+
import: warnings
26+
default-language: GHC2021
27+
hs-source-dirs: app
28+
main-is: Main.hs
29+
build-depends:
30+
base ^>=4.17.2.1,
31+
async ^>=2.2.5,
32+
CSD

‎LICENSE

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
Copyright (c) 2025, Gan Shen
2+
3+
4+
Redistribution and use in source and binary forms, with or without
5+
modification, are permitted provided that the following conditions are met:
6+
7+
* Redistributions of source code must retain the above copyright
8+
notice, this list of conditions and the following disclaimer.
9+
10+
* Redistributions in binary form must reproduce the above
11+
copyright notice, this list of conditions and the following
12+
disclaimer in the documentation and/or other materials provided
13+
with the distribution.
14+
15+
* Neither the name of the copyright holder nor the names of its
16+
contributors may be used to endorse or promote products derived
17+
from this software without specific prior written permission.
18+
19+
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
20+
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
21+
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
22+
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
23+
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
24+
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
25+
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
26+
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
27+
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
28+
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
29+
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

‎app/Main.hs

+124
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
{-# LANGUAGE GADTs #-}
2+
3+
module Main where
4+
5+
import Control.Arrow hiding ((>>>), (***))
6+
import Control.Concurrent.Async
7+
import Control.CSD
8+
import System.Environment
9+
10+
priceOf :: String -> Int
11+
priceOf "TaPL" = 80
12+
priceOf "PFPL" = 100
13+
priceOf _ = 999_999_999
14+
15+
-- Example 1: Basic Bookstore
16+
--
17+
-- A buyer sends the title of the book to the seller, then gets back its price.
18+
--
19+
-- > String > ()
20+
-- |\ |
21+
-- | ¯¯¯¯¯¯¯¯¯¯| |
22+
-- | \|
23+
-- | priceOf
24+
-- | /|
25+
-- | |¯¯¯¯¯¯¯¯¯¯ |
26+
-- |/ |
27+
-- < Int < ()
28+
29+
bookstore1 :: (Monad m) => CSD (Kleisli m) (Local String, Local ()) (Local Int, Local ())
30+
bookstore1 =
31+
(perf (\s -> return ((), s)) >>> Fork) *** noop
32+
>>> Perm AssocR
33+
>>> noop *** (Join >>> perf (\(t, _) -> return t))
34+
>>> noop *** perf (\t -> return (priceOf t, ()))
35+
>>> noop *** Fork
36+
>>> Perm AssocL
37+
>>> (Join >>> perf (\(_, p) -> return p)) *** noop
38+
39+
-- Example 2: Parallel Bookstore
40+
--
41+
-- Two buyers interact with a seller in parallel.
42+
--
43+
-- It might seem that we have seller, but they should be considered as *logical* sellers.
44+
-- When acutally running this choreography, we expect the *physical* seller would take the
45+
-- role of both logical seller and run them in parallel.
46+
47+
bookstore2 :: CSD (Kleisli IO) ((Local String, Local ()), (Local String, Local ())) ((Local Int, Local ()), (Local Int, Local ()))
48+
bookstore2 = bookstore1 *** bookstore1
49+
50+
priceOf' :: String -> Either String Int
51+
priceOf' "HoTT" = Right 123
52+
priceOf' "MLTT" = Right 456
53+
priceOf' s = Left s
54+
55+
-- Example 3: Conditional Choreography (with granular knowledge of choice)
56+
--
57+
-- Two sellers:
58+
-- Seller1 uses `priceOf'`, which is partial
59+
-- Seller1 forwards the title to seller 2 if it can't lookup its price.
60+
--
61+
-- > String > () > ()
62+
-- |\ | |
63+
-- | ¯¯¯¯¯¯¯¯¯¯| | |
64+
-- | \| |
65+
-- | priceOf' |
66+
-- | | /
67+
-- | / \ /
68+
-- | / _ \_______/
69+
-- | / | \ |
70+
-- | / | \ |
71+
-- | bookstore1 | |
72+
-- | | | | |
73+
-- | \__|____|___/
74+
-- | | |
75+
-- | /| |
76+
-- | |¯¯¯¯¯¯¯¯¯¯¯ | |
77+
-- |/ | |
78+
-- < Int < () < ()
79+
80+
bookstore3 :: CSD (Kleisli IO) (Local String, (Local (), Local ())) (Local Int, (Local (), Local ()))
81+
bookstore3 =
82+
(perf (\s -> return ((), s)) >>> Fork) *** noop *** noop
83+
>>> Perm (Trans AssocR (CongL AssocL))
84+
>>> noop *** (Join >>> perf (\(t, _) -> return t)) *** noop
85+
>>> noop *** perf (\t -> return (priceOf' t)) *** noop
86+
>>> noop *** Split *** noop
87+
>>> noop *** Notify
88+
>>> noop *** Branch bookstore1 (noop *** noop)
89+
>>> noop *** Perm Idem
90+
>>> noop *** perf (\p -> return (p, ())) *** noop
91+
>>> noop *** Fork *** noop
92+
>>> Perm (Trans AssocL (Trans (CongR AssocL) AssocR))
93+
>>> (Join >>> perf (\(_, p) -> return p)) *** noop *** noop
94+
95+
main :: IO ()
96+
main = do
97+
args <- getArgs
98+
case args of
99+
["bookstore1"] -> do
100+
s1 <- async (putStrLn "Type in the title of the book:" >> getLine)
101+
s2 <- async (return ())
102+
let prog = interpAsynced runKleisli bookstore1
103+
(s1', s2') <- prog (s1, s2)
104+
s1'' <- async (wait s1' >>= print)
105+
mapM_ wait [s1'', s2']
106+
["bookstore2"] -> do
107+
s11 <- async (putStrLn "Buyer 1: Type in the title of the book:" >> getLine)
108+
s12 <- async (return ())
109+
s21 <- async (putStrLn "Buyer 2: Type in the title of the book:" >> getLine)
110+
s22 <- async (return ())
111+
let prog = interpAsynced runKleisli bookstore2
112+
((s11', s12'), (s21', s22')) <- prog ((s11, s12), (s21, s22))
113+
s11'' <- async (wait s11' >>= print)
114+
s21'' <- async (wait s21' >>= print)
115+
mapM_ wait [s11'', s12', s21'', s22']
116+
["bookstore3"] -> do
117+
s1 <- async (putStrLn "Type in the title of the book:" >> getLine)
118+
s2 <- async (return ())
119+
s3 <- async (return ())
120+
let prog = interpAsynced runKleisli bookstore3
121+
(s1', (s2', s3')) <- prog (s1, (s2, s3))
122+
s1'' <- async (wait s1' >>= print)
123+
mapM_ wait [s1'', s2', s3']
124+
_ -> putStrLn "Unknown command-line arguments"

‎src/Control/CSD.hs

+122
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
{-# LANGUAGE TypeFamilies #-}
2+
3+
module Control.CSD where
4+
5+
import Control.Concurrent.Async
6+
import Data.Kind
7+
import Control.Arrow
8+
9+
infix 0 ≃
10+
infixr 1 >>>
11+
infixr 3 ***
12+
13+
-------------------------------------------------------------------------------
14+
-- * Site Configurations
15+
16+
data Local (a :: Type)
17+
18+
-- Configuration equality
19+
data a ≃ b where
20+
-- conjunction rules
21+
Swap :: (a, b) ≃ (b, a)
22+
AssocL :: (a, (b, c)) ≃ ((a, b), c)
23+
AssocR :: ((a, b), c) ≃ (a, (b, c))
24+
CongL :: a ≃ b -> (ctx, a) ≃ (ctx, b)
25+
CongR :: a ≃ b -> (a, ctx) ≃ (b, ctx)
26+
27+
-- Disjunction rules
28+
Idem :: Either a a ≃ a
29+
30+
Trans :: a ≃ b -> b ≃ c -> a ≃ c
31+
32+
-------------------------------------------------------------------------------
33+
-- * CSDs
34+
35+
data CSD f a b where
36+
-- sequence composition
37+
Perf :: f a b -> CSD f (Local a) (Local b)
38+
Seq :: CSD f a b -> CSD f b c -> CSD f a c
39+
40+
-- parallel composition
41+
Par :: CSD f a c -> CSD f b d -> CSD f (a, b) (c, d)
42+
Fork :: CSD f (Local (a, b)) (Local a, Local b)
43+
Join :: CSD f (Local a, Local b) (Local (a, b))
44+
Perm :: a ≃ b -> CSD f a b
45+
46+
-- Conditional execution
47+
Split :: CSD f (Local (Either a b)) (Either (Local a) (Local b))
48+
Notify :: CSD f (Either a b, c) (Either (a, c) (b, c))
49+
Branch :: CSD f a c -> CSD f b d -> CSD f (Either a b) (Either c d)
50+
51+
noop :: (Arrow f) => CSD f (Local a) (Local a)
52+
noop = Perf (arr id)
53+
54+
perf :: (Monad m) => (a -> m b) -> CSD (Kleisli m) (Local a) (Local b)
55+
perf f = Perf (Kleisli f)
56+
57+
-- the following operators are named after arrow operators share the same behavior
58+
59+
(>>>) :: CSD f a b -> CSD f b c -> CSD f a c
60+
a >>> b = Seq a b
61+
62+
(***) :: CSD f a c -> CSD f b d -> CSD f (a, b) (c, d)
63+
a *** b = Par a b
64+
65+
-------------------------------------------------------------------------------
66+
-- An interpreations to `Async`
67+
68+
-- There should be a more general way to interpret CSDs, and the `Async`ed
69+
-- interpretation is an instance of it
70+
71+
type family Asynced cfg where
72+
Asynced (a, b) = (Asynced a, Asynced b)
73+
Asynced (Either a b) = (Either (Asynced a) (Asynced b))
74+
Asynced (Local a) = Async a
75+
76+
interpAsynced :: (forall a b. f a b -> a -> IO b) -> CSD f a b -> Asynced a -> IO (Asynced b)
77+
interpAsynced hdl (Perf eff) a = do
78+
async $ do
79+
a' <- wait a
80+
hdl eff a'
81+
interpAsynced hdl (Seq f g) a = do
82+
b <- interpAsynced hdl f a
83+
interpAsynced hdl g b
84+
interpAsynced hdl (Par f g) (a, b) = do
85+
c <- interpAsynced hdl f a
86+
d <- interpAsynced hdl g b
87+
return (c, d)
88+
interpAsynced _ Fork ab = do
89+
a' <- async $ do
90+
(a, _) <- wait ab
91+
return a
92+
b' <- async $ do
93+
(_, b) <- wait ab
94+
return b
95+
return (a', b')
96+
interpAsynced _ Join (a, b) = do
97+
async $ do
98+
a' <- wait a
99+
b' <- wait b
100+
return (a', b')
101+
interpAsynced _ Split input = do
102+
i <- wait input
103+
case i of
104+
(Left x) -> Left <$> async (return x)
105+
(Right y) -> Right <$> async (return y)
106+
interpAsynced _ Notify (input1, input2) = do
107+
case input1 of
108+
(Left x) -> return (Left (x, input2))
109+
(Right y) -> return (Right (y, input2))
110+
interpAsynced hdl (Branch f g) input = do
111+
case input of
112+
(Left x) -> Left <$> interpAsynced hdl f x
113+
(Right y) -> Right <$> interpAsynced hdl g y
114+
-- structural rules
115+
interpAsynced _ (Perm Swap) (a, b) = return (b, a)
116+
interpAsynced hdl (Perm (CongL e)) (ctx, a) = (ctx,) <$> interpAsynced hdl (Perm e) a
117+
interpAsynced hdl (Perm (CongR e)) (a, ctx) = (,ctx) <$> interpAsynced hdl (Perm e) a
118+
interpAsynced _ (Perm AssocL) (a, (b, c)) = return ((a, b), c)
119+
interpAsynced _ (Perm AssocR) ((a, b), c) = return (a, (b, c))
120+
interpAsynced _ (Perm Idem) (Left a) = return a
121+
interpAsynced _ (Perm Idem) (Right a) = return a
122+
interpAsynced hdl (Perm (Trans e1 e2)) input = interpAsynced hdl (Perm e1) input >>= interpAsynced hdl (Perm e2)

0 commit comments

Comments
 (0)