Uncurrying and Polymorphism

The other answers are good, I just wanted to make it explicit that currying for dependent types is $$ textstyle prod (x : A) . prod (y : B(x)) . C(x, y) cong prod (p : sum (x : A) . B(x)) . C(pi_1(p), pi_2(p)) $$ which is more suggestive in Agda-style notation: $$ (x : A) to (y : B(x)) to C(x,y) cong (p : (x : A) times B(x)) to C(pi_1(p), pi_2(p)) $$ In your case, replace $Pi$ and $Sigma$ with $forall$ and $exists$.

The uncurrying process will lead to existential types. Since the adjoint of $(Xto)$ is $(Xtimesvphantom{Y})$ and the adjoint of $(forall X.)$ is $(exists X.)$, it is appearently inevitable. Also, it will lead to types depending on terms (where simple types only depends on types themselves, and polymorphism allows terms to depend on types). So generally it is not doable in your restricted type system.

Let's write these in more suggestive notations. The usual currying/uncurrying converts between $X to Y to Z$ and $X times Y to Z$. But the former can be written in the product notation: $prod_{x:X} prod_{y:Y} Z$, where $prod_{y:Y}Z$ means the product of many copies of $Z$, one for each element $y$ of $Y$, which is a function from $Y$ to $Z$. The latter can be written as $prod_{p:Xtimes Y} Z$. And $A times B$ can be rewritten as $sum_{a:A}B$, which is the sum of many copies of $B$, one for each element $a$ of $A$.

This notation is easily generalized to polymorphic types (or even more generally, dependent types), simply by allowing the inner expression to depend on the variable: $prod_{X : *} X to A$ means the product of $X to A$ for every type $X$. So we can make the more general currying/uncurrying process: $$prod_{x:X}prod_{y:Y_x} Z_{x, y} Leftrightarrow prod_{p:sum_{x:X} Y_x} Z_{pi_1(p), pi_2(p)},$$ where $pi_i(p)$ is the projection that selects the $i$-th element.

---

Back to the question itself. The first one is actually a function of three arguments. So just turning it into $forall X. (Xtimes mathtt{int}) to X$ is just uncurrying the second and third argument. The uncurried form neccesarily involves dependent types: $forall (p:exists X. Xtimes mathtt{int}). pi_1(p)$. The rest can be done similarly.

I can only think of some uncurrying of 1 and 3.

1. $forall X. (X times int) rightarrow X$
2. It looks like we can not uncurry this one, unless we transform it first into the isomorphic type 1.
3. $int rightarrow forall X. (X times int) rightarrow X$

Alternatively, if we can apply an isomorphism, (3) can be rewritten as $$ forall X. int rightarrow (X times int) rightarrow X $$ and then, by uncurrying $$ forall X. (int times X times int) rightarrow X $$

---

In my view, it is more interesting when we also have existential types in the calculus and the returned type does not involve $X$. E.g., we can perform a kind of uncurring on $$ forall X. X rightarrow (X rightarrow int) rightarrow int $$ and get $$ (exists X. X times (X rightarrow int)) rightarrow int $$ which is isomorphic to $$ int rightarrow int $$