2
$\begingroup$

How do we uncurry functions when they are polymorphic? For example, is it possible to uncurry the following types? If so what is the uncurried type?

  1. $\forall X. X \rightarrow int \rightarrow X$ ?
  2. $int \rightarrow \forall X. X \rightarrow X$ ?
  3. $int \rightarrow \forall X. X \rightarrow int \rightarrow X$ ?
$\endgroup$
4
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
2
$\begingroup$

The uncurrying process will lead to existential types. Since the adjoint of $(X\to)$ is $(X\times\vphantom{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:X\times 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. (X\times \mathtt{int}) \to X$ is just uncurrying the second and third argument. The uncurried form neccesarily involves dependent types: $\forall (p:\exists X. X\times \mathtt{int}). \pi_1(p)$. The rest can be done similarly.

| cite | improve this answer | |
$\endgroup$
1
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ I am confused on the use of existential types. Is there a reference paper that I can read? $\endgroup$ – Ram May 21 at 21:24
  • $\begingroup$ On uncurrying (3), is that not (int x (\forall X. (X x int))) -> X ? $\endgroup$ – Ram May 21 at 21:27
  • $\begingroup$ @Ram I can't recall a nice paper on that, sorry. Your (3) is wrong, since the scope of the $\forall$ extends until the end: your last $X$ would be unbound in your type. The original type has roughly the form $int \to (\forall X.\ something \to X)$ and you can't uncurry that (unless you first lift the forall at the top level -- that would be correct). I added that above. $\endgroup$ – chi May 21 at 21:43
  • $\begingroup$ Just curious, why can't we uncurry (2) as $\forall X. (int \times X ) \to X$? $\endgroup$ – BearAqua Jun 21 at 1:01
  • $\begingroup$ @BearAqua It depends on what exactly we call "currying". Your (2) is isomorphic to the original (2), but lifts the $\forall X$ outerwards, and then curries the arguments. So, to me it's "lifting, then currying" rather than "currying alone". In my answer above, I wrote "unless we transform it first into the isomorphic type 1" to address this option. $\endgroup$ – chi Jun 21 at 7:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.