We can define a reader/environment monad on the simply-typed lambda calculus, using the following three equations, where $ r$ is some fixed type, $ \alpha$ is any type (I subscript some terms with their types), $ \mathbb{M}$ is the proposed monadic type modality), $ \eta$ is the *unit* of the monad and $ \mu:\mathbb{M} \mathbb{M}\alpha → \mathbb{M}\alpha$ is the *join* of the monad:

$ $ \mathbb{M} \thinspace α = r → α \hspace{1cm} ∀α$ $ $ $ \eta \, a_{\alpha} = \lambda c_{r}.\; a \hspace{2cm} ∀a_{\alpha}$ $ $ $ \mu\,b_{\mathbb{M}\mathbb{M} \alpha} = λc_{r}.\; b_{\mathbb{M}\mathbb{M}\alpha}\, c\, c \hspace{1cm} ∀b_{\mathbb{M}\mathbb{M} \alpha} $ $

Can we always construct a reader monad by type synonyms of the form $ r = x$ , for arbitrary function types $ x$ (for example, where $ x$ is $ (\beta \to t) \to t$ ), for some type $ \beta$ ?