6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ To start with, do you understand intuitively why there should be no term with that type? $\endgroup$ – Aaron Rotenberg Jan 20 at 16:16
  • $\begingroup$ Kind of, basically it would mean that if such a term existed then the term would belong to all possible types. $\endgroup$ – Apoorv Ingle Jan 20 at 16:25
  • 3
    $\begingroup$ 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.) $\endgroup$ – Aaron Rotenberg Jan 20 at 16:36
4
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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 [[โˆ€๐›ผ.๐ต]]๐›พ :=[[๐ต]](๐—๐—‹๐—Ž๐–พ,๐›พ)โˆง[[๐ต]](๐–ฟ๐–บ๐—…๐—Œ๐–พ,๐›พ) $\endgroup$ – Apoorv Ingle Jan 21 at 15:07
  • $\begingroup$ @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). $\endgroup$ – András Kovács Jan 21 at 15:34
  • 1
    $\begingroup$ 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. $\endgroup$ – András Kovács Jan 21 at 15:39
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking โ€œPost Your Answerโ€, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.