<p>Every normal term may be typed in system F (I can't seem to find a reference now, I'll come back with one when I have some more time).  So, for example, letting <span class="math-container">$A:=\forall X.X$</span>, then</p>
<p><span class="math-container">$$x^A(A\to\alpha)x^A:\alpha.$$</span></p>
<p>The erasure of that term is the self-application <span class="math-container">$xx$</span>, which is obviously not simply-typable.</p>
<hr />
<p>For completeness, here's a proof that every normal <span class="math-container">$\lambda$</span>-term is typable in system F.  This statement makes sense in Curry-style system F, but here we are using Church-style system F, so we are going to prove the following instead: for every normal <span class="math-container">$\lambda$</span>-term <span class="math-container">$M$</span>, there exists a system F term whose erasure is <span class="math-container">$M$</span>.</p>
<p>The proof is by induction on the structure of <span class="math-container">$M$</span>, and we are going to prove something stronger: the term whose erasure is <span class="math-container">$M$</span> will have all of its free variables of type <span class="math-container">$\bot:=\forall\beta.\beta$</span>.</p>
<p>Since <span class="math-container">$M$</span> is normal, it is of the form
<span class="math-container">$$\lambda x_1\ldots\lambda x_n.yN_1\ldots N_k$$</span>
with <span class="math-container">$N_1,\ldots,N_k$</span> themselves normal. By the induction hypothesis, there exist <span class="math-container">$N_1^+:A_1,\ldots,N_k^+:A_k$</span> system F terms as stated above such that the erasure of <span class="math-container">$N_i^+$</span> is <span class="math-container">$N_i$</span>. We therefore let
<span class="math-container">$$M^+:=\lambda x_1^\bot\ldots\lambda x_n^\bot.y^\bot(A_1\to\cdots\to A_k\to\alpha)N_1^+\ldots N_k^+:\bot\to\cdots\to\bot\to\alpha,$$</span>
and we are done.  The fact that <span class="math-container">$y$</span> may be given type <span class="math-container">$\bot$</span> is where we use the extra hypothesis that every free variable of every <span class="math-container">$N_i^+$</span> has type <span class="math-container">$\bot$</span>: <span class="math-container">$y$</span> may appear free in one of these terms, so we cannot choose its type arbitrarily.</p>
<p>Retrospectively, the above proof is saying that every normal <span class="math-container">$\lambda$</span>-term may be seen as a (very contrived!) proof of &quot;false implies whatever&quot;.  If some information is known about free variables (how many occurrences, if every occurrence is applied to the same number of arguments, etc.), then less trivial tautologies may be obtained, as shown in the other answers.  But in general, the above observation gives a pretty strong constraint on the type of free variables, so I am not sure that there is uniform argument working in all cases and avoiding the uninhabited type <span class="math-container">$\bot$</span>.</p>

CC BY-SA 4.0
2023-12-22T19:54:08.097Z
Since I was asking for a closed term, that would be $Λα.λ(x:∀α.α).x((∀β.β)\to α)x$ in the notations of the question, with type $∀α.(∀β.β)\to α$. Very nice, thank you! I'd appreciate a reference for the initial claim when you can find one.
Gro-Tsen
CC BY-SA 4.0
2023-12-24T12:45:36.647Z
It's funny, this is well-known but I can't find a reference with a proof.  I thought that Sørensen and Urzyczyn's [Lecture Notes on the Curry-Howard Isomorphism](https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/curry-howard.pdf) would say something about this, but it's only listed as an exercise in the chapter on system F (Exercise 12.7.12).  Anyway, it really is an exercise, and I updated the answer with a possible solution.
Damiano Mazza
CC BY-SA 4.0
2023-12-22T19:07:33.400Z
2023-12-27T13:39:02.137Z
2023-12-27T13:39:02.137Z
Damiano Mazza
<p>Reacting to the previous answers, I think this is the simplest self-application which only contains types which have closed inhabitants.</p>
<p><span class="math-container">$$\lambda\,(f\,:\,\forall\,\alpha.\,\alpha\to\alpha).\,f\,(\forall\,\alpha.\,\alpha\to\alpha)\,f$$</span></p>

