[Prev][Next][Index][Thread]

F-omega type reconstruction; recursive vs. quantified types



Date: Tue, 14 Jul 92 18:17:25 -0400

       =============================================================
       Announcement Number 1: draft paper available by anonymous ftp
       =============================================================

Title: Type reconstruction in F_omega is undecidable,
Abstract: It is undecidable whether a given pure lambda term can be 
          assigned a type in the system F_omega.

To obtain: ftp to cs.bu.edu with login name: anonymous
                                   password: your e-mail address
           then type: cd urzy
                      get fomega-short.xxx
where xxx is either dvi or ps.

Warning: The paper contains a rough idea of the proof, with most details
         omitted. It is a highly technical proof, and its presentation in
         the draft is by no means complete. But this is what I can make
         available now. I hope to write a full report in the nearest future. 
         Also, I am willing to provide any further explanation on request.
         
     =================================================================
     Announcement Number 2: a remark on quantified vs. recursive types
     =================================================================

Furio Honsell suggested to me that I make this announcement, as it may 
clarify some misunderstandings about the relationships between recursive
types and quantificational polymorphism. Let 2 = \lambda fx.f(fx) and let
K = \lambda yz.y. The term 22K has the following properties:

(1) It is untypable in the second order polymorphic lambda calculus;
(2) It is typable with recursive types, with \mu t.\tau allowed when
    all occurrences of t in \tau are positive.

Property (1) is proved just by a careful analysis of how a type for this 
term could look like, and showing failure for each possibility - nothing
exciting. Property (2) is easy: assign the type \tau = \mu t.s->t to y, 
and assign s to z. Then K has type \tau -> s -> \tau and this equals 
\tau -> \tau, since \tau = s -> \tau. Typing the 2's is simple.

On the other hand simple types + \mu cannot type even \lambda x.xx, thus the 
``typing power'' of \mu is incomparable with that of the universal quantifier.
-------------------------------------------------------------------------------

My permanent e-mail address is urzy@mimuw.edu.pl.