Interpreter for action that adds on the effect stack - Polysemy

how can I implement runTransaction?

data Db m a where
  -- ...

data Token

runDb :: Member (Embed IO) r => Token -> Sem (Db ': r) a -> Sem r a
runDb tok = interpret \case

data Transaction m a where
  InTransaction :: Sem (Db ': r) a -> Transaction (Sem r) a

inTransaction :: Member Transaction r => Sem (Db ': r) a -> Sem r a
inTransaction = send . InTransaction

runTransaction ::
  forall r a.
  (Member (Embed IO) r) =>
  Sem r Token ->
  (Token -> Sem r ()) ->
  Sem (Transaction ': r) a ->
  Sem r a
runTransaction acquire release = _

this "should be" a straightforward of application and interpretation of Resource (right???), but I'm having issues with the fact that the inside action has a different type from the r

do we want to runDb inside runTransaction?

yup

otherwise you can't dispatch the Db inside

tentative solution, without Embed IO on runDb:

runTransaction ::
  forall r a.
  Members [Resource, Embed IO] r =>
  Sem r Token ->
  (Token -> Sem r ()) ->
  Sem (Transaction ': r) a ->
  Sem r a
runTransaction acquire release =
  interpretH intp
  where
    intp ::
      ∀ x f rInitial .
      Functor f =>
      Transaction (Sem rInitial) x ->
      Sem (WithTactics Transaction f (Sem rInitial) r) (f x)
    intp = \case
      InTransaction ma ->
        bracket (raise acquire) (raise . release) run
        where
          run :: Token -> Sem (Tactics f (Sem rInitial) (Transaction : r) : r) (f x)
          run tok = do
            let
              ma' :: Sem (Db : rInitial) x
              ma' = ma
              ran :: Sem rInitial x
              ran = runDb tok ma'
            a :: Sem (Transaction : r) (f x) <- runT ran
            raise (runTransaction acquire release a)

I've left all the signatures in for analysis

so it definitely helps for type inference to make all the existentials explicit

and it is very notable here that our ma is already concretely typed, but runT can still be used since it has ∀ m that is just instantiated to our visible Sem rInitial

do you think you'll need an explicit way to show that Member (Embed IO) (Db ': r) implies Member (Embed IO) rInitial?

it works if you put the constraint in the InTransaction ctor as well

but optimally I guess you'd just pass runDb as an argument to runTransaction

how does that help?

Embed IO won't be visible to runTransaction then

if you pass it in as an argument and use it you'll still get the constraint tho?

but at the callsite

ah so you mean run :: Token -> Sem r a

and not the specialised version

hmmm

one sec

like this. but this might have to be tweaked, search the polysemy-resume topic for significantly relaxed :sweat_smile:

but with this, you should be able to experiment more easily

cool, thanks!

still not sure how to navigate the Tactics/Strategy related type sigs/errors

well, the most important thing is to internalize that Tactics is just a regular effect that has to be at the head everywhere in interpretH

and that it carries an m, which corresponds to the Sem r in you higher-order thunk in the constructor InTransaction

and then you only need to find the right combinator from the Tactics module to lift your thunk into the right signature

runT does that here, it's Sem rInitial a -> Sem (Transaction : r) (f a) effectively

where rInitial is the r from InTransaction as seen from the perspective of interpretH, where r is the final stack

really curious to see if this works well at runtime :sweat_smile:

btw if you want to allow nested calls to inTransaction, you will have to switch out the interpreter in the last line to avoid double bracketing

if this doesn't work, Resource probably won't too :thinking: it's almost directly a Resource usage
in fact now that I think about it, you can probably do away with Transaction entirely

Torsten Schmits said:

btw if you want to allow nested calls to inTransaction, you will have to switch out the interpreter in the last line to avoid double bracketing

won't the semantics be right? in nested inTransactions you're using the "innermost" transaction

which is what I'd expected (e.g. from name shadowing)

guess so!

and using Resource directly just means that you can't use a pure interpreter

you can still runIgnoreResource which just drops alloc and dealloc (not in library), if you want to use a Set instead of an actual db

I see!

for completeness:

runTransaction' ::
  forall t r .
  Member Resource r =>
  (∀ r' . t -> InterpreterFor Db r') ->
  Sem r t ->
  (t -> Sem r ()) ->
  InterpreterFor Transaction r
runTransaction' runDb' acquire release =
  interpretH \case
    InTransaction ma ->
      bracket (raise acquire) (raise . release) \ tok ->
        raise . runTransaction runDb' acquire release =<< runT (runDb' tok ma)

btw, do you know how the Tactics internals actually "give you" the next Transaction that you might need

for the recursive call

afaiu you're peeling off all the possible Transaction invocations (and in general, when you use Tactics and make that recursive call you're doing that)

when you recurse, you basically run the interpreter on the ma, since it might contain repeated uses of it, afaiu. I recommend (re-)reading Sandy's blogposts on the matter

because at that point, your ma is still untouched and you're already in the interpreter

funny, you can't do that transformation

        bracket (raise acquire) (raise . release) \tok -> do
          a <- (let x = runT $ runDb' tok ma in x)
          let g = raise . runTransaction runDb' acquire release
          g a

this is fine

nvm, just sleepy

aand the Transaction-less version is uh..

runTransaction ::
  Member Resource r =>
  Sem r Token ->
  (Token -> Sem r ()) ->
  (forall r'. Token -> forall b. Sem (Db ': r') b -> Sem r' b) ->
  Sem (Db ': r) a ->
  Sem r a
runTransaction acquire release act query =
  bracket acquire release (`act` query)

and that's better?

¯\_(ツ)_/¯

you won't be able to switch acquire and release for no-ops outside of the program

if I make Token polymorphic it'll be fine

then I can use token ~ ()

how are you using that function then? won't you call it in business logic?

yeah yeah, it's worse

you're basically doing the work of polysemy manually

because you'll end up threading all your functions as arguments

that you need to mock

just so I'm on the same page, you would have passed acquire etc into the business logic?

if I wanted to use the Transaction-less version, I would have made my "business logic" functions take polymorphic functions (the acquire, release and act) to use

that sounds very uncomfortable!

I think you can't actually call (in a "meaningful way") runTransaction with that type signature

since you have to provide a runDb :: (forall r'. t -> InterpreterFor Db r') that means that your runDb has to work for any r', or in other words, you can't rely on any effects (other than Db) being in the stack :thinking:

I can add a constraint like so

data Transaction eff m a where
  InTransaction :: forall eff inn a. Member eff inn => Sem (Db ': inn) a -> Transaction eff (Sem inn) a

but now I can't write the "send" function :thinking:

yeah, that's what I meant earlier with "look at the other thread" :smile:

why can't you write the function?

when I so much as mention InTransaction e.g.

inTransaction :: forall eff r a. Member (Transaction eff) r => Sem (Db ': r) a -> Sem r a
inTransaction _ = undefined $ (InTransaction @eff @r @a undefined)

I get a "can't find the effect eff" (Could not deduce LocateEff eff r ~ '())

maybe my signature should be different

Member eff r =>?

:facepalm:

but I think you need to change the signature of the interpreter parameter in the Transaction interpreter

going to sleep first, this is not productive :big_smile:

:big_smile: I'll take a look later as well

Torsten Schmits said:

but I think you need to change the signature of the interpreter parameter in the Transaction interpreter

from experience with trying a similar thing?

exactly

https://funprog.zulipchat.com/#narrow/stream/216942-Polysemy/topic/cross-interpreter.20errors/near/212495795

might be sufficient to just use r instead of an existential

I took another look and I don't see how it could be possible for this to work. we can only hope @Love Waern (King of the Homeless) has some dark magic up his sleeve

Seems so. Here's my first go:

data Transaction s m a where
  Trade :: s -> Db m a -> Transaction s m a
  InTransaction :: (s -> m a) -> Transaction s m a

interpretH' :: (forall x. Weaving e (Sem (e ': r)) x -> Sem r x)
            -> Sem (e ': r) a
            -> Sem r a
interpretH' h sem = Sem $ \k -> runSem sem $ \u -> case decomp u of
  Right wav -> runSem (h wav) k
  Left  g   -> k $ hoist (interpretH' h) g

inTransaction :: forall s r a. Member (Transaction s) r => Sem (Db ': r) a -> Sem r a
inTransaction main = send $ InTransaction @s $ \token -> transform (Trade token) main

runTransaction ::
  forall t r a.
  Member Resource r =>
  (t -> InterpreterFor Db r) ->
  Sem r t ->
  (t -> Sem r ()) ->
  Sem (Transaction t ': r) a ->
  Sem r a
runTransaction runner acquire release =
  let
    go :: forall x. Sem (Transaction t ': r) x -> Sem r x
    go = interpretH' $ \(Weaving eff s wv ex ins) -> case eff of
      Trade token db -> runner token (liftSem $ injWeaving $ Weaving db s (raise . go . wv) ex ins)
      InTransaction main -> do
        let main' token = go $ wv (main token <$ s)
        ex <$> bracket acquire release main'
  in
    go

Yet again interpretH fails me and I need to work with Weavings directly.
This might or might not be safe depending on the semantics of the runner. Is it ok if it's used multiple times for a single token -- once per Db action -- as long as the block within a specific token is used is delimited by acquire and release? If so, then this is safe. If not, then this is not safe.

Note that Transaction now needs a type variable. This is like Cont, where application code is expected to keep it fully polymorphic.

There's probably a more elegant solution. Maybe. I'll look into it more later.

what is the Trade for?

so I guess there's no "easy" way to "limit" what effects you can use inside InTransaction (or any HO effect for that matter) :thinking: and hide them from the "outside world" so that it can't interpret them however it pleases

The way my definition of Transaction works is that InTransaction provides the means of executing effects of Db locally within a region through some token. Executing actions of Db is done through Trade. Combining these, you can create the inTransaction action, where you gain access to a token locally so that you may execute actions of Db, and then you interpret the Db effect by using Trade.
This is an implementation detail: users should never use the constructors InTransaction and Trade directly.

The only way to "limit" what effects you can use inside a InTransaction is to have a parametrized monad:

data Transaction rTransaction m a where
  InTransaction :: Sem (Db ': rTransaction) a -> Transaction rTransaction m a

This is as easy to interpret as it is difficult for application code to use. It's not even a higher-order effect. It's like defining:

data StMTransaction m a where
  Atomically :: StM a -> StMTransaction m a

or the "wooden" way of

data Transaction t m a where
  InTransaction :: (t -> m a) -> Transaction t m a

data Db t m a where
  ..add a t argument to all the actions..

:big_smile:

Eh. That leaks implementation details of Transaction to Db. I prefer the Trade approach.

yep, as a library writer!

in inTransaction you're replacing all the Db actions with the same actions but with Trades around them, right?

Yes.

cool, thanks!

oh yeah I can use transform for that. Forgot that existed.

so mayber interpretH' should also be somewhere in the library, especially if you've had to rely on it more than once?

I've been humming and hawing about that. Honestly, I'm not satisfied with interpretH. It's too complicated for it's own good.

In fact, personally, I learned how Weavings worked before I learned how interpretH worked!

Maybe this could be added as an alternative:

interpretH' :: (  forall s r0 x
                . s ()
               -> (forall y. s (Sem r0 y) -> Sem (e ': r) (s y))
               -> (forall y. s y -> Maybe y)
               -> e (Sem r0) x
               -> Sem r (s x)
               )
            -> Sem (e ': r) a
            -> Sem r a

Which basically inlines the Weaving.

Alternatively, maybe the design of Tactical could be revamped. Not sure.

You know what would be really neat? This:

interpretHGood :: (  forall q x
                   . (forall x. z y -> Sem (Opaque q ': r) y)
                  -> e z x
                  -> Sem (Opaque q ': r) x
                  )
               -> Sem (e ': r) a
               -> Sem r a

Where Opaque is simply a newtype-wrapper to prevent the polymorphic q from messing with Member.
No weird state threading required! Believe it or not, this is almost possible! You can switch from the weave abstraction to a different mechanism with all the same restrictions, but is able to support interpretHGood. Still, there's so much tied to the weave abstraction that doing that switch would cause massive breakage. Something for v2.0 maybe.

since we now had two discussions of that kind within a few days, I think we need an interpretH that specializes in e (Sem r1) a -> Tactical e (Sem r2) r x, or whatever would make sense.
or at least r1 ~ eff : r2

and nice solution with the Trade!!!