4 Jun 2008 18:41

## 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 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
```

4 Jun 2008 19:37

### Re: Question about the polymorphic lambda calculus

```[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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

```

Gmane