|
Peter Møller Neergaard and Harry G. Mairson
Rank bounded intersection: Types, potency, and
idempotency
This paper is obsolete and has been replaced with
[15], 2003
Intersection type systems realize a finite
polymorphism where different types for a term are
itemized explicitly. We analyze System I,
a rank-bounded intersection type system where
intersection is not associative, commutative,
or idempotent (ACI), but includes a
substitution mechanism employing expansion
variables that facilitates modular program
composition and flow analysis. This type system is
used in a prototype intersection type compiler for
the Church project. We prove that the problem of
type inference is exactly as hard as the problem of
normalization: the worst-case cost of both is an
elementary function, where the iterated exponential
depends on the rank. The key to these results is
that simply-typed terms must be linear without ACI,
but have the usual nonelementary power with
ACI. Further, type inference is always
synonymous with normalization: the cost of computing
the principal typing of any term is exactly the cost
of computing its normal form. These results do not
hold when AC, and particularly I, is added.
[ bib ]
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.
|
