[TYPES] the polymorphic lambda calculus - A related question concerning its uniformity

Wed Jun 25 16:20:30 EDT 2008

Consider a modification of the typing system for System F so that one deals with ground items only.  Namely, contexts are now lists t1 : A1,..., tn : An with the ti's ground terms and the Ai's ground types, and the typing system consists of the following (some of them infinitary) rules, where I use t,s for ground terms, x for term variables, A,B for ground types, p for arbitrary terms, D for arbitrary types, and X for type variables: 

      . 
------------------------[t:A in Gamma]   
Gamma |-- t : A

Gamma, t : A  |--  p[t/x] : B for all t
--------------------------------------------------[FreeVars(p) included in
 {x}]
Gamma  |--  lam x : A. p : A -> B

Gamma  |--  p[A/X] : D[A/x] for all
 A
---------------------------------------------------[FreeVars(p) and FreeVars(D) included in {X}]
Gamma |-- lam X. p : All X. D

Gamma |-- t : A -> B     Gamma |-- s : A
----------------------------------------------------------
Gamma |-- t s : B 

Gamma |-- t : All X. D
------------------------------------[FreeVars(D) included in {X}]
Gamma |-- t [A] : D[A/X]

It is easy to see that this ground type system is at least as powerful as the original system, in that any ground term typable in the empty context in the original system 
is also typable in the empty context in the above ground system.  Is the converse true? 

Thanks in advance, 
   Andrei 

--- On Wed, 6/11/08, types-list-request at lists.seas.upenn.edu <types-list-request at lists.seas.upenn.edu> wrote:
From: types-list-request at lists.seas.upenn.edu <types-list-request at lists.seas.upenn.edu>
Subject: Types-list Digest, Vol 46, Issue 2
To: types-list at lists.seas.upenn.edu
Date: Wednesday, June 11, 2008, 4:49 PM

Send Types-list mailing list submissions to
	types-list at lists.seas.upenn.edu

To subscribe or unsubscribe via the World Wide Web, visit
	http://lists.seas.upenn.edu/mailman/listinfo/types-list
or, via email, send a message with subject or body 'help' to
	types-list-request at lists.seas.upenn.edu

You can reach the person
 managing the list at
	types-list-owner at lists.seas.upenn.edu

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Types-list digest..."

Today's Topics:

   1. Re:  Question about the polymorphic lambda calculus
      (Noam Zeilberger)
   2. Re:  Question about the
 polymorphic lambda calculus
      (Samuel E. Moelius III)
   3. Re:  Question about the polymorphic lambda calculus
      (Noam Zeilberger)
   4. Re:  Question about the polymorphic lambda calculus (Miles Sabin)
   5. Re:  Question about the polymorphic lambda calculus
      (Noam Zeilberger)
   6. Re:  Question about the polymorphic lambda calculus
      (Samuel E. Moelius III)
   7. Re:  Question about the polymorphic lambda calculus
      (Herman Geuvers)
   8.  Fwd: Revenue-neutral Adjustment for Functional Programming
      (Matthias Felleisen)
   9.  Paper announcement:
 Intersection types ? la Church
      (Luigi Liquori INRIA)

----------------------------------------------------------------------

Message: 1
Date: Tue, 3 Jun 2008 11:34:05 -0400
From: Noam Zeilberger <noam+types at cs.cmu.edu>
Subject: Re: [TYPES] Question about the polymorphic lambda calculus
To:
 "Samuel E. Moelius III" <moelius at cis.udel.edu>
Cc: types-list at lists.seas.upenn.edu
Message-ID: <20080603153403.GA22041 at cs.cmu.edu>
Content-Type: text/plain; charset=us-ascii

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

------------------------------

Message: 2
Date: Tue, 3 Jun 2008 12:26:15 -0400
From: "Samuel E. Moelius III" <moelius at cis.udel.edu>
Subject: Re: [TYPES] Question about the polymorphic lambda calculus
To: Noam Zeilberger
 <noam+types at cs.cmu.edu>
Cc: types-list at lists.seas.upenn.edu
Message-ID: <C98ECF9A-3189-11DD-9A8B-003065EF4660 at cis.udel.edu>
Content-Type: text/plain; charset=US-ASCII; format=flowed

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

------------------------------

Message: 3
Date: Wed, 4 Jun 2008 12:41:52 -0400
From: Noam Zeilberger <noam+types at cs.cmu.edu>
Subject: Re: [TYPES] Question about the polymorphic lambda calculus
To:
 "Samuel E. Moelius III" <moelius at cis.udel.edu>
