*Bounty: 50*

*Bounty: 50*

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.