[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.