# Constructing a monad via type synonyms of a particular kind

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$$?