[TYPES] Question about the polymorphic lambda calculus

[Noam Zeilberger]

On Wed, Jun 04, 2008 at 12:41:52PM -0400, Noam Zeilberger wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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.

Oops, it seems I read too much into the question again.  Samuel did
not state that T has a single occurrence of X, just that X is the
single free type variable.

Noam