Suppose I have a term $ a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $ \alpha, \beta, \gamma$ stand for arbitrary types) and I want to **lift** it to a term

$ \lambda x_{\beta}. \;(x, \, a)$

I could use a function $ \lambda z_{\alpha}, x. \;(x,\, z)$ .

Suppose we then form $ (b, a) : \beta \times \alpha$ , by applying $ \lambda x_{\beta}. \;(x, \, a)$ to $ \,b_{\beta}$ .

We might want to add $ c$ to the beginning of this to form $ (c, b, a) : \gamma \times \beta \times \alpha$ . We could do this (here $ \pi_1$ and $ \pi_2$ are projections)) by having a function $ \lambda z’_{\beta \times \alpha}, z. \,(z,\, \pi_1 z’,\, \pi_2 z’)$ . And again, we could cook up a function to form $ (d,\, c,\, b,\, a)$ and $ (e,\,d,\, c,\, b,\, a)$ (so on and so forth).

I could do things in the way above; however, I wondered whether there was a way of doing this kind of operation via an applicative or a monad. Then I could (ideally) use the operations of the monad or applicative, to lift term $ a$ (perhaps into $ \lambda x.\,(x, \, a)$ , and then form these tuples $ (b, a), (c, b, a), (d, c, b, a)$ , etc, by the operations of the monad or applicative.

If you know a way of doing this I would be very interested.