<p>In the context of pure type systems (say Calculus of Constructions) I am looking for references discussing the properties of the following polymorphic type: <span class="math-container">$\Pi t : * . ((t \to t) \to t) \to t$</span>. What I notice is that this type could in principle be used to encode pairs of naturals as follows:
<span class="math-container">$$
  (m, n) := \lambda t : * . \lambda f : (t \to t) \to t . (g ^ m \ (f \ g ^ n))
$$</span>
where powers stand for repeated applications and <span class="math-container">$g := \lambda x : t . (f \ \lambda y : t . x)$</span>. For the intuition about how it works, the type of <span class="math-container">$g$</span> is <span class="math-container">$t \to t$</span>, so we can apply <span class="math-container">$f$</span> to <span class="math-container">$g ^ n$</span> to obtain a value of type <span class="math-container">$t$</span>, and then we can repeatedly apply <span class="math-container">$g$</span> to obtain additional values of type <span class="math-container">$t$</span>.</p>
<p>Working with pairs of naturals encoded this way is probably more tedious than using the regular Church encoding, but I find this idea nevertheless interesting because we're able to get two numbers from a type that has the same number of <code>t</code>s in its signature, and we're able to do so starting from the identity function, which is in some sense external, because it is not provided as an argument, like zero is for the Church encoding. But so far I was unable to find any research related to this (which can also be because I am unaware if this type has a name already or not).</p>

CC BY-SA 4.0
2021-11-29T18:02:31.300Z
If I am reading your suggestion correctly, then $f^2 (\lambda x : t . x)$ does not type, does it? The type of $f (\lambda x : t . x)$ is $t$, and so we cannot apply $f$ to it.
Andrej Bauer
CC BY-SA 4.0
2021-11-30T08:47:40.570Z
@AndrejBauer You are correct, of course. I was writing from memory instead of my notes and got it wrong. $f$ does not compose with itself, only $g$ does, so $g$ needs to be used for the second element of the pair also. I have corrected the formula to reflect this.
Cristian Gratie
CC BY-SA 4.0
2021-11-30T08:57:47.110Z
Can you define the first and the second projection?
Andrej Bauer
CC BY-SA 4.0
2021-11-30T15:13:56.793Z
Yes, sort of. Consider a context where we have $s: t \to t$ and $z: t$ (from the Church encoding of naturals) and a (meta) natural number $p > 0$. We define $f := \lambda h : t \to t . s \ (h ^ p \ z)$ and we have $g := \lambda x : t . (f \ \lambda y : t . x) = \lambda x : t . (s \ x) = s$. With this, $(g ^ m \ (f \ g ^ n)) = (s ^ m \ (s \ (s^{np} \ z)))$ which is the encoding of $m + np + 1$. From these we can recover $m$ and $n$. I don't know if there is a simpler way to get them.
Cristian Gratie
CC BY-SA 4.0
2021-11-30T18:34:05.237Z
If what you wrote is right, then you can do this for $p = 2$ and $p = 3$. This gives you a system of two equations $m + 2 n + 1 = a$ and $m + 3 n + 1 = b$, from which it follows that $n = b - a$ and $m = 3 a - 2 b - 1$.
Andrej Bauer
CC BY-SA 4.0
2021-11-30T19:51:15.937Z
Yes, that would work also with $p = 1$ and $p = 2$ but the end result is pretty ugly due to the fact of needing to compute subtractions. It's why I was wondering if there is any research on this polymorphic type which would at least highlight its already known properties.
Cristian Gratie
CC BY-SA 4.0
2021-12-01T07:45:46.167Z
Ah true, you said $p  > 0$ and I somehow read that as $p > 1$. What's wrong with subtraction? But this is interesting. Here's another question whose answer might further illuminate things. Is $N \times N$ where $N = \Pi t : * . (t \to t) \to (t \to t)$ a retract of your type? It looks like it is, via the projections.
Andrej Bauer
<type-systems><calculus-of-constructions>
Properties of the polymorphic type $\Pi t : * . ((t \to t) \to t) \to t$
Cristian Gratie
# Properties of the polymorphic type $\Pi t : * . ((t \to t) \to t) \to t$

(Asked by: username_0 on 2021-11-29)

In the context of pure type systems (say Calculus of Constructions) I am looking for references discussing the properties of the following polymorphic type: $\Pi t : \* . ((t \to t) \to t) \to t$. What I notice is that this type could in principle be used to encode pairs of naturals as follows:
$$
(m, n) := \lambda t : \* . \lambda f : (t \to t) \to t . (g ^ m \ (f \ g ^ n))
$$
where powers stand for repeated applications and $g := \lambda x : t . (f \ \lambda y : t . x)$. For the intuition about how it works, the type of $g$ is $t \to t$, so we can apply $f$ to $g ^ n$ to obtain a value of type $t$, and then we can repeatedly apply $g$ to obtain additional values of type $t$.

Working with pairs of naturals encoded this way is probably more tedious than using the regular Church encoding, but I find this idea nevertheless interesting because we're able to get two numbers from a type that has the same number of `t`s in its signature, and we're able to do so starting from the identity function, which is in some sense external, because it is not provided as an argument, like zero is for the Church encoding. But so far I was unable to find any research related to this (which can also be because I am unaware if this type has a name already or not).

**Tags:** type-systems, calculus-of-constructions

> **Comments:**
> **username_1**: If I am reading your suggestion correctly, then $f^2 (\lambda x : t . x)$ does not type, does it? The type of $f (\lambda x : t . x)$ is $t$, and so we cannot apply $f$ to it.  
> **username_0**: @AndrejBauer You are correct, of course. I was writing from memory instead of my notes and got it wrong. $f$ does not compose with itself, only $g$ does, so $g$ needs to be used for the second element of the pair also. I have corrected the formula to reflect this.  
> **username_1**: Can you define the first and the second projection?  
> **username_0**: Yes, sort of. Consider a context where we have $s: t \to t$ and $z: t$ (from the Church encoding of naturals) and a (meta) natural number $p > 0$. We define $f := \lambda h : t \to t . s \ (h ^ p \ z)$ and we have $g := \lambda x : t . (f \ \lambda y : t . x) = \lambda x : t . (s \ x) = s$. With this, $(g ^ m \ (f \ g ^ n)) = (s ^ m \ (s \ (s^{np} \ z)))$ which is the encoding of $m + np + 1$. From these we can recover $m$ and $n$. I don't know if there is a simpler way to get them.  
> **username_1**: If what you wrote is right, then you can do this for $p = 2$ and $p = 3$. This gives you a system of two equations $m + 2 n + 1 = a$ and $m + 3 n + 1 = b$, from which it follows that $n = b - a$ and $m = 3 a - 2 b - 1$.  
> **username_0**: Yes, that would work also with $p = 1$ and $p = 2$ but the end result is pretty ugly due to the fact of needing to compute subtractions. It's why I was wondering if there is any research on this polymorphic type which would at least highlight its already known properties.  
> **username_1**: Ah true, you said $p  > 0$ and I somehow read that as $p > 1$. What's wrong with subtraction? But this is interesting. Here's another question whose answer might further illuminate things. Is $N \times N$ where $N = \Pi t : * . (t \to t) \to (t \to t)$ a retract of your type? It looks like it is, via the projections.  

---

## 0 answers

