Example of a term in system F which is not typable in the simply typed lambda calculus

Question

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

Answer 1

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

Answer 2

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

Answer 3

Damiano Mazza'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 = <fun>

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