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 ts 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).

  • $\begingroup$ 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. $\endgroup$ Nov 29 '21 at 18:02
  • $\begingroup$ @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. $\endgroup$ Nov 30 '21 at 8:47
  • $\begingroup$ Can you define the first and the second projection? $\endgroup$ Nov 30 '21 at 8:57
  • $\begingroup$ 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. $\endgroup$ Nov 30 '21 at 15:13
  • 1
    $\begingroup$ 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. $\endgroup$ Dec 1 '21 at 7:45

Your Answer

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

Browse other questions tagged or ask your own question.