CC BY-SA 4.0
2023-12-22T20:05:57.977Z
Ah! Interesting that we can write a $Λ$-less term! $λ(f:∀α.α\to α).f(∀α.α\to α)f$ has type $(∀α.α\to α) \to (∀α.α\to α)$ but, shall we say, an “unusual proof” of the latter.
Gro-Tsen
CC BY-SA 4.0
2023-12-22T19:57:48.283Z
2023-12-22T19:57:48.283Z
András Kovács
<p>Damiano Mazza's example uses an uninhabited type, <span class="math-container">$∀ X ⋅ X$</span>. It is correct, but raises the obvious question whether one can do without. Here is an example that I find quite natural:</p>
<p><span class="math-container">$$Λ \ A B ⋅ λ \ (p : ∀ O ⋅ ((A → B) → A → O) → O) ⋅\\ p\ (A → B)\ (λ \ (f : A → B) (a : A) ⋅ f)\ (p\ A \ (λ\ (f : A → B) (a : A) ⋅ \ a))$$</span></p>
<p>which is to be understood as the Scheme code</p>
<pre><code>(lambda (pair)
  ((car pair) (cdr pair)))
</code></pre>
<p>or the OCaml code</p>
<pre><code># let app pair = let (f, a) = pair in f a;;
val app : ('a -&gt; 'b) * 'a -&gt; 'b = &lt;fun&gt;
</code></pre>
<p>This is well-typed in system F, but the corresponding term with types erased,</p>
<p><span class="math-container">$$λ p ⋅ p \ (λ\ f\ a ⋅ f)\ (p\ (λ\ f\ a ⋅ a))$$</span></p>
<p>is untypable with simple types: since <span class="math-container">$p$</span> is applied, it must have some type <span class="math-container">$X → Y$</span>, but it is never possible to apply a term of some type <span class="math-container">$Y$</span> to a term of the same type <span class="math-container">$Y$</span>.</p>
<p>The intuition behind this is that in system F, you can encode pairs and retain the ability to extract either of their components. In st-λc, when you construct a pair, you must choose in advance what you want to be able to get out of it, since the pair encoding fixes the &quot;result&quot; type. The term above takes a pair of type <span class="math-container">$X × Y$</span> and tries to extract both the first component and the second component, which forces <span class="math-container">$X = Y$</span>. And it applies a term of type <span class="math-container">$X$</span> to a term of type <span class="math-container">$Y$</span>, which forces <span class="math-container">$X ≠ Y$</span>.</p>

CC BY-SA 4.0
2023-12-22T19:51:49.550Z
2023-12-22T19:51:49.550Z
Jean Abou Samra
<p>What is the simplest possible example of a (correctly typed) term in system F that does not correspond to any correctly typed term in the simply typed λ-calculus?</p>
<p>More precisely, I am looking for a closed well-typed term in system F, i.e., something like
<span class="math-container">$$
\Lambda \alpha.  \lambda (f:\alpha\to\alpha). \lambda (x:\alpha). f(f x)
$$</span>
(where I wrote <span class="math-container">$\Lambda$</span> for abstraction on types) such that, if we remove all <span class="math-container">$\Lambda$</span> and type variables, and all type annotations on <span class="math-container">$\lambda$</span>, the resulting term (of the <em>untyped</em> λ-calculus), which in my example would be
<span class="math-container">$$
\lambda f. \lambda x. f(fx)
$$</span>
does <em>not</em> correspond to the removing of type annotations from a term of the simply-typed λ-calculus (over an infinite stock of type variables).  Of course, the above example doesn't work (we can just write <span class="math-container">$\lambda (f:\alpha\to\alpha). \lambda (x:\alpha). f(f x)$</span>), or I wouldn't be asking the question; nor can any example where all <span class="math-container">$\Lambda$</span>'s are prenex.</p>
<p>But note that I'm not just asking for a term of system F which cannot be “faithfully” typed into the s.t.λ.c., I'm asking for one which cannot be typed <em>at all</em>: for example, even though
<span class="math-container">$$
\Lambda\alpha. \; \lambda(h:\forall \gamma.(\alpha\to\gamma)\to\gamma). \;
h\alpha(\lambda(x:\alpha).x)
$$</span>
has type <span class="math-container">$\forall\alpha.(\forall \gamma.(\alpha\to\gamma)\to\gamma)\to\alpha$</span> which has no obvious analogue in the s.t.λ.c., the deannotated term
<span class="math-container">$$
\lambda h. h(\lambda x.x)
$$</span>
can still be typed in the latter as <span class="math-container">$((\delta\to\delta)\to\beta)\to\beta$</span>, thus not answering my question.</p>
<p>I believe there is a term such as I ask, because system F is so much powerful than the s.t.λ.c. so certainly there should be strictly more functions in the untyped λ-calculus that are somehow typable in system F than in the s.t.λ.c.  But I couldn't find a concrete example of one (I guess coding an interpreter of the s.t.λ.c. in system F is possible and answers my question, but I imagine there's a waaaaay simpler term than that).</p>

