[TYPES] Question about the polymorphic lambda calculus

[Noam Zeilberger]

On Tue, Jun 03, 2008 at 06:38:13AM -0400, Samuel E. Moelius III wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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)?
>
> In other words, in the situation described above, can the meta-level 
> ``forall'' be pushed down into the types?

I'm not sure these two questions are the same.  As stated, I'm
reading the first question as:

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?

But perhaps you mean something like so, which could more naturally
be considered "pushing down the meta-level forall":

Question 2
  Suppose that T is a type with exactly one free variable X.  Further
  suppose that for every closed type U, there is some term t_U with type
  T[U/X].  Then does there exist some term t with type (forall X. T), 
  such that for all U, the terms t(U) and t_U are observationally
  equivalent?

The answer to Q2 is no, in general.  For a counterexample, suppose we
have sum types T1+T2.  If these aren't primitive, we can Church encode
them (T1+T2 = forall Y.(T1->Y)->(T2->Y)->Y).  Let T = 1+X, and define
the term t_U of type 1+U as follows:

         inr(t')        if there exists some t' : U
  t_U = 
         inl()          if U is uninhabited

Now, there is only one inhabitant of the type (forall X.1+X), the
term t = [X].inl().  But for inhabited types U, t(U) is not
equivalent to t_U.

If you drop the restriction that X appears exactly once in T, you
can come up with even simpler counterexamples.  For example,
with T = bool (again, you can Church encode the booleans), take

         true           if U = bool
  t*_U =
         false          otherwise

In fact, the restriction doesn't make a difference, because you can
weaken T to X->bool and define t*_U appropriately as \x.true or
\x.false.

Is Q2 what you meant, or did you really mean Q1?

Noam