From: Mart Lubbers Date: Fri, 24 Jul 2020 11:59:13 +0000 (+0200) Subject: asynchronous parametric lenses X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=527267cbd314c675ba7c1ba9a7c3461e1f9bfe97;p=clean-tests.git asynchronous parametric lenses --- 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