From 527267cbd314c675ba7c1ba9a7c3461e1f9bfe97 Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 24 Jul 2020 13:59:13 +0200
Subject: [PATCH] asynchronous parametric lenses

---
 uds/asds.dcl | 138 +++++++++++++++++++++++++++++++++
 uds/asds.icl | 210 +++++++++++++++++++++++++++++++++++++++++++++++++++
 uds/auds.dcl |   4 +-
 uds/auds.icl |  27 +++----
 4 files changed, 361 insertions(+), 18 deletions(-)
 create mode 100644 uds/asds.dcl
 create mode 100644 uds/asds.icl

diff --git a/uds/asds.dcl b/uds/asds.dcl
new file mode 100644
index 0000000..816b096
--- /dev/null
+++ b/uds/asds.dcl
@@ -0,0 +1,138 @@
+definition module asds
+
+from Control.Applicative import class Applicative, class pure, class <*>
+from Control.Monad import class Monad
+from Control.Monad.State import :: StateT
+from Data.Either import :: Either
+from Data.Functor import class Functor
+from Data.Map import :: Map
+from StdMaybe import :: Maybe
+from StdOverloaded import class <, class fromString
+from System.FilePath import :: FilePath
+from System.IO import :: IO
+from System.Time import :: Timestamp
+
+class MonadFail m | Monad m where fail :: String -> m a
+instance MonadFail Maybe, []
+instance MonadFail (Either a) | fromString a
+instance MonadFail (StateT s m) | MonadFail m
+
+//* Result of a single read rewrite
+:: ReadResult m p r w
+	= Read r //* done reading
+	| E.sds: Reading (sds m p r w) & read sds //* not done reading
+	| ReadResultUnused (m ())
+
+//* Result of a single write rewrite
+:: WriteResult m p r w
+	= Written () //* done writing
+	| E.sds: Writing (sds m p r w) & write sds //* not done writing
+	| WriteResultUnused (m ())
+
+//* Read a share with one rewrite step
+class read v :: (v m p r w) p -> m (ReadResult m p r w) | TC r & Monad m
+//* Write a share with one rewrite step
+class write v :: (v m p r w) p w -> m (WriteResult m p r w) | TC w & Monad m
+//* Read a share completely
+getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w
+//* Write a share completely
+setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w
+//* Update a share completely
+updShare :: (r -> w) (sds m () r w) -> m w | Monad m & read sds & write sds & TC r & TC w
+
+//* Box type, to get rid of a possible complex constructor of combinators
+:: SDS m p r w = E.sds: SDS (sds m p r w) (m ()) /*force kind*/ & read sds & write sds
+sds :: (sds m p r w) -> SDS m p r w | read sds & write sds & Monad m
+
+instance read SDS, ReadSource
+instance read (RWPair sdsr sdsw) | read sdsr
+instance read (Par sdsl sdsr) | read sdsl & read sdsr
+instance read (Lens sds) | read sds
+//instance read (Select sdsl sdsr) | read sdsl & read sdsr
+
+instance write SDS, WriteSource
+instance write (RWPair sdsr sdsw) | write sdsw
+instance write (Par sdsl sdsr) | read sdsl & read sdsr & write sdsl & write sdsr
+instance write (Lens sds) | read sds & write sds
+//instance write (Select sdsl sdsr) | read sdsl & write sdsr
+
+//* Just read something
+:: ReadSource m p r w = ReadSource (p -> m r)
+//* Just write something
+:: WriteSource m p r w = WriteSource (p w -> m ())
+//* Pair a two shares to form a read/write sds that only touches one share per action
+:: RWPair sdsr sdsw m p r w = RWPair (sdsr m p r w) (sdsw m p r w) | RWPairUnused (m ())
+
+//* Special type of RWPair that contains sds sources
+:: Source m p r w :== RWPair ReadSource WriteSource m p r w
+source :: (p -> m r) (p w -> m ()) -> Source m p r w
+
+//* Combine two shares in parallel
+:: Par sdsl sdsr m p r w = E.p1 p2 r1 r2 w1 w2: Par (ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w) & TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2
+par :: (p -> (p1, p2)) (r1 r2 -> r) (p w r1 -> m (Maybe w1)) (p w r2 -> m (Maybe w2)) (sdsl m p1 r1 w1) (sdsr m p2 r2 w2) -> Par sdsl sdsr m p r w | TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2
+:: ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w =
+	{ param  :: p -> (p1, p2)
+	, readl  :: r1 r2 -> r
+	, writel :: p w r1 -> m (Maybe w1)
+	, writer :: p w r2 -> m (Maybe w2)
+	, left   :: sdsl m p1 r1 w1
+	, right  :: sdsr m p2 r2 w2
+	}
+
+//* Apply a lens to a share
+:: Lens sds m p r w = E.p1 r1 w1: Lens (LensOpts sds m p1 r1 w1 p r w) & TC r1 & TC w1 & TC p1
+lens :: (p -> p1) (p r1 -> m r) (p w r1 -> m (Maybe w1)) (sds m p1 r1 w1) -> Lens sds m p r w | TC r1 & TC w1 & TC p1
+:: LensOpts sds m p1 r1 w1 p r w =
+	{ param  :: p -> p1
+	, mapr   :: p r1 -> m r
+	, mapw   :: p w r1 -> m (Maybe w1)
+	, lens   :: sds m p1 r1 w1
+	}
+
+//* Determine a share from the value read from another share
+:: Select sdsl sdsr m p r w = E.p1 r1 w1 p2: Select (SelectOpts sdsl sdsr m p1 r1 w1 p2 p r w) & TC r1 & TC p1 & TC p2
+//select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+:: SelectOpts sdsl sdsr m p1 r1 w1 p2 p r w =
+	{ index  :: sdsl m p1 r1 w1
+	, source :: sdsr m p2 r w
+	, parami :: p -> p1
+	, params :: p r1 -> p2
+	, unused :: m ()
+	}
+
+//* Immediately returns the given value on a read
+constShare :: a -> ReadSource m p a b | Monad m
+//* Values written are discarded
+nullShare :: WriteSource m p a b | Monad m
+
+//* Current time
+timeStamp :: ReadSource IO () Timestamp ()
+
+////* Map a function to the value read
+mapRead :: (r -> m r`) (sds m p r w) -> Lens sds m p r` w | TC r` & TC r & TC w & TC p & Monad m
+(>?@) infixl 6
+(>?@) :== mapRead
+
+//* Map a function to the value written.
+mapWrite :: (w` r -> m (Maybe w)) (sds m p r w) -> Lens sds m p r w` | TC r & TC w & TC w` & TC p & Monad m
+(>!@) infixl 6
+(>!@) :== mapWrite
+
+//* Translate the parameter space
+translate :: (p -> ps) (sds m ps r w) -> Lens sds m p r w | TC r & TC w & TC p & TC ps & Monad m
+//* focus a parameter: @type :: p (sds m p r w) -> (sds m p` r w)
+focus p :== translate \_->p
+
+(>*<) infixl 6 :: (sdsl m p1 r1 w1) (sdsr m p2 r2 w2) -> Par sdsl sdsr m (p1, p2) (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2 & Monad m
+
+fromDynStore :: (sds m p Dynamic Dynamic) -> Lens sds m p r w | TC r & TC w & TC p & MonadFail m
+toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m
+
+indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m
+keyedStore :: (sds m p (Map k v) (Map k v)) -> Lens sds m (p, k) v v | TC v & TC k & < k & TC p & MonadFail m
+
+astore :: Lens (Lens (Lens (RWPair ReadSource WriteSource))) (StateT (Map String Dynamic) m) String a a | MonadFail m & TC a
+dstore :: Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) String Dynamic Dynamic | MonadFail m
+store :: Source (StateT (Map String Dynamic) m) () (Map String Dynamic) (Map String Dynamic) | Monad m
+
+file :: Source IO FilePath String String
diff --git a/uds/asds.icl b/uds/asds.icl
new file mode 100644
index 0000000..e4351d4
--- /dev/null
+++ b/uds/asds.icl
@@ -0,0 +1,210 @@
+implementation module asds
+
+import StdEnv
+import Data.Maybe
+import Data.Functor
+import Data.Func
+import Data.Either
+import Data.Tuple
+import Data.List
+import Control.Applicative
+import Control.Monad
+import Control.Monad.State
+import Control.Monad.Trans
+import qualified Data.Map
+from Data.Map import :: Map
+import System.FilePath
+
+import System.IO
+import System.Time
+
+instance MonadFail Maybe where fail _ = Nothing
+instance MonadFail [] where fail _ = []
+instance MonadFail (Either a) | fromString a where fail s = Left $ fromString s
+instance MonadFail (StateT s m) | MonadFail m where fail s = liftT $ fail s
+
+sds :: (sds m p r w) -> SDS m p r w | read sds & write sds & Monad m
+sds s = SDS s (pure ())
+instance read SDS where read (SDS s _) p = read s p
+instance write SDS where write (SDS sds _) p w = write sds p w
+
+source :: (p -> m r) (p w -> m ()) -> Source m p r w
+source read write = RWPair (ReadSource read) (WriteSource write)
+
+constShare :: a -> ReadSource m p a b | Monad m
+constShare a = ReadSource \_->pure a
+
+nullShare :: WriteSource m p a b | Monad m
+nullShare = WriteSource \_ _->pure ()
+
+instance read ReadSource where read (ReadSource read) p = Read <$> read p
+instance write WriteSource where write (WriteSource write) p w = Written <$> write p w
+
+timeStamp :: ReadSource IO () Timestamp ()
+timeStamp = ReadSource \_->withWorld time
+
+par :: (p -> (p1, p2)) (r1 r2 -> r) (p w r1 -> m (Maybe w1)) (p w r2 -> m (Maybe w2)) (sdsl m p1 r1 w1) (sdsr m p2 r2 w2) -> Par sdsl sdsr m p r w | TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2
+par param readl writel writer left right = Par {param=param,readl=readl,writel=writel,writer=writer,left=left,right=right}
+
+(>*<) infixl 6 :: (sdsl m p1 r1 w1) (sdsr m p2 r2 w2) -> Par sdsl sdsr m (p1, p2) (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2 & Monad m
+(>*<) l r = par id tuple (\p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r
+
+(>+<) infixl 6 :: (sdsl m p r1 w1) (sdsr m p r2 w2) -> Par sdsl sdsr m p (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & TC p & Monad m
+(>+<) l r = par (\p->(p, p)) tuple (\p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r
+
+instance read (Par sdsl sdsr) | read sdsl & read sdsr
+where
+	read (Par t=:{param,readl,left,right}) p
+		= read left p1 >>= \v->case v of
+			Reading s = pure $ Reading $ Par {t & left=s}
+			Read l = read right p2 >>= \v->case v of
+				Reading s = pure $ Reading $ Par {t & left=constShare l, right=s}
+				Read r = pure $ Read $ readl l r
+	where (p1, p2) = param p
+instance write (Par sdsl sdsr) | read sdsl & read sdsr & write sdsl & write sdsr
+where
+	write (Par t=:{param,writel,writer,left,right}) p w
+		= read left p1 >>= \v->case v of
+			Reading s = pure $ Writing $ Par {t & left=RWPair s left}
+			Read r1 = write` left p1 (writel p w r1) >>= \v->case v of
+				Writing s = pure $ Writing $ Par {t & left=RWPair (constShare r1) left}
+				Written () = read right p2 >>= \v->case v of
+					Reading s = pure $ Writing $ Par {t & left=RWPair (constShare r1) nullShare, right=RWPair s right}
+					Read r2 = write` right p2 (writer p w r2) >>= \v->case v of
+						Writing s = pure $ Writing $ Par {t & left=RWPair (constShare r1) nullShare, right=RWPair (constShare r2) right}
+						Written () = pure $ Written ()
+	where (p1, p2) = param p
+
+write` :: (sds m p r w) p (m (Maybe w)) -> m (WriteResult m p r w) | TC w & Monad m & write sds
+write` sds p mmv = mmv >>= \mv->case mv of
+	Nothing = pure $ Written ()
+	Just v = write sds p v
+
+lens :: (p -> p1) (p r1 -> m r) (p w r1 -> m (Maybe w1)) (sds m p1 r1 w1) -> Lens sds m p r w | TC r1 & TC w1 & TC p1
+lens param mapr mapw lens = Lens {param=param,mapr=mapr,mapw=mapw,lens=lens}
+
+instance read (Lens sds) | read sds
+where
+	read (Lens t=:{param,mapr,lens}) p = read lens (param p) >>= \v->case v of
+		Reading s = pure $ Reading $ Lens {t & lens=s}
+		Read r = Read <$> mapr p r
+
+instance read (RWPair sdsr sdsw) | read sdsr
+where
+	read (RWPair s w) p = read s p >>= \v->case v of
+		Reading s = pure $ Reading (RWPair s w)
+		Read r = pure $ Read r
+instance write (RWPair sdsr sdsw) | write sdsw
+where
+	write (RWPair r s) p w = write s p w >>= \v->case v of
+		Writing s = pure $ Writing $ RWPair r s
+		Written _ = pure $ Written ()
+
+instance write (Lens sds) | read sds & write sds
+where
+	write (Lens t=:{param,mapw,lens}) p w = read lens (param p) >>= \v->case v of
+		Reading s = pure $ Writing $ Lens {t & lens=RWPair s lens}
+		Read r = mapw p w r >>= \v->case v of
+			Nothing = pure $ Written ()
+			Just w = write lens (param p) w >>= \v->case v of
+				Writing s = pure $ Writing $ Lens {t & mapw= \_ _ _->pure $ Just w, lens=RWPair (constShare r) s}
+				Written _ = pure $ Written ()
+
+mapRead :: (r -> m r`) (sds m p r w) -> Lens sds m p r` w | TC r` & TC r & TC w & TC p & Monad m
+mapRead f sds = lens id (\p r->f r) (\p w r->pure Nothing) sds
+
+fromDynStore :: (sds m p Dynamic Dynamic) -> Lens sds m p r w | TC r & TC w & TC p & MonadFail m
+fromDynStore sds = lens
+	id
+	(\_ r->case r of
+		(r :: r^) = pure r
+		_ = fail "type mismatch")
+	(\_ w _->pure $ Just (dynamic w))
+	sds
+
+toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m
+toDynStore sds = lens
+	id
+	(\_ r->pure (dynamic r))
+	(\_ w _->case w of
+		(w :: w^) = pure $ Just w
+		_ = fail "type mismatch")
+	sds
+
+mapWrite :: (w` r -> m (Maybe w)) (sds m p r w) -> Lens sds m p r w` | TC r & TC w & TC w` & TC p & Monad m
+mapWrite f sds = lens id (\_->pure) (\_->f) sds
+
+translate :: (p -> ps) (sds m ps r w) -> Lens sds m p r w | TC r & TC w & TC p & TC ps & Monad m
+translate param sds = lens param (\_ r->pure r) (\_ w _->pure $ Just w) sds
+
+indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m
+indexedStore sds = lens param read write sds
+where
+	param (p, _) = p
+	read (_, idx) r = maybe (fail "out of range") pure (r !? idx)
+	write (_, idx) w r = pure $ Just $ updateAt idx w r
+
+keyedStore :: (sds m p (Map k v) (Map k v)) -> Lens sds m (p, k) v v | TC v & TC k & < k & TC p & MonadFail m
+keyedStore sds = lens param read write sds
+where
+	param (p, _) = p
+	read (_, k) r = maybe (fail "key not present") pure $ 'Data.Map'.get k r
+	write (_, k) w r = pure $ Just $ 'Data.Map'.put k w r
+
+//select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+select :: (p -> p1) (p r1 -> p2) (sdsl m p1 r1 w1) (sdsr m p2 r w) -> Select sdsl sdsr m p r w | TC p & TC p1 & TC p2 & TC r1 & TC r & TC w
+select parami params index source = Select {parami=parami,params=params,index=index,source=source,unused=undef}
+
+instance read (Select sdsl sdsr) | read sdsl & read sdsr
+where
+	read (Select t=:{parami,params,index,source}) p = read index (parami p) >>= \v->case v of
+		Reading s = pure $ Reading $ Select {t & index=s}
+		Read r1 = read source (params p r1) >>= \v->case v of
+			Reading s = pure $ Reading $ Select {t & index=constShare r1, source=s}
+			Read r = pure $ Read r
+instance write (Select sdsl sdsr) | read sdsl & write sdsr
+where
+	write (Select t=:{parami,params,index,source}) p w = read index (parami p) >>= \v->case v of
+		Reading s = pure $ Writing $ Select {t & index=s}
+		Read r1 = write source (params p r1) w >>= \v->case v of
+			Writing s = pure $ Writing $ Select {t & index=constShare r1, source=s}
+			Written () = pure $ Written ()
+
+getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w
+getShare s = read s () >>= \v->case v of
+	Reading s = getShare s
+	Read r = pure r
+
+setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w
+setShare w s = write s () w >>= \v->case v of
+	Writing s = setShare w s
+	Written _ = pure ()
+
+updShare :: (r -> w) (sds m () r w) -> m w | Monad m & read sds & write sds & TC r & TC w
+updShare f s = f <$> getShare s >>= \v->setShare v s >>| pure v
+
+//Start :: Either String (Map String Dynamic)
+Start :: Either String ((), Map String Dynamic)
+Start = runStateT t $ 'Data.Map'.singleton "blurp" (dynamic 38)
+where
+	t = setShare (42, "blurp") (focus "foo" astore >+< focus "bar" astore)
+//	t = write 42 (astore "blurp")
+//		>>| read (astore "blurp")
+//	t = setShare 42 (focus "blurp" astore)
+//		>>| getShare (focus "blurp" astore)
+
+//Start world = evalIO t world
+//where
+//	t = getShare (focus "auds.icl" file)
+
+astore :: Lens (Lens (Lens (RWPair ReadSource WriteSource))) (StateT (Map String Dynamic) m) String a a | MonadFail m & TC a
+astore = fromDynStore dstore
+
+dstore :: Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) String Dynamic Dynamic | MonadFail m
+dstore = translate (\i->((), i)) $ keyedStore store
+
+store :: Source (StateT (Map String Dynamic) m) () (Map String Dynamic) (Map String Dynamic) | Monad m
+store = source (\_->getState) \_->put
+
+file :: Source IO FilePath String String
+file = source readFileM writeFileM
diff --git a/uds/auds.dcl b/uds/auds.dcl
index accd9d2..176d1e6 100644
--- a/uds/auds.dcl
+++ b/uds/auds.dcl
@@ -30,8 +30,8 @@ instance MonadFail (StateT s m) | MonadFail m
 	| WriteResultUnused (m ())
 
 
-class read v :: (v m r w) -> m (ReadResult m r w) | TC r & Monad m
-class write v :: w (v m r w) -> m (WriteResult m r w) | TC w & Monad m
+class read v  :: (v m r w) -> m (ReadResult m r w) | TC r & Monad m
+class write v :: (v m r w) w -> m (WriteResult m r w) | TC w & Monad m
 
 //* Box type, to get rid of a possible complex constructor of combinators
 :: SDS m r w = E.sds: SDS (sds m r w) (m ()) /*force kind*/ & read sds & write sds
diff --git a/uds/auds.icl b/uds/auds.icl
index a94b077..adb7c32 100644
--- a/uds/auds.icl
+++ b/uds/auds.icl
@@ -26,7 +26,7 @@ instance MonadFail (StateT s m) | MonadFail m where fail s = liftT $ fail s
 sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m
 sds s = SDS s (pure ())
 instance read SDS where read (SDS s _) = read s
-instance write SDS where write w (SDS sds _) = write w sds
+instance write SDS where write (SDS sds _) w = write sds w
 
 source :: (m r) (w -> m ()) -> Source m r w
 source read write = RWPair (ReadSource read) (WriteSource write)
@@ -38,13 +38,8 @@ nullShare :: WriteSource m a b | Monad m
 nullShare = WriteSource (\_->pure ())
 
 instance read ReadSource where read (ReadSource read) = Read <$> read
-instance write WriteSource where write w (WriteSource write) = Written <$> write w
+instance write WriteSource where write (WriteSource write) w = Written <$> write w
 
-//upd :: (r -> w) (v m r w) -> m w | TC r & TC w & read, write v & Monad m
-//upd fun sds = read sds >>= \r
-//	# w = fun r
-//	= write w sds >>| pure w
-//
 timeStamp :: ReadSource IO Timestamp ()
 timeStamp = ReadSource $ withWorld time
 
@@ -63,9 +58,9 @@ where
 		Reading s = pure $ Reading $ Par {t & left=s}
 instance write (Par sdsl sdsr) | write sdsl & write sdsr
 where
-	write w (Par t=:{writel,left,right})
-		= writel w >>= \(w1, w2)->write w1 left >>= \v->case v of
-			Written _ = write w2 right >>= \v->case v of
+	write (Par t=:{writel,left,right}) w
+		= writel w >>= \(w1, w2)->write left w1 >>= \v->case v of
+			Written _ = write right w2 >>= \v->case v of
 				Written _ = pure $ Written ()
 				Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=nullShare, right=s}
 			Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=s}
@@ -86,16 +81,16 @@ where
 		Reading s = pure $ Reading (RWPair s w)
 instance write (RWPair sdsr sdsw) | write sdsw
 where
-	write w (RWPair r s) = write w s >>= \v->case v of
+	write (RWPair r s) w = write s w >>= \v->case v of
 		Written _ = pure $ Written ()
 		Writing s = pure $ Writing $ RWPair r s
 
 instance write (Lens sds) | read sds & write sds
 where
-	write w (Lens t=:{mapw,lens}) = read lens >>= \v->case v of
+	write (Lens t=:{mapw,lens}) w = read lens >>= \v->case v of
 		Read r = mapw w r >>= \w->case w of
 			Nothing = pure $ Written ()
-			Just w = write w lens >>= \v->case v of
+			Just w = write lens w >>= \v->case v of
 				Written _ = pure $ Written ()
 				Writing s = pure $ Writing $ Lens {t & mapw= \_ _->pure $ Just w, lens=RWPair (constShare r) s}
 		Reading s = pure $ Writing $ Lens {t & lens=RWPair s lens}
@@ -144,8 +139,8 @@ where
 		Reading s = pure $ Reading $ Select {t & select=s}
 instance write (Select sdsl sdsr) | read sdsl & write sdsr
 where
-	write w (Select t=:{select,bind}) = read select >>= \v->case v of
-		Read r = bind r >>= write w
+	write (Select t=:{select,bind}) w = read select >>= \v->case v of
+		Read r = bind r >>= flip write w
 		Reading s = pure $ Writing $ Select {t & select=s}
 
 indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
@@ -161,7 +156,7 @@ getShare s = read s >>= \v->case v of
 	Reading s = getShare s
 
 setShare :: w (sds m r w) -> m () | Monad m & write sds & TC r & TC w
-setShare w s = write w s >>= \v->case v of
+setShare w s = write s w >>= \v->case v of
 	Written _ = pure ()
 	Writing s = setShare w s
 
-- 
2.20.1