headers
Samuel E. Moelius III | 3 Jun 2008 12:38
Picon
Favicon

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?

Thanks in advance.

Sam Moelius
Permalink | Reply | 7 comments |
headers
Noam Zeilberger | 3 Jun 2008 17:34
Picon
Favicon

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)

Permalink | Reply | 3 comments |
headers
Samuel E. Moelius III | 3 Jun 2008 18:26
Picon
Favicon

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
Permalink | Reply | 2 comments |
headers
Noam Zeilberger | 4 Jun 2008 18:41
Picon
Favicon

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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Miles Sabin | 4 Jun 2008 19:28
Gravatar

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
Permalink | Reply | 1 comment |
headers
Noam Zeilberger | 4 Jun 2008 19:37
Picon
Favicon

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
Permalink | Reply | 0 comments |
headers
Samuel E. Moelius III | 5 Jun 2008 14:01
Picon
Favicon

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
Permalink | Reply | 0 comments |
headers
Herman Geuvers | 6 Jun 2008 14:58
Picon
Favicon

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?
>
> Thanks in advance.
>
> 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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Matthias Felleisen | 10 Jun 2008 15:34
Favicon

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  
institutions overseas. As you may recall, I alerted the readers of  
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.)

Please consider contributing comments to the web site. A simple "Yes,  
I think this is a great idea" will be helpful. A short explanation is  
even better.

Thanks -- Matthias
(Continue reading)

Permalink | Reply | 0 comments |
headers
Luigi Liquori INRIA | 11 Jun 2008 12:12
Picon
Picon
Favicon

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
(Continue reading)

Permalink | Reply | 0 comments |

Gmane