# Why is the type ∀t.t un-inhabited in System F?

How do you prove that there exists no term with the type $$\forall t. t$$ in System F?

I tried searching through Pierce's TAPL and Reynold's ToPL, but could not find anything. I suspect that the proof may involve some kind of model theoritic argument, but I fail to see where to start.

• To start with, do you understand intuitively why there should be no term with that type? Commented Jan 20, 2020 at 16:16
• Kind of, basically it would mean that if such a term existed then the term would belong to all possible types. Commented Jan 20, 2020 at 16:25
• It would be more accurate to say that such a term would represent a function where you give it any type and it gives you back a value of that type. So you could substitute any uninhabited type for $t$ in the term of type $\forall t. t$ to get a value of that uninhabited type—a contradiction. (This is not a complete proof by itself because you would also need to show that System F has an uninhabited type.) Commented Jan 20, 2020 at 16:36

The simplest proof is giving a model where types are interpreted as propositions, and terms as proofs, then observing that $$\forall \alpha.\alpha$$ is interpreted as the false proposition, so any $$\cdot \vdash t : \forall \alpha.\alpha$$ would be a proof of falsehood. It is important to remember that $$\forall \alpha.\alpha$$ is only uninhabited for sure in the empty context $$\cdot$$, in other contexts it may be trivially inhabited.

Concretely, first interpret each $$A$$ type with $$n$$ free type variables in the following way:

\begin{alignat*}{2} & [\![ A ]\!] && : \mathsf{Bool}^n \to \mathsf{Bool}\\ & [\![ \alpha ]\!]\,\gamma && := \text{\alpha-th component of \gamma}\\ & [\![ A \to B ]\!]\,\gamma && := [\![ A ]\!]\,\gamma \Rightarrow [\![ B ]\!]\,\gamma\\ & [\![ \forall \alpha.\,B]\!]\,\gamma && := [\![B]\!]\,(\mathsf{true},\,\gamma)\,\land\,[\![B]\!]\,(\mathsf{false},\,\gamma) \end{alignat*}

Interpret every typing context $$\Gamma$$ with $$n$$ free type variables as:

\begin{alignat*}{2} & [\![\Gamma]\!] : \mathsf{Bool}^n\to \mathsf{Bool}\\ & [\![\Gamma]\!]\,\gamma := \bigwedge\limits_{A\,\in\,\Gamma}\,[\![A]\!]\,\gamma \end{alignat*}

Then show for each $$\Gamma \vdash t : A$$ term, that for each truth valuation $$\gamma : \mathsf{Bool}^n$$, if $$[\![\Gamma]\!]\,\gamma = \mathsf{true}$$, then $$[\![A]\!]\,\gamma = \mathsf{true}$$. This can be done by induction on terms.

Now, $$[\![\forall \alpha.\alpha]\!]$$ with no free type variables evaluates to $$\mathsf{false}$$, since it's $$\mathsf{true}$$ when $$\alpha$$ is instantiated to $$\mathsf{true}$$, and $$\mathsf{false}$$ when it's instantiated to $$\mathsf{false}$$, and the conjunction of these is $$\mathsf{false}$$. Assuming $$\cdot\vdash t : \forall \alpha.\alpha$$, we have by the previous result that $$[\![\forall \alpha.\alpha]\!]$$ is $$\mathsf{true}$$, a contradiction, hence there is no $$\cdot\vdash t : \forall \alpha.\alpha$$.

• Thank you for your answer! I can see the structure of the proof now. Can you please help me understand how do you read the equation [[∀𝛼.𝐵]]𝛾 :=[[𝐵]](𝗍𝗋𝗎𝖾,𝛾)∧[[𝐵]](𝖿𝖺𝗅𝗌𝖾,𝛾) Commented Jan 21, 2020 at 15:07
• @ApoorvIngle the line is the definition of the Bool^n -> Bool function in the case when a type is a forall-quantified type. It says that a quantified type yields true in a truth-valuation environment if it yields true no matter how the bound alpha variable is interpreted (i.e. as true or as false). Commented Jan 21, 2020 at 15:34
• We interpret each closed type as either true (a "true proposition") or false (a "false proposition"). Since a universally quantified type ranges over arbitrary types, we have in the model that a forall-type is true iff it's true when it is instantiated with a true proposition plus also true when it is instantiated with a false proposition. Commented Jan 21, 2020 at 15:39

There is a proof by using parametricity/logical relations framework or free theorems as mentioned in Zhao et al.[1]

For instance, we can conclude that there is no closed inhabitant of type ∀α.α in a pure setting. If there were such a term, it must yield a value of any type at which it is instantiated, but there is no uniform algorithm to compute a value at any type. Therefore, ∀α.α is an empty type.

[1]: Zhao J., Zhang Q., Zdancewic S. (2010) Relational Parametricity for a Polymorphic Linear Lambda Calculus. In: Ueda K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_24

Here is a simple answer. If we have a lambda-term $$x : \forall t.\,t$$ then we should be able to apply the term $$x$$ to any type $$t$$ and obtain a value of type $$t$$. Denote type application by $$x t$$ and find that $$x t$$ is a value of any given type $$t$$. Let us apply this ability to the void type $$0$$. Then $$x 0$$ is a value of type $$0$$. But there are no values of type $$0$$. So, we could not have had a value $$x$$ either.

Another proof is based on using naturality laws. If you have a pure lambda-term of type $$\forall t.\,t$$ in System F, you can conclude by parametricity theorems that this term satisfies the law of natural transformations of type $$\forall t.\,\underline 1 \to t$$ (where I denote the unit type by $$\underline1$$).

Then you write the naturality law: for an arbitrary function $$f: a\to b$$, a function $$\phi: \forall t.\,\underline1\to t$$ satisfies the equation:

$$f \circ \phi = \phi$$

We can derive from this equation that there can't be any function $$\phi$$. For an $$x: \underline1$$ (there is only one such value $$x$$) we will have some value $$a_1=\phi(x)$$ of type $$a$$ and also some value $$b_1=\phi(x)$$ of type $$b$$. However, the value $$b_1$$ must be at the same time equal to $$f(a_1)$$ for all functions $$f: a\to b$$. This is impossible. So, we conclude that $$\phi$$ cannot exist, and the type $$\forall t.\,t$$ is void.