Cc: types-list at lists.seas.upenn.edu
Message-ID: <20080604164152.GA23990 at cs.cmu.edu>
Content-Type: text/plain; charset=us-ascii

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

Proof: by induction on T.

Do you buy that?  It seems that the statement can be generalized to
when T has multiple occurrences of X, but they are all either positive
or negative.  I am
 curious, though, of whether you know of any
counterexamples when X occurs both positively and negatively in T?

Noam

------------------------------

Message: 4
Date: Wed, 4 Jun 2008 18:28:27 +0100
From: "Miles Sabin"
 <miles at milessabin.com>
Subject: Re: [TYPES] Question about the polymorphic lambda calculus
To: "Samuel E. Moelius III" <moelius at cis.udel.edu>
Cc: types-list at lists.seas.upenn.edu
Message-ID:
	<30961e500806041028w4573c84dyf5ca2390dc38005a at mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1

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

------------------------------

Message: 5
Date: Wed, 4 Jun 2008 13:37:59 -0400
From: Noam Zeilberger <noam+types at cs.cmu.edu>
Subject: Re: [TYPES] Question about the polymorphic lambda calculus
To:
 "Samuel E. Moelius III" <moelius at cis.udel.edu>
Cc: types-list at lists.seas.upenn.edu
Message-ID: <20080604173759.GA24128 at cs.cmu.edu>
Content-Type: text/plain; charset=us-ascii

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

------------------------------

Message: 6
Date: Thu, 05 Jun 2008 08:01:47 -0400
From: "Samuel
 E. Moelius III" <moelius at cis.udel.edu>
Subject: Re: [TYPES] Question about the polymorphic lambda calculus
To: Miles Sabin <miles at milessabin.com>
Cc: types-list at lists.seas.upenn.edu
Message-ID: <4847D5AB.5020308 at cis.udel.edu>
Content-Type: text/plain; charset="ISO-8859-1"; format=flowed

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

------------------------------

Message: 7
Date: Fri, 06 Jun 2008 14:58:31 +0200
From: Herman Geuvers <herman at cs.ru.nl>
Subject: Re: [TYPES] Question about the polymorphic lambda calculus
To: "Samuel E. Moelius III" <moelius at cis.udel.edu>,
	types-list at lists.seas.upenn.edu
Message-ID: <48493477.6090801 at cs.ru.nl>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

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 
second order quantifier over propositions.

Now, in the classical case, your conjecture holds, because then, if |-

Phi(U)  for every closed proposition U, then
|- Phi(top) and |- Phi(bot) and so |- forall X. Phi(X).
(In classical PROP2, let's call it CPROP2, we have an axiom forall X.(X 
\/ ~X); bot is forall X.X and
top is
 forall X. X->X. The definition of the connectives is just the 
usual one from PROP2.)
That |- Phi(top) and |- Phi(bot) imply |- forall X. Phi(X) is because we 
have a complete truth table semantics for CPROP2. I have spelled that 
out in detail in my PhD thesis in 1993.

Now, can we conclude anything from this for PROP2?
Yes, because there is a G"odel not-not translation from CPROP2 to PROP2. 
One can take the one from Coquand-Herbelin (called "A-translation" in

their paper) or the "standard one" in the book of Van Dalen (Logic
and 
Structure):
Coquand-Herbelin:
    X* := X
    (A->B)* := ~~A* -> ~~B*
    (forall X.A)* := forall X. ~~A*
van Dalen:
    X* := ~~X

 (A->B)* := A* -> B*
    (forall X.A)* := forall X. A*
For the first one, we have
    Gamma |-_{CPROP2} phi   <=> ~~(Gamma*) |- _{PROP2} ~~(phi*)
For the second one, we have
    Gamma |-_{CPROP2}
 phi   <=> Gamma* |- _{PROP2} phi*

So if we consider the van Dalen translation, we can derive that for 
formulas of the form Phi(X)*, we have (in PROP2):
       If |- Phi(U)*  for every closed proposition U, then |- forall X. 
Phi(X)*

Proof: If |-_{PROP2} Phi(U)*  for every closed proposition U, then 
|-_{PROP2} Phi(top)*
and |-_{PROP2} Phi(bot)*, so |-_{CPROP2} Phi(top) and |-_{CPROP2} 
Phi(bot), so |-_{CPROP2} forall X. Phi(X),
so |-_{PROP2} forall X. Phi(X)*.

