From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 24 Jul 2020 08:44:37 +0000 (+0200)
Subject: add uds and auds implementations
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=19f417f58ffdd44a610978030433082def910187;p=clean-tests.git

add uds and auds implementations
---

diff --git a/uds/auds.dcl b/uds/auds.dcl
new file mode 100644
index 0000000..accd9d2
--- /dev/null
+++ b/uds/auds.dcl
@@ -0,0 +1,123 @@
+definition module auds
+
+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 r w
+	= Read r //* done reading
+	| E.sds: Reading (sds m r w) & read sds //* not done reading
+	| ReadResultUnused (m ())
+
+//* Result of a single write rewrite
+:: WriteResult m r w
+	= Written () //* done writing
+	| E.sds: Writing (sds m r w) & write sds //* not done writing
+	| 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
+
+//* 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
+sds :: (sds m r w) -> SDS m 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) | 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 r w = ReadSource (m r)
+//* Just write something
+:: WriteSource m r w = WriteSource (w -> m ())
+//* Pair a two shares to form a read/write sds that only touches one share per action
+:: RWPair sdsr sdsw m r w = RWPair (sdsr m r w) (sdsw m r w) | RWPairUnused (m ())
+
+//* Special type of RWPair that contains sds sources
+:: Source m r w :== RWPair ReadSource WriteSource m r w
+source :: (m r) (w -> m ()) -> Source m r w
+
+//* Combine two shares in parallel
+:: Par sdsl sdsr m r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr m r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
+par :: (r1 r2 -> m r) (w -> m (w1, w2)) (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m r w | TC r1 & TC r2 & TC w1 & TC w2
+:: ParOpts sdsl sdsr m r1 r2 w1 w2 r w =
+	{ readl  :: r1 r2 -> m r
+	, writel :: w -> m (w1, w2)
+	, left   :: sdsl m r1 w1
+	, right  :: sdsr m r2 w2
+	}
+
+//* Apply a lens to a share
+:: Lens sds m r w = E.r1 w1: Lens (LensOpts sds m r1 w1 r w) & TC r1 & TC w1
+lens :: (r1 -> m r) (w r1 -> m (Maybe w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+:: LensOpts sds m r1 w1 r w =
+	{ mapr :: r1 -> m r
+	, mapw :: w r1 -> m (Maybe w1)
+	, lens :: sds m r1 w1
+	}
+
+//* Determine a share from the value read from another share
+:: Select sdsl sdsr m r w = E.r1 w1: Select (SelectOpts sdsl sdsr m r1 w1 r w) & TC r1 & TC w1
+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 r1 w1 r w =
+	{ select :: sdsl m r1 w1
+	, bind   :: r1 -> m (sdsr m r w)
+	}
+
+//* Immediately returns the given value on a read
+constShare :: a -> ReadSource m a b | Monad m
+//* Values written are discarded
+nullShare :: WriteSource m a b | Monad m
+
+//* Current time
+timeStamp :: ReadSource IO Timestamp ()
+
+//* Map a function to the value read
+mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
+(>?@) infixl 6
+(>?@) :== mapRead
+
+//* Map a function to the value written.
+mapWrite :: (w` r -> m (Maybe w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+(>!@) infixl 6
+(>!@) :== mapWrite
+
+(>*<) infixl 6 :: (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & Monad m
+
+fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
+toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
+
+indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
+keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
+
+indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
+keyedSelect :: (sdsl m k z) (sdsr m (Map k v) (Map k v)) -> Select sdsl (Lens sdsr) m v v | TC z & TC v & TC k & < k & MonadFail m
+
+astore :: String -> Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
+dstore :: String -> Lens (RWPair ReadSource WriteSource) (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
+store :: Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic) | Monad m
+
+file :: FilePath -> Source IO String String
diff --git a/uds/auds.icl b/uds/auds.icl
new file mode 100644
index 0000000..a94b077
--- /dev/null
+++ b/uds/auds.icl
@@ -0,0 +1,195 @@
+implementation module auds
+
+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 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
+
+source :: (m r) (w -> m ()) -> Source m r w
+source read write = RWPair (ReadSource read) (WriteSource write)
+
+constShare :: a -> ReadSource m a b | Monad m
+constShare a = ReadSource $ pure a
+
+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
+
+//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
+
+par :: (r1 r2 -> m r) (w -> m (w1, w2)) (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m r w | TC r1 & TC r2 & TC w1 & TC w2
+par readl writel left right = Par {readl=readl,writel=writel,left=left,right=right}
+
+(>*<) infixl 6 :: (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & Monad m
+(>*<) l r = par (\x y->pure (x, y)) pure l r
+
+instance read (Par sdsl sdsr) | read sdsl & read sdsr
+where
+	read (Par t=:{readl,left,right}) = read left >>= \v->case v of
+		Read l = read right >>= \v->case v of
+			Read r = Read <$> readl l r
+			Reading s = pure $ Reading $ Par {t & left=constShare l, right=s}
+		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
+				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}
+
+lens :: (r1 -> m r) (w r1 -> m (Maybe w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+lens mapr mapw lens = Lens {mapr=mapr,mapw=mapw,lens=lens}
+
+instance read (Lens sds) | read sds
+where
+	read (Lens t=:{mapr,lens}) = read lens >>= \v->case v of
+		Read r = Read <$> mapr r
+		Reading s = pure $ Reading $ Lens {t & lens=s}
+
+instance read (RWPair sdsr sdsw) | read sdsr
+where
+	read (RWPair s w) = read s >>= \v->case v of
+		Read r = pure $ Read r
+		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
+		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
+		Read r = mapw w r >>= \w->case w of
+			Nothing = pure $ Written ()
+			Just w = write w lens >>= \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}
+
+mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
+mapRead f sds = lens f (\_ _->pure Nothing) sds
+
+fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
+fromDynStore sds = lens
+	(\r->case r of
+		(r :: r^) = pure r
+		_ = fail "type mismatch")
+	(\w _->pure $ Just (dynamic w))
+	sds
+
+toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
+toDynStore sds = lens
+	(\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 r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+mapWrite f sds = lens pure f sds
+
+indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
+indexedStore idx sds = lens
+	(\r->maybe (fail "out of range") pure (r !? idx))
+	(\w->pure o Just o updateAt idx w)
+	sds
+
+keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
+keyedStore key sds = lens
+	(maybe (fail "key not present") pure o 'Data.Map'.get key)
+	(\w->pure o Just o 'Data.Map'.put key w)
+	sds
+
+select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+select select bind = Select {select=select,bind=bind}
+
+instance read (Select sdsl sdsr) | read sdsl & read sdsr
+where
+	read (Select t=:{select,bind}) = read select >>= \v->case v of
+		Read r = bind r >>= read
+		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
+		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
+indexedSelect l r = select l $ pure o flip indexedStore r
+
+keyedSelect :: (sdsl m k z) (sdsr m (Map k v) (Map k v))
+	-> Select sdsl (Lens sdsr) m v v | TC z & TC v & TC k & < k & MonadFail m
+keyedSelect l r = select l $ pure o flip keyedStore r
+
+getShare :: (sds m r w) -> m r | Monad m & read sds & TC r & TC w
+getShare s = read s >>= \v->case v of
+	Read r = pure r
+	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
+	Written _ = pure ()
+	Writing s = setShare w s
+
+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 (Int, Map String Dynamic)
+Start = runStateT t $ 'Data.Map'.singleton "blurp" (dynamic 38)
+where
+//	t = write (42, "blurp") (astore "foo" >*< astore "bar")
+//	t = write 42 (astore "blurp")
+//		>>| read (astore "blurp")
+	t = setShare 42 (astore "blurp")
+		>>| getShare (astore "blurp")
+
+//Start world = evalIO t world
+//where
+//	t = read (file "auds.icl")
+
+astore :: String -> Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
+astore s = fromDynStore $ dstore s
+
+dstore :: String -> Lens (RWPair ReadSource WriteSource) (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
+dstore s = keyedStore s store
+
+store :: Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic) | Monad m
+store = source getState put
+
+file :: FilePath -> Source IO String String
+file p = source (readFileM p) (writeFileM p)
diff --git a/uds/test.icl b/uds/test.icl
deleted file mode 100644
index fe83fe0..0000000
--- a/uds/test.icl
+++ /dev/null
@@ -1,132 +0,0 @@
-module test
-
-import StdEnv
-import Data.Maybe
-import Data.Functor
-import Data.Func
-import Data.Tuple
-import Data.List
-import Control.Applicative
-import Control.Monad
-import qualified Data.Map
-
-class get v ~st :: (v r w) .st -> .(Maybe r, .st) | TC r
-class put v ~st :: w (v r w) .st -> .(Maybe (), .st) | TC w
-
-:: SDS sds a :== sds a a
-
-:: Source r w = Source String
-:: St :== 'Data.Map'.Map String Dynamic
-
-instance get Source St
-where
-	get (Source n) st = case 'Data.Map'.get n st of
-		Just (a :: a^) = (Just a, st)
-		_ = (Nothing, st)
-
-instance put Source St
-where
-	put w (Source n) st = (Just (), 'Data.Map'.put n (dynamic w) st)
-
-:: Par sdsl sdsr r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
-:: ParOpts sdsl sdsr r1 r2 w1 w2 r w =
-	{ read  :: r1 r2 -> Maybe r
-	, write :: w -> Maybe (w1, w2)
-	, left  :: sdsl r1 w1
-	, right :: sdsr r2 w2
-	}
-(>*<) infixl 6 :: (sdsl r1 w1) (sdsr r2 w2) -> Par sdsl sdsr (r1, r2) (w1, w2) | get sdsl St & put sdsr St & TC r1 & TC r2 & TC w1 & TC w2
-(>*<) l r = Par {read= \x y->Just (x, y), write=Just, left=l, right=r}
-
-instance get (Par sdsl sdsr) St | get sdsl St & get sdsr St
-where
-	get (Par {read,left,right}) st
-		# (ml, st) = get left st
-		# (mr, st) = get right st
-		= (join $ read <$> ml <*> mr, st)
-instance put (Par sdsl sdsr) St | put sdsl St & put sdsr St
-where
-	put w (Par {write,left,right}) st
-		= case write w of
-			Just (w1, w2)
-				# (ml, st) = put w1 left st
-				# (mr, st) = put w2 right st
-				= (ml *> mr, st)
-			Nothing = (Nothing, st)
-
-:: Lens sds r w = E.r1 w1: Lens (LensOpts sds r1 w1 r w) & TC r1 & TC w1
-:: LensOpts sds r1 w1 r w =
-	{ mapr :: r1   -> Maybe r
-	, mapw :: w r1 -> Maybe w1
-	, lens :: sds r1 w1
-	}
-
-instance get (Lens sds) St | get sds St
-where
-	get (Lens {mapr,lens}) st = appFst ((=<<) mapr) $ get lens st
-instance put (Lens sds) St | get sds St & put sds St
-where
-	put w (Lens {mapw,lens}) st
-		# (mv, st) = get lens st
-		= case mv of
-			Just r = case mapw w r of
-				Just w = put w lens st
-				Nothing = (Nothing, st)
-			Nothing = (Nothing, st)
-
-:: Select sdsl sdsr r w = E.r1 w1: Select (SelectOpts sdsl sdsr r1 w1 r w) & TC r1 & TC w1
-:: SelectOpts sdsl sdsr r1 w1 r w =
-	{ select :: sdsl r1 w1
-	, bind   :: r1 -> (sdsr r w)
-	}
-
-instance get (Select sdsl sdsr) St | get sdsl St & get sdsr St
-where
-	get (Select {select,bind}) st
-		= case get select st of
-			(Just r, st)  = get (bind r) st
-			(Nothing, st) = (Nothing, st)
-instance put (Select sdsl sdsr) St | get sdsl St & put sdsr St
-where
-	put w (Select {select,bind}) st
-		= case get select st of
-			(Just r, st) = put w (bind r) st
-			(Nothing, st) = (Nothing, st)
-
-mapRead :: (r -> r`) (sds r w) -> Lens sds r` w | TC r` & TC r & TC w
-mapRead f sds = Lens {mapr=Just o f, mapw=const o Just, lens=sds}
-(>?@) infixl 6
-(>?@) :== mapRead
-
-mapWrite :: (w` r -> Maybe w) (sds r w) -> Lens sds r w` | TC r & TC w & TC w`
-mapWrite f sds = Lens {mapr=Just, mapw=f, lens=sds}
-(>!@) infixl 6
-(>!@) :== mapWrite
-
-indexedStore :: Int (SDS sds [a]) -> SDS (Lens sds) a | TC a
-indexedStore idx sds
-	= Lens
-		{ mapr = \r->r !? idx
-		, mapw = \w->Just o updateAt idx w
-		, lens = sds
-		}
-
-indexedSelect :: (sdsl Int z) (SDS sdsr [a]) -> SDS (Select sdsl (Lens sdsr)) a | TC a & TC z
-indexedSelect l r = Select {select=l, bind=flip indexedStore r}
-
-keyedSelect :: (sdsl k z) (SDS sdsr ('Data.Map'.Map k v)) -> SDS (Select sdsl (Lens sdsr)) v | TC z & TC v & TC k & < k
-keyedSelect l r = Select {select=l, bind=flip keyedStore r}
-
-keyedStore :: k (SDS sds ('Data.Map'.Map k v)) -> SDS (Lens sds) v | TC v & TC k & < k
-keyedStore key sds
-	= Lens
-		{ mapr = 'Data.Map'.get key
-		, mapw = \r->Just o 'Data.Map'.put key r
-		, lens = sds
-		}
-
-Start = appSnd 'Data.Map'.toList
-	$ put (42, "blurp") (store "foo" >*< store "bar") 'Data.Map'.newMap
-
-store :: (String -> Source a a) | TC a
-store = Source
diff --git a/uds/uds.dcl b/uds/uds.dcl
new file mode 100644
index 0000000..8c3e495
--- /dev/null
+++ b/uds/uds.dcl
@@ -0,0 +1,95 @@
+definition module uds
+
+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
+
+class read v :: (v m r w) -> m r | TC r & Monad m
+class write v :: w (v m r w) -> m () | TC w & Monad m
+upd :: (r -> w) (v m r w) -> m w | TC r & TC w & read, write v & Monad m
+
+sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m
+:: SDS m r w = E.sds: SDS (sds m r w) (m ()) /*force kind*/ & read sds & write sds
+
+instance read SDS, ReadSource, Source
+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, Source
+instance write (Par sdsl sdsr) | write sdsl & write sdsr
+instance write (Lens sds) | read sds & write sds
+instance write (Select sdsl sdsr) | read sdsl & write sdsr
+
+:: ReadSource m r w = ReadSource (m r)
+:: WriteSource m r w = WriteSource (w -> m ())
+
+source :: (m r) (w -> m ()) -> Source m r w
+:: Source m r w = Source (ReadSource m r w) (WriteSource m r w)
+
+par :: (r1 r2 -> m r) (w -> m (w1, w2)) (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m r w | TC r1 & TC r2 & TC w1 & TC w2
+:: Par sdsl sdsr m r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr m r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
+:: ParOpts sdsl sdsr m r1 r2 w1 w2 r w =
+	{ readl  :: r1 r2 -> m r
+	, writel :: w -> m (w1, w2)
+	, left   :: sdsl m r1 w1
+	, right  :: sdsr m r2 w2
+	}
+
+lens :: (r1 -> m r) (w r1 -> m w1) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+:: Lens sds m r w = E.r1 w1: Lens (LensOpts sds m r1 w1 r w) & TC r1 & TC w1
+:: LensOpts sds m r1 w1 r w =
+	{ mapr :: r1 -> m r
+	, mapw :: w r1 -> m w1
+	, lens :: sds m r1 w1
+	}
+
+select :: (sdsl m r1 w1) (r1 -> sdsr m r w) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+:: Select sdsl sdsr m r w = E.r1 w1: Select (SelectOpts sdsl sdsr m r1 w1 r w) & TC r1 & TC w1
+:: SelectOpts sdsl sdsr m r1 w1 r w =
+	{ select :: sdsl m r1 w1
+	, bind   :: r1 -> sdsr m r w
+	, unused :: m () //* to force correct kinds
+	}
+
+constShare :: a -> ReadSource m a () | Monad m
+nullShare :: WriteSource m () a | Monad m
+
+timeStamp :: ReadSource IO Timestamp ()
+
+mapRead :: (r -> r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
+(>?@) infixl 6
+(>?@) :== mapRead
+mapWrite :: (w` r -> m w) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+(>!@) infixl 6
+(>!@) :== mapWrite
+
+(>*<) infixl 6 :: (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & Monad m
+
+fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
+toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
+
+indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
+keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
+
+indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
+keyedSelect :: (sdsl m k z) (sdsr m (Map k v) (Map k v)) -> Select sdsl (Lens sdsr) m v v | TC z & TC v & TC k & < k & MonadFail m
+
+astore :: String -> Lens (Lens Source) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
+dstore :: String -> Lens Source (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
+store :: (Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic)) | Monad m
+
+file :: FilePath -> Source IO String String
diff --git a/uds/uds.icl b/uds/uds.icl
new file mode 100644
index 0000000..57be2eb
--- /dev/null
+++ b/uds/uds.icl
@@ -0,0 +1,153 @@
+implementation module uds
+
+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
+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 r w) -> SDS m r w | read sds & write sds & Monad m
+sds s = SDS s (pure ())
+instance read SDS where read (SDS sds _) = read sds
+instance write SDS where write w (SDS sds _) = write w sds
+
+source :: (m r) (w -> m ()) -> Source m r w
+source read write = Source (ReadSource read) (WriteSource write)
+
+constShare :: a -> ReadSource m a () | Monad m
+constShare a = ReadSource (pure a)
+
+nullShare :: WriteSource m () a | Monad m
+nullShare = WriteSource (\_->pure ())
+
+instance read ReadSource where read (ReadSource read) = read
+instance write WriteSource where write w (WriteSource write) = write w
+instance read Source where read (Source s _) = read s
+instance write Source where write w (Source _ s) = write w s
+
+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
+
+par :: (r1 r2 -> m r) (w -> m (w1, w2)) (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m r w | TC r1 & TC r2 & TC w1 & TC w2
+par readl writel left right = Par {readl=readl,writel=writel,left=left,right=right}
+
+(>*<) infixl 6 :: (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & Monad m
+(>*<) l r = par (\x y->pure (x, y)) pure l r
+
+instance read (Par sdsl sdsr) | read sdsl & read sdsr
+where
+	read (Par {readl,left,right}) = join $ readl <$> read left <*> read right
+instance write (Par sdsl sdsr) | write sdsl & write sdsr
+where
+	write w (Par {writel,left,right})
+		= writel w >>= \(w1, w2)->write w1 left >>| write w2 right
+
+lens :: (r1 -> m r) (w r1 -> m w1) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+lens mapr mapw lens = Lens {mapr=mapr,mapw=mapw,lens=lens}
+
+instance read (Lens sds) | read sds
+where
+	read (Lens {mapr,lens}) = read lens >>= mapr
+instance write (Lens sds) | read sds & write sds
+where
+	write w (Lens {mapw,lens}) = read lens >>= mapw w >>= flip write lens
+
+mapRead :: (r -> r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
+mapRead f sds = lens (pure o f) (const o pure) sds
+
+fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
+fromDynStore sds = lens
+	(\r->case r of
+		(r :: r^) = pure r
+		_ = fail "type mismatch")
+	(\w _->pure (dynamic w))
+	sds
+
+toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
+toDynStore sds = lens
+	(\r->pure (dynamic r))
+	(\w _->case w of
+		(w :: w^) = pure w
+		_ = fail "type mismatch")
+	sds
+
+mapWrite :: (w` r -> m w) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+mapWrite f sds = lens pure f sds
+
+indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
+indexedStore idx sds = lens
+	(\r->maybe (fail "out of range") pure (r !? idx))
+	((o) pure o updateAt idx)
+//	(\w->pure o updateAt idx w)
+	sds
+
+keyedStore :: k (sds m ('Data.Map'.Map k v) ('Data.Map'.Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
+keyedStore key sds = lens
+	(maybe (fail "key not present") pure o 'Data.Map'.get key)
+	((o) pure o 'Data.Map'.put key)
+//	(\w->pure o 'Data.Map'.put key w)
+	sds
+
+select :: (sdsl m r1 w1) (r1 -> sdsr m r w) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+select select bind = Select {select=select,bind=bind,unused=pure ()}
+
+instance read (Select sdsl sdsr) | read sdsl & read sdsr
+where
+	read (Select {select,bind}) = read select >>= read o bind
+instance write (Select sdsl sdsr) | read sdsl & write sdsr
+where
+	write w (Select {select,bind}) = read select >>= write w o bind
+
+indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
+indexedSelect l r = select l $ flip indexedStore r
+
+keyedSelect :: (sdsl m k z) (sdsr m ('Data.Map'.Map k v) ('Data.Map'.Map k v))
+	-> Select sdsl (Lens sdsr) m v v | TC z & TC v & TC k & < k & MonadFail m
+keyedSelect l r = select l $ flip keyedStore r
+
+//Start :: Either String ('Data.Map'.Map String Dynamic)
+//Start :: Either String (Int, 'Data.Map'.Map String Dynamic)
+//Start = runStateT t $ 'Data.Map'.singleton "blurp" (dynamic 38)
+//where
+//	t = write (42, "blurp") (astore "foo" >*< astore "bar")
+//	t = write 42 (astore "blurp")
+//		>>| read (astore "blurp")
+
+//Start world = evalIO t world
+//where
+//	t = read (file "test.icl")
+
+astore :: String -> Lens (Lens Source) (StateT ('Data.Map'.Map String Dynamic) m) a a | MonadFail m & TC a
+astore s = fromDynStore $ dstore s
+
+dstore :: String -> Lens Source (StateT ('Data.Map'.Map String Dynamic) m) Dynamic Dynamic | MonadFail m
+dstore s = keyedStore s store
+
+store :: (Source (StateT ('Data.Map'.Map String Dynamic) m) ('Data.Map'.Map String Dynamic) ('Data.Map'.Map String Dynamic)) | Monad m
+store = Source (ReadSource getState) (WriteSource put)
+
+file :: FilePath -> Source IO String String
+file p = source (readFileM p) (writeFileM p)
+
+Start = 42