[ 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/contrib/Data/List/AtIndex.idr → 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,11 +98,12 @@ 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 ->
               AtIndex x (ws ++ xs) n -> AtIndex x xs (minus n (fst p))
 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/papers/Data/OpenUnion.idr → 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,22 +127,36 @@ 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
 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)
 
 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)