<type-theory><lambda-calculus><type-inference>
Example of a term in system F which is not typable in the simply typed lambda calculus
Gro-Tsen
# Example of a term in system F which is not typable in the simply typed lambda calculus

(Asked by: username_0 on 2023-12-22)

What is the simplest possible example of a (correctly typed) term in system F that does not correspond to any correctly typed term in the simply typed λ-calculus?

More precisely, I am looking for a closed well-typed term in system F, i.e., something like
$$
\Lambda \alpha. \lambda (f:\alpha\to\alpha). \lambda (x:\alpha). f(f x)
$$
(where I wrote $\Lambda$ for abstraction on types) such that, if we remove all $\Lambda$ and type variables, and all type annotations on $\lambda$, the resulting term (of the *untyped* λ-calculus), which in my example would be
$$
\lambda f. \lambda x. f(fx)
$$
does *not* correspond to the removing of type annotations from a term of the simply-typed λ-calculus (over an infinite stock of type variables). Of course, the above example doesn't work (we can just write $\lambda (f:\alpha\to\alpha). \lambda (x:\alpha). f(f x)$), or I wouldn't be asking the question; nor can any example where all $\Lambda$'s are prenex.

But note that I'm not just asking for a term of system F which cannot be “faithfully” typed into the s.t.λ.c., I'm asking for one which cannot be typed *at all*: for example, even though
$$
\Lambda\alpha. \; \lambda(h:\forall \gamma.(\alpha\to\gamma)\to\gamma). \;
h\alpha(\lambda(x:\alpha).x)
$$
has type $\forall\alpha.(\forall \gamma.(\alpha\to\gamma)\to\gamma)\to\alpha$ which has no obvious analogue in the s.t.λ.c., the deannotated term
$$
\lambda h. h(\lambda x.x)
$$
can still be typed in the latter as $((\delta\to\delta)\to\beta)\to\beta$, thus not answering my question.

I believe there is a term such as I ask, because system F is so much powerful than the s.t.λ.c. so certainly there should be strictly more functions in the untyped λ-calculus that are somehow typable in system F than in the s.t.λ.c. But I couldn't find a concrete example of one (I guess coding an interpreter of the s.t.λ.c. in system F is possible and answers my question, but I imagine there's a waaaaay simpler term than that).

**Tags:** type-theory, lambda-calculus, type-inference


---

## 3 answers

### Answer by username_1 on 2023-12-22. Score: 7 | Accepted answer

Every normal term may be typed in system F (I can't seem to find a reference now, I'll come back with one when I have some more time). So, for example, letting $A:=\forall X.X$, then

$$x^A(A\to\alpha)x^A:\alpha.$$

The erasure of that term is the self-application $xx$, which is obviously not simply-typable.

---

For completeness, here's a proof that every normal $\lambda$-term is typable in system F. This statement makes sense in Curry-style system F, but here we are using Church-style system F, so we are going to prove the following instead: for every normal $\lambda$-term $M$, there exists a system F term whose erasure is $M$.

The proof is by induction on the structure of $M$, and we are going to prove something stronger: the term whose erasure is $M$ will have all of its free variables of type $\bot:=\forall\beta.\beta$.

