[TYPES] The "omega rule" in polymorphic lambda calculus

[Andrew Polonsky]

Hi all,

The following question was posed by Samuel E. Moelius III to the TYPES list
on Jun 3, 2008. [1]

> Suppose that T is a type with exactly one free variable X. Further
> suppose that for every closed type U, there is some term with type
> T[U/X]. Then, does there necessarily exist some term with type (forall
> X. T)?

The question was not fully answered at the time, but it occurs to me that a
remark by Herman Geuvers later in the thread [2] leads to a simple
counterexample.

Bot  = forall X. X
 ~A  = A -> Bot
A \/ B = forall X. (A -> X) -> (B -> X) -> X
 EM  = forall X. X \/ ~X

Put T(X) = (EM -> X) \/ (EM -> ~X)

Let A be a closed type.
Then classically, A is either equivalent to Bot or to Top = Bot -> Bot.
In either case, T(A) is provable by the appropriate injection.

However, this choice cannot be made without having EM in the context
already.
Therefore, the type (forall X. T(X)) is not inhabited.

More precisely, any normal closed inhabitant of the above type would have
the form
/\X /\Y \f : (EM -> X) -> Y \g : (EM -> ~X) -> Y). t
where t=t(X,Y,f,g) : Y.

In turn, the term t would have to begin with an application of either f or
g.  Either choice is refuted by an appropriate instance of X.

Cheers,
Andrew
[1] https://lists.seas.upenn.edu/pipermail/types-list/2008/001240.html 
[2] https://lists.seas.upenn.edu/pipermail/types-list/2008/001247.html