[ new ] System.Concurrency.(Linear/Session) (#3294)

* [ refactor ] moving Data.OpenUnion to base

* [ new ] System.Concurrency.(Linear/Session)

* [ test ] for the new feature

Fixing other tests impacted by the refactoring

* [ cleanup ] move definitions around, touch up docs

* [ fix ] re-export linear notations for Control.Linear.LIO

libs/base/Data/List/AtIndex.idr

@@ -1,3 +1,10 @@
+||| Indexing into Lists.
+|||
+||| `Elem` proofs give existential quantification that a given element
+||| *is* in the list, but not where in the list it is!  Here we give a
+||| predicate that presents proof that a given index in a list, given
+||| by a natural number, will return a certain element.
+
 module Data.List.AtIndex
 
 import Data.DPair
@@ -51,25 +58,6 @@ find x (y :: xs) with (decEq x y)
         (Element Z p) => void (neqxy (inverseZ p))
         (Element (S n) prf) => absurd (notInxs (Element n (inverseS prf)))
 
-||| If the equality is not decidable, we may instead rely on interface resolution
-public export
-interface Member (0 t : a) (0 ts : List a) where
-  isMember' : Subset Nat (AtIndex t ts)
-
-public export
-isMember : (0 t : a) -> (0 ts : List a) -> Member t ts =>
-              Subset Nat (AtIndex t ts)
-isMember t ts @{p} = isMember' @{p}
-
-public export
-Member t (t :: ts) where
-  isMember' = Element 0 Z
-
-public export
-Member t ts => Member t (u :: ts) where
-  isMember' = let (Element n prf) = isMember t ts in
-              Element (S n) (S prf)
-
 ||| Given an index, we can decide whether there is a value corresponding to it
 public export
 lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\ x => AtIndex x xs n))
@@ -86,18 +74,22 @@ inRange n [] p = void (absurd p)
 inRange Z (x :: xs) p = LTEZero
 inRange (S n) (x :: xs) p = LTESucc (inRange n xs (inverseS p))
 
-|||
+||| An index remains unchanged if we extend the list to the right
 export
 weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n
 weakenR Z = Z
 weakenR (S p) = S (weakenR p)
 
