3 Jun 12:38 2008

### Question about the polymorphic lambda calculus

```[ 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?

If this is a theorem, could someone please point me to a proof of it?

Sam Moelius

```
3 Jun 17:34 2008

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

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

3 Jun 18:26 2008

### Re: Question about the polymorphic lambda calculus

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

Noam,

> 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?

Yes, that's exactly what I meant.

But your response to the alternative question was interesting and
appreciated, nonetheless.  :)

Sam

```
4 Jun 18:41 2008

### 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 19:28 2008

### Re: Question about the polymorphic lambda calculus

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

On Tue, Jun 3, 2008 at 11:38 AM, Samuel E. Moelius III
<moelius@...> 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?

Maybe I'm missing something, but I would have thought that in general
the answer has to be no: it doesn't follow from the fact that
universal quantification is expressible in the meta-language that it's
expressible in the object-language.

Compare the analogous situation with first-order predicate calculus as
the meta-language for first-order propositional calculus with
countably infinite named constants and a finiteness constraint on
proposition and proof length.

Cheers,

Miles

```
4 Jun 19:37 2008

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

```
5 Jun 14:01 2008

### Re: Question about the polymorphic lambda calculus

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

Miles,

> Maybe I'm missing something, but I would have thought that in general
> the answer has to be no: it doesn't follow from the fact that
> universal quantification is expressible in the meta-language that it's
> expressible in the object-language.

I appreciate your point.  But this case is special in at least two
respects: (1) the quantified statements are all of a certain form (i.e.,
there exists a term with a certain type), and (2) the object language is
the polymorphic lambda calculus, specifically.  For this special case, I
think there is good reason to suspect that the universal quantifier can
be expressed in the object language.

Sam

```
6 Jun 14:58 2008

### Re: Question about the polymorphic lambda calculus

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

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?
>
> If this is a theorem, could someone please point me to a proof of it?
>
>
> Sam Moelius
>
>

Dear Sam,

If I look at your question in the polymorphic lambda calculus (system
F), then it is basically a question about derivability in second order
proposition logic PROP2:
Does the following hold?
If |- Phi(U)  for every closed proposition U, then |- forall X Phi(X)

PROP2 is constructive proposition logic: only implication -> and a
```

10 Jun 15:34 2008

### Fwd: Revenue-neutral Adjustment for Functional Programming

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

This message is slightly off-topic, and apologies for that. I
believe, however, that it is in the spirit of this list.

The ACM Curriculum board has re-opened the 2001 design for review.
Although ACM is a US-based organization, the curriculum is not only
influential at the middle tier of US colleges and universities, it is
also taken seriously by many evolving and developing educational
this list in the late 90s that the curriculum has relegated the study
of PL and type systems to a peripheral status. We may now have an
opening to make a small change.

The ACM Curriculum board has agreed to consider a proposal on
including FP as an equal to OOP (10 "hours" each) in the standard
curriculum. See forwarded message below. This was the most concrete
outcome of the PLC workshop at Harvard two weeks ago. (Stuart Reges,
Shriram Krishnamurthi, and I drafted the proposal; Larry Snyder
volunteered to submit it once the workshop expressed its unanimous
support. The three of us came to the conclusion that only an
inclusion of FP in the general curriculum will prepare students for
properly designed though possibly optional PL courses, including a
thorough study of type systems.)

I think this is a great idea" will be helpful. A short explanation is
even better.

Thanks -- Matthias
```

11 Jun 12:12 2008

### Paper announcement: Intersection types à la Church

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

I'm pleased to announce the available of a new paper on Intersection
Types à la Church:

http://dx.doi.org/10.1016/j.ic.2007.03.005

http://www-sop.inria.fr/members/Luigi.Liquori/PAPERS/ic-07.pdf

As always, comments and suggestions are welcome.

Luigi Liquori and Simona Ronchi Della Rocca.

Intersection-Types à la Church

by

Luigi Liquori
INRIA Sophia Antipolis, France
Simona Ronchi Della Rocca
Dipartimento di Informatica, Università di Torino, Italy

Abstract
In this paper, we present Λt∧, a fully typed λ-calculus based on
the intersection-type system
discipline, which is a counterpart à la Church of the type assignment
system as invented
by Coppo and Dezani. The relationship between Λt∧ and the
intersection type assignment
system is the standard isomorphism between typed and type assignment
```