### Re: Question about the polymorphic lambda calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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?

(Continue reading)