Since $M$ is normal, it is of the form
$$\lambda x\_1\ldots\lambda x\_n.yN\_1\ldots N\_k$$
with $N\_1,\ldots,N\_k$ themselves normal. By the induction hypothesis, there exist $N\_1^+:A\_1,\ldots,N\_k^+:A\_k$ system F terms as stated above such that the erasure of $N\_i^+$ is $N\_i$. We therefore let
$$M^+:=\lambda x\_1^\bot\ldots\lambda x\_n^\bot.y^\bot(A\_1\to\cdots\to A\_k\to\alpha)N\_1^+\ldots N\_k^+:\bot\to\cdots\to\bot\to\alpha,$$
and we are done. The fact that $y$ may be given type $\bot$ is where we use the extra hypothesis that every free variable of every $N\_i^+$ has type $\bot$: $y$ may appear free in one of these terms, so we cannot choose its type arbitrarily.

Retrospectively, the above proof is saying that every normal $\lambda$-term may be seen as a (very contrived!) proof of "false implies whatever". If some information is known about free variables (how many occurrences, if every occurrence is applied to the same number of arguments, etc.), then less trivial tautologies may be obtained, as shown in the other answers. But in general, the above observation gives a pretty strong constraint on the type of free variables, so I am not sure that there is uniform argument working in all cases and avoiding the uninhabited type $\bot$.

> **Comments:**
> **username_0**: Since I was asking for a closed term, that would be $Λα.λ(x:∀α.α).x((∀β.β)\to α)x$ in the notations of the question, with type $∀α.(∀β.β)\to α$. Very nice, thank you! I'd appreciate a reference for the initial claim when you can find one.  
> **username_1**: It's funny, this is well-known but I can't find a reference with a proof.  I thought that Sørensen and Urzyczyn's [Lecture Notes on the Curry-Howard Isomorphism](https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/curry-howard.pdf) would say something about this, but it's only listed as an exercise in the chapter on system F (Exercise 12.7.12).  Anyway, it really is an exercise, and I updated the answer with a possible solution.  

---

### Answer by username_2 on 2023-12-22. Score: 10

Reacting to the previous answers, I think this is the simplest self-application which only contains types which have closed inhabitants.

$$\lambda\,(f\,:\,\forall\,\alpha.\,\alpha\to\alpha).\,f\,(\forall\,\alpha.\,\alpha\to\alpha)\,f$$

> **Comments:**
> **username_0**: Ah! Interesting that we can write a $Λ$-less term! $λ(f:∀α.α\to α).f(∀α.α\to α)f$ has type $(∀α.α\to α) \to (∀α.α\to α)$ but, shall we say, an “unusual proof” of the latter.  

---

### Answer by username_3 on 2023-12-22. Score: 7

username_1's example uses an uninhabited type, $∀ X ⋅ X$. It is correct, but raises the obvious question whether one can do without. Here is an example that I find quite natural:
$$Λ \ A B ⋅ λ \ (p : ∀ O ⋅ ((A → B) → A → O) → O) ⋅\\ p\ (A → B)\ (λ \ (f : A → B) (a : A) ⋅ f)\ (p\ A \ (λ\ (f : A → B) (a : A) ⋅ \ a))$$
which is to be understood as the Scheme code
(lambda (pair)
  ((car pair) (cdr pair)))

or the OCaml code
# let app pair = let (f, a) = pair in f a;;
val app : ('a -> 'b) * 'a -> 'b = 

This is well-typed in system F, but the corresponding term with types erased,
$$λ p ⋅ p \ (λ\ f\ a ⋅ f)\ (p\ (λ\ f\ a ⋅ a))$$
is untypable with simple types: since $p$ is applied, it must have some type $X → Y$, but it is never possible to apply a term of some type $Y$ to a term of the same type $Y$.
The intuition behind this is that in system F, you can encode pairs and retain the ability to extract either of their components. In st-λc, when you construct a pair, you must choose in advance what you want to be able to get out of it, since the pair encoding fixes the "result" type. The term above takes a pair of type $X × Y$ and tries to extract both the first component and the second component, which forces $X = Y$. And it applies a term of type $X$ to a term of type $Y$, which forces $X ≠ Y$.


---

