[ linear ] fork1, concurrently1

Prompted by Peter Thiemann, an attempt at refactoring
par1 into reusable components.

libs/linear/System/Concurrency/Linear.idr

@@ -3,27 +3,56 @@ module System.Concurrency.Linear
 import Control.Linear.LIO
 import System.Concurrency
 
-||| Run two linear computations in parallel and return the results.
+||| Run a linear computation in a separate thread
 export
-par1 : L1 IO a -@ L1 IO b -@ L1 IO (LPair a b)
-par1 x y
-  = do aChan <- makeChannel
-       bChan <- makeChannel
-       aId <- liftIO1 $ fork $ withChannel aChan x
-       bId <- liftIO1 $ fork $ withChannel bChan y
-       a <- channelGet aChan
-       b <- channelGet bChan
-       pure1 (a # b)
+fork1 : L IO () -@ L IO ThreadID
+fork1 act = liftIO1 $ fork $ LIO.run act
+
+||| Run a computation concurrently to the current thread.
+||| This returns a receiver for the value. A typical usage
+||| pattern is showcased by the implementation of `par1`:
+||| in a do block start executing a series of actions
+||| concurrently and then collect the results with a series
+||| of receiving steps.
+|||
+|||  do recva <- concurrently1 ioa
+|||     recvb <- concurrently1 iob
+|||     a <- recva
+|||     b <- recvb
+|||     pure1 (a # b)
+export
+concurrently1 : L1 IO a -@ L1 IO (L1 IO a)
+concurrently1 act = do
+  ch <- makeChannel
+  _ <- fork1 $ withChannel ch act
+  pure1 $ do
+    a <- channelGet ch
+    pure1 a
 
   where
 
   -- This unsafe implementation temporarily bypasses the linearity checker.
-  -- However `par`'s implementation does not duplicate the values
-  -- and the type of `par` ensures that client code is not allowed to either!
-  withChannel : Channel t -> L1 IO t -@ IO ()
+  -- However `concurrently`'s implementation does not duplicate the values
+  -- and the type of `concurrently` ensures that client code is not allowed
+  -- to either!
+  withChannel : Channel t -> L1 IO t -@ L IO ()
   withChannel ch = assert_linear $ \ act => do
-    a <- LIO.run (act >>= assert_linear pure)
-    channelPut ch a
+    a <- act
+    assert_linear (channelPut ch) a
+
+
+||| Run two linear computations concurrently and return the results.
+export
+par1 : L1 IO a -@ L1 IO b -@ L1 IO (LPair a b)
+par1 ioa iob
+  = do -- run the two actions on separate threads
+       recva <- concurrently1 ioa
+       recvb <- concurrently1 iob
+       -- collect the results
+       a <- recva
+       b <- recvb
+       -- return the pair
+       pure1 (a # b)
 
 ||| Run two unrestricted computations in parallel and return the results.
 export