I have no idea to which extent this extends to the general case.

Best Regards

Herman Geuvers

References:
========
My PhD thesis:
J.H. Geuvers, Logics and Type systems

<http://www.cs.ru.nl/%7Eherman/PUBS/Proefschrift.ps.gz>, PhD. Thesis, 
University of Nijmegen, September 1993. 
http://www.cs.ru.nl/~herman/PUBS/Proefschrift.ps.gz

Thierry Coquand, Hugo Herbelin
A-translation and Looping
 Combinators in Pure Type Systems, 1994, 
Journal of Functional Programming

Dirk van Dalen
Logic and Structure (3rd extended ed.). Springer Verlag, Berlin.

------------------------------

Message: 8
Date: Tue, 10 Jun 2008 09:34:43 -0400
From: Matthias Felleisen <matthias at ccs.neu.edu>
Subject: [TYPES] Fwd: Revenue-neutral Adjustment for Functional
	Programming
To: types <types-list at lists.seas.upenn.edu>
Message-ID: <2AB09C8E-B503-4BD9-98D1-22B2591BD234 at ccs.neu.edu>
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed

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

>> Begin forwarded message:
>>
>>> From: Larry Snyder <snyder at CS.WASHINGTON.EDU>
>>> Date: June 9, 2008 6:58:43 PM EDT
>>> To: PL-CURRC-WKSHP-INVITEES at LISTSERV.ACM.ORG
>>> Subject: Revenue-neutral Adjustment for Functional Programming
>>> Reply-To: Larry Snyder <snyder at CS.WASHINGTON.EDU>
>>>
>>> Colleagues:
>>>
>>> The ACM Education
 Board accepted our last minute input for adding 

>>> Functional Programming to the core of the revised CC2001-CS  
>>> curriculum, has posted our proposed changes on it's Web
 site
>>>
>>> http://wiki.acm.org/cs2001/index.php?title=SIGPLAN_Proposal
>>>
>>> and invited comments. Feel free to endorse our "revenue
neutral"  
>>> workshop motion. (I quickly wrote the text in support of this for 

>>> use by the Ed Board, not expecting it to be included in the  
>>> posting; so apologies if I missed points or messed them up.)   
>>> Accordingly, crisp arguments for this change will doubtless be  
>>> helpful. -- LS
>>>
>>
>

------------------------------

Message: 9
Date: Wed, 11 Jun 2008 12:12:38 +0200
From: Luigi Liquori INRIA
 <Luigi.Liquori at sophia.inria.fr>
Subject: [TYPES] Paper announcement: Intersection types ? la Church
To: types at lists.chalmers.se, types-list at lists.seas.upenn.edu
Cc: Luigi Liquori INRIA
 <Luigi.Liquori at sophia.inria.fr>
Message-ID: <52DF8FBA-7F2A-4BD0-8E77-9464FC131EB1 at sophia.inria.fr>
Content-Type: text/plain;	charset=UTF-8;	delsp=yes;	format=flowed

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  
system, and so
the typed language inherits from the untyped system all the good  
properties, like subject
reduction and strong normalization. Moreover both type checking and  
type reconstruction
are decidable.

Key words: Logics and Intersection-Types, ?-calculus ? la Curry and  
? la Church

-- 
  Luigi Liquori, H.d.R., Ph.D.
  INRIA Researcher, Sophia Antipolis M?diterran?e
  LogNet Research Team
  Vox      : +33 4 92 38 71 93
  Fax      : +33 4 92 38 79 71
  Hom    : +33 4 93 67 09 72
  MobFr : +33 6 65 39 51 32
  MobIt   : +39 3 49 16 56 45 1
  SIP      
 : luigi_liquori at voip.wengo.fr
  Url        : www-sop.inria.fr/members/Luigi.Liquori
  Url        : www.inria.fr/recherche/equipes/lognet.en.html
  Email   : Let (*,#)=(.,@) in
 Luigi*Liquori#inria*fr
  Addr    : INRIA, 2004 Route des Lucioles - BP 93
                 FR-06902 Sophia Antipolis, France
?
	Pensez ? la plan?te et n'imprimez ce message que si n?cessaire !
	Earth will kind ask you to print this message only if really needed!
?

------------------------------

_______________________________________________
Types-list mailing list
Types-list at lists.seas.upenn.edu
http://lists.seas.upenn.edu/mailman/listinfo/types-list

End of Types-list Digest, Vol 46, Issue 2
*****************************************