+||| An index into `xs` is shifted by `m` if we prepend a list of size `m`
+||| in front of it
 export
 weakenL : (p : Subset Nat (flip HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n)
 weakenL m p with (view m)
   weakenL (Element 0 Z) p | Z = p
   weakenL (Element (S (fst m)) (S (snd m))) p | (S m) = S (weakenL m p)
 
+||| Conversely to `weakenR`, if an index is smaller than the length of
+||| a prefix then it points into that prefix.
 export
 strengthenL : (p : Subset Nat (flip HasLength xs)) ->
               lt n (fst p) === True ->
@@ -106,6 +98,8 @@ strengthenL m lt idx with (view m)
   strengthenL (Element (S (fst m)) (S (snd m))) lt Z | (S m) = Z
   strengthenL (Element (S (fst m)) (S (snd m))) lt (S k) | (S m) = S (strengthenL m lt k)
 
+||| Conversely to `weakenL`, if an index is larger than the length of
+||| a prefix then it points into the suffix.
 export
 strengthenR : (p : Subset Nat (flip HasLength ws)) ->
               lte (fst p) n === True ->
@@ -113,4 +107,3 @@ strengthenR : (p : Subset Nat (flip HasLength ws)) ->
 strengthenR m lt idx with (view m)
   strengthenR (Element 0 Z) lt idx | Z = rewrite minusZeroRight n in idx
   strengthenR (Element (S (fst m)) (S (snd m))) lt (S k) | (S m) = strengthenR m lt k
-

libs/base/Data/OpenUnion.idr

@@ -2,8 +2,8 @@
 ||| Freer Monads, More Extensible Effects
 ||| by Oleg Kiselyov and Hiromi Ishii
 |||
-||| By using an AtIndex proof, we are able to get rid of all of the unsafe
-||| coercions in the original module.
+||| By using an AtIndex proof, we are able to get rid of all of
+||| the unsafe coercions in the original module.
 
 module Data.OpenUnion
 
@@ -17,49 +17,47 @@ import Syntax.WithProof
 
 %default total
 
-||| An open union of families is an index picking a family out together with
-||| a value in the family thus picked.
+||| An open union transformer takes
+||| @ts   a list of type descriptions
+||| @elt  a method to turn descriptions into types
+||| and returns a union of the types described in the list.
+||| Elements are given by an index selecting a value in the list
+||| together with a value of the appropriately decoded type.
 public export
-data Union : (elt : a -> Type) -> (ts : List a) -> Type where
-  Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> Union elt ts
+data UnionT : (elt : a -> Type) -> (ts : List a) -> Type where
+  Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> UnionT elt ts
+
+||| A union of types is obtained by taking the union transformer
+||| where the decoding function is the identity.
+public export
+Union : List Type -> Type
+Union = UnionT Prelude.id
 
 ||| An empty open union of families is empty
 public export
-Uninhabited (Union elt []) where
+Uninhabited (UnionT elt []) where
   uninhabited (Element _ p _) = void (uninhabited p)
 
 ||| Injecting a value into an open union, provided we know the index of
 ||| the appropriate type family.
-inj' : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> Union elt ts
-inj' = Element
+export
+inj : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> UnionT elt ts
+inj = Element
 
 ||| Projecting out of an open union, provided we know the index of the
 ||| appropriate type family. This may obviously fail if the value stored
 ||| actually corresponds to another family.
-prj' : (k : Nat) -> (0 _ : AtIndex t ts k) -> Union elt ts -> Maybe (elt t)
-prj' k p (Element k' q t) with (decEq k  k')
-  prj' k p (Element k q t) | Yes Refl = rewrite atIndexUnique p q in Just t
-  prj' k p (Element k' q t) | No neq = Nothing
-
-||| Given that equality of type families is not decidable, we have to
-||| rely on the interface `Member` to automatically find the index of a
-||| given family.
-public export
-inj : Member t ts => elt t -> Union elt ts
-inj = let (Element n p) = isMember t ts in inj' n p
-
-||| Given that equality of type families is not decidable, we have to
-||| rely on the interface `Member` to automatically find the index of a
-||| given family.
-public export
-prj : Member t ts => Union elt ts -> Maybe (elt t)
-prj = let (Element n p) = isMember t ts in prj' n p
+export
+prj : (k : Nat) -> (0 _ : AtIndex t ts k) -> UnionT elt ts -> Maybe (elt t)
+prj k p (Element k' q t) with (decEq k  k')
+  prj k p (Element k q t) | Yes Refl = rewrite atIndexUnique p q in Just t
+  prj k p (Element k' q t) | No neq = Nothing
 
 ||| By doing a bit of arithmetic we can figure out whether the union's value
 ||| came from the left or the right list used in the index.
 public export
 split : Subset Nat (flip HasLength ss) ->
-        Union elt (ss ++ ts) -> Either (Union elt ss) (Union elt ts)
+        UnionT elt (ss ++ ts) -> Either (UnionT elt ss) (UnionT elt ts)
 split m (Element n p t) with (@@ lt n (fst m))
   split m (Element n p t) | (True ** lt)
     = Left (Element n (strengthenL m lt p) t)
@@ -72,25 +70,25 @@ split m (Element n p t) with (@@ lt n (fst m))
 ||| whether the value it contains belongs either to the first family or any
 ||| other in the tail.
 public export
-decomp : Union elt (t :: ts) -> Either (Union elt ts) (elt t)
+decomp : UnionT elt (t :: ts) -> Either (UnionT elt ts) (elt t)
 decomp (Element 0     (Z)   t) = Right t
 decomp (Element (S n) (S p) t) = Left (Element n p t)
 
 ||| An open union over a singleton list is just a wrapper
 public export
-decomp0 : Union elt [t] -> elt t
+decomp0 : UnionT elt [t] -> elt t
 decomp0 elt = case decomp elt of
   Left t => absurd t
   Right t => t
 
 ||| Inserting new union members on the right leaves the index unchanged.
 public export
-weakenR : Union elt ts -> Union elt (ts ++ us)
+weakenR : UnionT elt ts -> UnionT elt (ts ++ us)
 weakenR (Element n p t) = Element n (weakenR p) t
 
 ||| Inserting new union members on the left, requires shifting the index by
 ||| the number of members introduced. Note that this number is the only
 ||| thing we need to keep around at runtime.
 public export
-weakenL : Subset Nat (flip HasLength ss) -> Union elt ts -> Union elt (ss ++ ts)
+weakenL : Subset Nat (flip HasLength ss) -> UnionT elt ts -> UnionT elt (ss ++ ts)
 weakenL m (Element n p t) = Element (fst m + n) (weakenL m p) t

libs/base/base.ipkg

@@ -38,6 +38,7 @@ modules = Control.App,
           Data.Bifoldable,
           Data.Bits,
           Data.Bool,
+          Data.Bool.Decidable,
           Data.Bool.Xor,
           Data.Buffer,
           Data.Colist,
@@ -55,6 +56,7 @@ modules = Control.App,
           Data.IORef,
           Data.Integral,
           Data.List,
+          Data.List.AtIndex,
           Data.List.Elem,
           Data.List.HasLength,
           Data.List.Lazy,
@@ -69,7 +71,9 @@ modules = Control.App,
           Data.Morphisms,
           Data.Nat,
           Data.Nat.Order,
+          Data.Nat.Order.Properties,
           Data.Nat.Views,
+          Data.OpenUnion,
           Data.Primitives.Interpolation,
           Data.Primitives.Views,
           Data.Ref,
@@ -91,6 +95,7 @@ modules = Control.App,
           Data.Vect.AtIndex,
           Data.Vect.Elem,
           Data.Vect.Quantifiers,
+          Data.Void,
           Data.Zippable,
 
           Debug.Trace,
@@ -112,6 +117,7 @@ modules = Control.App,
           Syntax.PreorderReasoning,
           Syntax.PreorderReasoning.Ops,
           Syntax.PreorderReasoning.Generic,
+          Syntax.WithProof,
 
           System,
           System.Clock,

libs/contrib/contrib.ipkg

@@ -24,7 +24,6 @@ modules = Control.ANSI,
           Data.Binary,
 
           Data.Bool.Algebra,
-          Data.Bool.Decidable,
 
           Data.Fin.Extra,
 
@@ -48,7 +47,6 @@ modules = Control.ANSI,
           Data.List.Reverse,
           Data.List.Views.Extra,
           Data.List.Palindrome,
-          Data.List.AtIndex,
           Data.List.Alternating,
           Data.List.Sufficient,
 
@@ -69,7 +67,6 @@ modules = Control.ANSI,
           Data.Nat.Factor,
           Data.Nat.Fib,
           Data.Nat.Order.Strict,
-          Data.Nat.Order.Properties,
           Data.Nat.Order.Relation,
           Data.Nat.Properties,
 
@@ -111,8 +108,6 @@ modules = Control.ANSI,
           Data.Vect.Sort,
           Data.Vect.Views.Extra,
 
-          Data.Void,
-
           Debug.Buffer,
 
           Decidable.Finite.Fin,
@@ -129,8 +124,6 @@ modules = Control.ANSI,
           Language.JSON.String.Tokens,
           Language.JSON.Tokens,
 
-          Syntax.WithProof,
-
           System.Console.GetOpt,
           System.Directory.Tree,
           System.Future,

libs/linear/Control/Linear/LIO.idr

@@ -1,10 +1,13 @@
 module Control.Linear.LIO
 
+import public Data.Linear.Notation
+import System
+
 ||| Like `Monad`, but the action and continuation must be run exactly once
 ||| to ensure that the computation is linear.
 public export
 interface LinearBind io where
-  bindL : (1 _ : io a) -> (1 _ : a -> io b) -> io b
+  bindL : io a -@ (a -> io b) -@ io b
 
 export
 LinearBind IO where
@@ -71,7 +74,7 @@ RunCont Unrestricted t b = t -> b
 -- concrete type of the continuation is.
 runK : {use : _} ->
        LinearBind io =>
-       (1 _ : L io {use} a) -> (1 _ : RunCont use a (io b)) -> io b
+       L io {use} a -@ RunCont use a (io b) -@ io b
 runK (Pure0 x) k = k x
 runK (Pure1 x) k = k x
 runK (PureW x) k = k x
@@ -86,7 +89,7 @@ runK (Bind {u_act = Unrestricted} act next) k = runK act (\x => runK (next x) k)
 ||| underlying context
 export
 run : Applicative io => LinearBind io =>
-      (1 _ : L io a) -> io a
+      L io a -@ io a
 run prog = runK prog pure
 
 export
@@ -110,12 +113,12 @@ export
 export %inline
 (>>=) : {u_act : _} ->
         LinearBind io =>
-        (1 _ : L io {use=u_act} a) ->
-        (1 _ : ContType io u_act u_k a b) -> L io {use=u_k} b
+        L io {use=u_act} a -@
+        ContType io u_act u_k a b -@ L io {use=u_k} b
 (>>=) = Bind
 
 export
-delay : {u_act : _} -> (1 _ : L io {use=u_k} b) -> ContType io u_act u_k () b
+delay : {u_act : _} -> L io {use=u_k} b -@ ContType io u_act u_k () b
 delay mb = case u_act of
   None => \ _ => mb
   Linear => \ () => mb
@@ -124,8 +127,8 @@ delay mb = case u_act of
 export %inline
 (>>) : {u_act : _} ->
         LinearBind io =>
-        (1 _ : L io {use=u_act} ()) ->
-        (1 _ : L io {use=u_k} b) -> L io {use=u_k} b
+        L io {use=u_act} () -@
+        L io {use=u_k} b -@ L io {use=u_k} b
 ma >> mb = ma >>= delay mb
 
 export %inline
@@ -133,9 +136,16 @@ pure0 : (0 x : a) -> L io {use=0} a
 pure0 = Pure0
 
 export %inline
-pure1 : (1 x : a) -> L io {use=1} a
+pure1 : a -@ L io {use=1} a
 pure1 = Pure1
 
+||| Shuffling around linearity annotations: a computation of an
+||| unrestricted value can be seen as a computation of a linear
+||| value that happens to be unrestricted.
+export %inline
+bang : L IO t -@ L1 IO (!* t)
+bang io = io >>= \ a => pure1 (MkBang a)
+
 export
 (LinearBind io, HasLinearIO io) => HasLinearIO (L io) where
   liftIO1 p = Action (liftIO1 p)
@@ -143,3 +153,10 @@ export
 public export
 LinearIO : (Type -> Type) -> Type
 LinearIO io = (LinearBind io, HasLinearIO io)
+
+||| Linear version of `die`
+export
+die1 : LinearIO io => String -> L1 io a
+die1 err = do
+  x <- die err
+  pure1 x

libs/linear/System/Concurrency/Linear.idr

@@ -0,0 +1,33 @@
+module System.Concurrency.Linear
+
+import Control.Linear.LIO
+import System.Concurrency
+
+||| Run two linear computations in parallel and return the results.
+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)
+
+  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 ()
+  withChannel ch = assert_linear $ \ act => do
+    a <- LIO.run (act >>= assert_linear pure)
+    channelPut ch a
+
+||| Run two unrestricted computations in parallel and return the results.
+export
+par : L IO a -@ L IO b -@ L IO (a, b)
+par x y = do
+  (MkBang a # MkBang b) <- par1 (bang x) (bang y)
+  pure (a, b)

libs/linear/System/Concurrency/Session.idr

@@ -0,0 +1,218 @@
+module System.Concurrency.Session
+
+import Control.Linear.LIO
+
+import Data.List.AtIndex
+import Data.Nat
+
+import Data.OpenUnion
+import System
+import System.File
+import System.Concurrency as Threads
+import System.Concurrency.Linear
+
+import Language.Reflection
+
+%default total
+
+------------------------------------------------------------------------
+-- Session types
+
+namespace Session
+
+  ||| A session type describes the interactions one thread may have with
+  ||| another over a shared bidirectional channel: it may send or receive
+  ||| values of arbitrary types, or be done communicating.
+  public export
+  data Session : Type where
+    Send : (ty : Type) -> (s : Session) -> Session
+    Recv : (ty : Type) -> (s : Session) -> Session
+    End  : Session
+
+  ||| Dual describes how the other party to the communication sees the
+  ||| interactions: our sends become their receives and vice-versa.
+  public export
+  Dual : Session -> Session
+  Dual (Send ty s) = Recv ty (Dual s)
+  Dual (Recv ty s) = Send ty (Dual s)
+  Dual End = End
+
+  ||| Duality is involutive: the dual of my dual is me
+  export
+  dualInvolutive : (s : Session) -> Dual (Dual s) === s
+  dualInvolutive (Send ty s) = cong (Send ty) (dualInvolutive s)
+  dualInvolutive (Recv ty s) = cong (Recv ty) (dualInvolutive s)
+  dualInvolutive End = Refl
+
+||| We can collect the list of types that will be sent over the
+||| course of a session by walking down its description
+||| This definition is purely internal and will not show up in
+||| the library's interface.
+SendTypes : Session -> List Type
+SendTypes (Send ty s) = ty :: SendTypes s
+SendTypes (Recv ty s) = SendTypes s
+SendTypes End = []
+
+||| We can collect the list of types that will be received over
+||| the course of a session by walking down its description
+||| This definition is purely internal and will not show up in
+||| the library's interface.
+RecvTypes : Session -> List Type
+RecvTypes (Send ty s) = RecvTypes s
+RecvTypes (Recv ty s) = ty :: RecvTypes s
+RecvTypes End = []
+
+||| The types received by my dual are exactly the ones I am sending
+||| This definition is purely internal and will not show up in
+||| the library's interface.
+RecvDualTypes : (s : Session) -> RecvTypes (Dual s) === SendTypes s
+RecvDualTypes (Send ty s) = cong (ty ::) (RecvDualTypes s)
+RecvDualTypes (Recv ty s) = RecvDualTypes s
+RecvDualTypes End = Refl
+
+||| The types sent by my dual are exactly the ones I receive
+||| This definition is purely internal and will not show up in
+||| the library's interface.
+SendDualTypes : (s : Session) -> SendTypes (Dual s) === RecvTypes s
+SendDualTypes (Send ty s) = SendDualTypes s
+SendDualTypes (Recv ty s) = cong (ty ::) (SendDualTypes s)
+SendDualTypes End = Refl
+
+namespace Seen
+
+  ||| The inductive family (Seen m n f) states that the function `f`
+  ||| was obtained by composing an interleaving of `m` receiving
+  ||| steps and `n` sending ones.
+  public export
+  data Seen : Nat -> Nat -> (Session -> Session) -> Type where
+    None : Seen 0 0 Prelude.id
+    Recv : (ty : Type) -> Seen m n f -> Seen (S m) n (f . Recv ty)
+    Send : (ty : Type) -> Seen m n f -> Seen m (S n) (f . Send ty)
+
+||| If we know that `ty` is at index `n` in the list of received types
+||| and that `f` is a function defined using an interleaving of steps
+||| comprising `m` receiving stepsx then `ty` is at index `m + n` in `f s`.
+atRecvIndex : Seen m _ f ->
+          (s : Session) ->
+          AtIndex ty (RecvTypes s) n ->
+          AtIndex ty (RecvTypes (f s)) (m + n)
+atRecvIndex None accS accAt = accAt
+atRecvIndex (Recv ty s) accS accAt
+  = rewrite plusSuccRightSucc (pred m) n in
+    atRecvIndex s (Recv ty accS) (S accAt)
+atRecvIndex (Send ty s) accS accAt
+  = atRecvIndex s (Send ty accS) accAt
+
+||| If we know that `ty` is at index `n` in the list of sent types
+||| and that `f` is a function defined using an interleaving of steps
+||| comprising `m` sending steps then `ty` is at index `m + n` in `f s`.
+atSendIndex : Seen _ m f ->
+          (s : Session) ->
+          AtIndex ty (SendTypes s) n ->
+          AtIndex ty (SendTypes (f s)) (m + n)
+atSendIndex None accS accAt = accAt
+atSendIndex (Recv ty s) accS accAt
+  = atSendIndex s (Recv ty accS) accAt
+atSendIndex (Send ty s) accS accAt
+  = rewrite plusSuccRightSucc (pred m) n in
+    atSendIndex s (Send ty accS) (S accAt)
+
+
+||| A (bidirectional) channel is parametrised by a session it must respect.
+|||
+||| It is implemented in terms of two low-level channels: one for sending
+||| and one for receiving. This ensures that we never are in a situation
+||| where a thread with session (Send Nat (Recv String ...)) sends a natural
+||| number and subsequently performs a receive before the other party
+||| to the communication had time to grab the Nat thus receiving it
+||| instead of a String.
+|||
+||| The low-level channels can only carry values of a single type. And so
+||| they are given respective union types corresponding to the types that
+||| can be sent on the one hand and the ones that can be received on the
+||| other.
+||| These union types are tagged unions where if `ty` is at index `k` in
+||| the list of types `tys` then `(k, v)` is a value of `Union tys` provided
+||| that `v` has type `ty`.
+|||
+||| `sendStep`, `recvStep`, `seePrefix`, and `seen` encode the fact that
+||| we have already performed some of the protocol and so the low-level
+||| channels' respective types necessarily mention types that we won't
+||| see anymore.
+export
+record Channel (s : Session) where
+  constructor MkChannel
+  {sendStep     : Nat}
+  {recvStep     : Nat}
+  {0 seenPrefix : Session -> Session}
+  0 seen        : Seen recvStep sendStep seenPrefix
+
+  sendChan : Threads.Channel (Union (SendTypes (seenPrefix s)))
+  recvChan : Threads.Channel (Union (RecvTypes (seenPrefix s)))
+
+||| Consume a linear channel with a `Recv ty` step at the head of the
+||| session type in order to obtain a value of type `ty` together with
+||| a linear channel for the rest of the session.
+export
+recv : LinearIO io =>
+  Channel (Recv ty s) -@
+  L1 io (Res ty (const (Channel s)))
+recv (MkChannel {recvStep} seen sendCh recvCh) = do
+  x@(Element k prf val) <- channelGet recvCh
+  -- Here we check that we got the right message by projecting out of
+  -- the union type using the current `recvStep`. Both ends should be
+  -- in sync because of the `RecvDualTypes` and `SendDualTypes` lemmas.
+  let Just val = prj (recvStep + 0) (atRecvIndex seen (Recv ty s) Z) x
+    | Nothing => die1 "Error: invalid recv expected \{show recvStep} but got \{show k}"
+  pure1 (val # MkChannel (Recv ty seen) sendCh recvCh)
+
+
+||| Consume a linear channel with a `Send ty` step at the head of the
+||| session type in order to send a value of type `ty` and obtain a
+||| linear channel for the rest of the session.
+export
+send : LinearIO io =>
+  (1 _ : Channel (Send ty s)) ->
+  ty ->
+  L1 io (Channel s)
+send (MkChannel {sendStep} seen sendCh recvCh) x = do
+  let val = inj (sendStep + 0) (atSendIndex seen (Send ty s) Z) x
+  channelPut sendCh val
+  pure1 (MkChannel (Send ty seen) sendCh recvCh)
+
+||| Discard the channel provided that the session has reached its `End`.
+export
+end : LinearIO io => Channel End -@ L io ()
+end (MkChannel _ _ _) = do
+  pure ()
+
+||| Given a session, create a bidirectional communiaction channel and
+||| return its two endpoints
+export
+makeChannel :
+  LinearIO io =>
+  (0 s : Session) ->
+  L1 io (LPair (Channel s) (Channel (Dual s)))
+makeChannel s = do
+  sendChan <- Threads.makeChannel
+  recvChan <- Threads.makeChannel
+  let 1 posCh : Channel s
+    := MkChannel None sendChan recvChan
+  let 1 negCh : Channel (Dual s)
+    := MkChannel None
+         (rewrite SendDualTypes s in recvChan)
+         (rewrite RecvDualTypes s in sendChan)
+  pure1 (posCh # negCh)
+
+||| Given a session and two functions communicating according to that
+||| sesion, we can run the two programs concurrently and collect their
+||| final results.
+export
+fork : (0 s : Session) ->
+       (Channel       s  -@ L IO a) -@
+       (Channel (Dual s) -@ L IO b) -@
+       L IO (a, b)
+fork s kA kB = do
+  let 1 io = makeChannel s
+  (posCh # negCh) <- io
+  par (kA posCh) (kB negCh)

libs/linear/linear.ipkg

@@ -15,4 +15,7 @@ modules = Control.Linear.LIO,
           Data.Linear.LMaybe,
           Data.Linear.LNat,
           Data.Linear.LVect,
-          Data.Linear.Notation
+          Data.Linear.Notation,
+
+          System.Concurrency.Linear,
+          System.Concurrency.Session

libs/papers/papers.ipkg

@@ -24,8 +24,6 @@ modules = Control.DivideAndConquer,
           Data.Linear.Diff,
           Data.Linear.Inverse,
 
-          Data.OpenUnion,
-
           Data.ProofDelay,
 
           Data.Recursion.Free,

tests/Main.idr

@@ -192,6 +192,10 @@ baseLibraryTests = testsInDir "base" "Base library" {requirements = [Chez, Node]
 contribLibraryTests : IO TestPool
 contribLibraryTests = testsInDir "contrib" "Contrib library" {requirements = [Chez, Node]}
 
+-- same behavior as `baseLibraryTests`
+linearLibraryTests : IO TestPool
+linearLibraryTests = testsInDir "linear" "Linear library" {requirements = [Chez, Node]}
+
 codegenTests : IO TestPool
 codegenTests = testsInDir "codegen" "Code generation"
 
@@ -227,6 +231,7 @@ main = runner $
   , !ideModeTests
   , !preludeTests
   , !baseLibraryTests
+  , !linearLibraryTests
   , !contribLibraryTests
   , !chezTests
   , !refcTests

tests/linear/system_concurrency_session/Main.idr

@@ -0,0 +1,28 @@
+import Control.Linear.LIO
+import System.Concurrency.Session
+
+main : IO ()
+main = LIO.run $ do
+  let nm1 : String := "natrando"
+  let nm2 : String := "computer"
+  putStrLn "main: Forking two threads \{nm1} and \{nm2}"
+  res <- fork (Send Nat $ Send Nat $ Recv Nat End)
+    (\ ch => do let m : Nat := 100
+                putStrLn "\{nm1}: picked the natural \{show m}"
+                ch <- send ch m
+                let n : Nat := 50
+                putStrLn "\{nm1}: picked the natural \{show n}"
+                ch <- send ch n
+                (s # ch) <- recv ch
+                end ch
+                pure (m, n))
+    (\ ch => do (m # ch) <- recv ch
+                (n # ch) <- recv ch
+                putStrLn "\{nm2}: summing \{show m} and \{show n}"
+                let s = m + n
+                ch <- send ch s
+                end ch
+                pure s)
+  let mn = fst res
+  let mplusn = snd res
+  putStrLn {io = L IO} "main: Threads have finished and returned \{show mn} and \{show mplusn}"

tests/linear/system_concurrency_session/expected

@@ -0,0 +1,5 @@
+main: Forking two threads natrando and computer
+natrando: picked the natural 100
+natrando: picked the natural 50
+computer: summing 100 and 50
+main: Threads have finished and returned (100, 50) and 150

tests/linear/system_concurrency_session/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+run -p linear Main.idr