0 | module System.Concurrency.Linear
 1 |
 2 | import Control.Linear.LIO
 3 | import System.Concurrency
 4 |
 5 | ||| Run a linear computation in a separate thread
 6 | export
 7 | fork1 : L IO () -@ L IO ThreadID
 8 | fork1 act = liftIO1 $ fork $ LIO.run act
 9 |
10 | ||| Run a computation concurrently to the current thread.
11 | ||| This returns a receiver for the value.
12 | export
13 | concurrently : L IO a -@ L1 IO (L IO a)
14 | concurrently act = do
15 |   ch <- makeChannel
16 |   _ <- fork1 $ do
17 |     x <- act
18 |     channelPut ch x
19 |   pure1 $ channelGet ch
20 |
21 | ||| Run a computation concurrently to the current thread.
22 | ||| This returns a receiver for the value. A typical usage
23 | ||| pattern is showcased by the implementation of `par1`:
24 | ||| in a do block start executing a series of actions
25 | ||| concurrently and then collect the results with a series
26 | ||| of receiving steps.
27 | |||
28 | |||  do recva <- concurrently1 ioa
29 | |||     recvb <- concurrently1 iob
30 | |||     a <- recva
31 | |||     b <- recvb
32 | |||     pure1 (a # b)
33 | export
34 | concurrently1 : L1 IO a -@ L1 IO (L1 IO a)
35 | concurrently1 act = do
36 |   ch <- makeChannel
37 |   _ <- fork1 $ withChannel ch act
38 |   pure1 $ do
39 |     a <- channelGet ch
40 |     pure1 a
41 |
42 |   where
43 |
44 |   -- This unsafe implementation temporarily bypasses the linearity checker.
45 |   -- However `concurrently`'s implementation does not duplicate the values
46 |   -- and the type of `concurrently` ensures that client code is not allowed
47 |   -- to either!
48 |   withChannel : Channel t -> L1 IO t -@ L IO ()
49 |   withChannel ch = assert_linear $ \ act => do
50 |     a <- act
51 |     assert_linear (channelPut ch) a
52 |
53 |
54 | ||| Run two linear computations concurrently and return the results.
55 | export
56 | par1 : L1 IO a -@ L1 IO b -@ L1 IO (LPair a b)
57 | par1 ioa iob
58 |   = do -- run the two actions on separate threads
59 |        recva <- concurrently1 ioa
60 |        recvb <- concurrently1 iob
61 |        -- collect the results
62 |        a <- recva
63 |        b <- recvb
64 |        -- return the pair
65 |        pure1 (a # b)
66 |
67 | ||| Run two unrestricted computations in parallel and return the results.
68 | export
69 | par : L IO a -@ L IO b -@ L IO (a, b)
70 | par x y = do
71 |   (MkBang a # MkBang b) <- par1 (bang x) (bang y)
72 |   pure (a, b)
73 |