[TYPES] Question about the polymorphic lambda calculus

[Noam Zeilberger]

On Tue, Jun 03, 2008 at 12:26:15PM -0400, Samuel E. Moelius III wrote:
> >Question 1
> >  Suppose that T is a type with exactly one free variable X.  Further
> >  suppose that for every closed type U, the type T[U/X] is inhabited.
> >  Then is the type (forall X.T) inhabited?
> 
> Yes, that's exactly what I meant.

Aha, sorry I assumed otherwise.  I think the answer to Q1 is yes.
Examine the single occurrence of X in T.  Is it positive or negative?
(Definition: X occurs positively in X; X occurs positively (neg.) in
A->B if it occurs pos. (neg.) in B or neg. (pos.) in A.)  Then define
an instance T' of T as follows:

        T[bot/X]                X occurs positively
  T' = 
        T[top/X]                X occurs negatively

where top = forall Y.Y->Y and bot = forall Y.Y

By assumption, T' is inhabited.  From this it follows that T (and hence
forall X.T) is inhabited, by the following pair of lemmas:

Lemmas
 1. If X occurs only positively in T, then [bot/X]T |- T, and if
 negatively then T |- [bot/X]T
 2. If X occurs only positively in T, then T |- [top/X]T, and if
 negatively then [top/X]T |- T

Proof: by induction on T.

Do you buy that?  It seems that the statement can be generalized to
when T has multiple occurrences of X, but they are all either positive
or negative.  I am curious, though, of whether you know of any
counterexamples when X occurs both positively and negatively in T?

Noam