In https://link.springer.com/content/pdf/10.1007/s10670-019-00128-z.pdf , page 16, the following clause is given for a modal operator $\langle R_k \rangle$ (see definition 4.2 for the definition of a model):
$$\mathfrak{M},\, w \models \langle R_k \rangle \, \phi \,\text{ if and only if } \mathfrak{M'}, w \models \phi \text{ for some } (\mathfrak{M'},\, w) \, \text{ which is } R_k\text{-accessible from }(\mathfrak{M},\, w) \tag{*}$$
$\langle R_k \rangle$ effects a model transformation. Roughly (see the paper for details, definitions 4,5 and 6), a model $(\mathfrak{M'},\, w)$ is $R_k$-accessible from a model $(\mathfrak{M},\, w)$ if $\mathfrak{M'}$ contains worlds that have been generated in a certain way by applying $R_k$ to certain propositions that are true at certain worlds, where $R_k$ is a rule of inference (see definitions 5 and 6 of the paper above for details). So if a world verifies $p$ and $p \to q$ but neither verifies nor falsifies $q$ and $R_k$ is modus ponens, then we generate a world in which $p$, $p \to q$ and $q$ are true. For each world $w$ in a certain set of worlds in the original model, we generate a set of worlds, the worlds reachable by applying $R_k$ in some way to $w$. From this set of sets of worlds, a function $\mathcal{C} ∶ \mathcal{P}(\mathcal{P}(\mathcal{W})) \to \mathcal{P}(\mathcal{P}(\mathcal{W}))$ takes a set $\mathcal{W} = \{W_1,...,W_n \}$ of sets of worlds as input and returns the set of sets of worlds which results from all the ways in which exactly one element can be picked from each non-empty $W_i \in \mathcal{W}$. The $R_k$-accessible models then consist of those models whose worlds are chosen in this way.
Formulas like $\langle R_k \rangle B \, \phi$--where $B$ is a doxastic modal operator of some kind--when evaluated at a model $\mathfrak{M}$ and a world $w$ then express that, agent $a$ can believe $\phi$ after applying the inference rule $R_k$ in some way.
In the simply-typed lambda calculus with types $m, s,t$ and $e$, respectively, for models $(\mathfrak{M}, w)$ worlds, booleans and individuals, we could express ($*$) dispensing with $\langle R_k \rangle$,given a predicate symbol $\mathcal{R_k}$, representing that a model is $R_k$-accessible from another model (we subscript expressions with their types, and use $\to$ to form function types):
$$\lambda p_{m \to s \to t}\lambda l_{m},w_s. \exists l'_{m}(\mathcal{R_k}(l)(l')\, \land \,p(l')(w)) \tag{**}$$
We can then imagine a triple $(\bigcirc, \eta, \bigstar)$, which behaves like the 'reader/environment monad' (see https://ncatlab.org/nlab/show/function+monad, and https://arxiv.org/pdf/cs/0205026.pdf, page 289), and is defined as follows:
$$\bigcirc \,\alpha = m \to \alpha \;\;\;\; \text{for all types } \alpha$$
$$\eta(a) = \lambda l_m.a \;\;\;\; \text{for all } a_\alpha$$
$$n \bigstar k = \lambda l_m. k(n(l))(l) \;\;\;\; \text{for all }n_{\bigcirc \, \alpha}, k_{\alpha \to \bigcirc \beta}.$$
With this monad, (**) would be an expression of type $\bigcirc(s \to t) \to \bigcirc (s \to t)$.
I am looking for another way to implement the model transformation operator $\langle R_k \rangle$ in the simply-typed lambda calculus, using monads, as I have outline above, but which does not use the reader monad.
I thought maybe that the power set monad (https://en.wikipedia.org/wiki/Monad_(category_theory)#The_power_set_monad) might help in generating the worlds reachable by the $R_k$ transformation, but I'm not sure.
Can anyone help me?