|
Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Turbak, and J. B.
Wells
Relating typability
and expressibility in finite-rank intersection type systems
In Proc. 1999 Int'l Conf. Functional Programming, pages
90-101 ACM Press, 1999
We investigate finite-rank intersection type
systems, analyzing the complexity of their type
inference problems and their relation to the problem
of recognizing semantically equivalent
terms. Intersection types allow something of type
tau1/\tau2 to be used in some places at
type tau1 and in other places at type
tau2. A finite-rank intersection type
system bounds how deeply the /\ can appear in
type expressions. Such type systems enjoy strong
normalization, subject reduction, and computable
type inference, and they support a pragmatics for
implementing parametric polymorphism. As a
consequence, they provide a conceptually simple and
tractable alternative to the impredicative
polymorphism of System F and its extensions, while
typing many more programs than the Hindley-Milner
type system found in ML and Haskell. While type
inference is computable at every rank, we show that
its complexity grows exponentially as rank
increases. Let K(0,n)=n and
K(t+1,n)=2K(t,n); we prove
that recognizing the pure lambda-terms of size
n that are typable at rank k is complete for
dtime[K(k-1,n)]. We then
consider the problem of deciding whether two
lambda-terms typable at rank k have the same
normal form, generalizing a well-known result of
Statman from simple types to finite-rank
intersection types. We show that the equivalence
problem is
dtime[K(K(k-1,n),2)]-complete.
This relationship between the complexity of
typability and expressiveness is identical in
well-known decidable type systems such as simple
types and Hindley-Milner types, but seems to fail
for System F and its generalizations. The
correspondence gives rise to a conjecture that if
T is a predicative type system where
typability has complexity t(n) and expressiveness
has complexity e(n), then
t(n)=Omega(log*e(n)).
[ bib |
.ps.gz |
.html ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
