Peter Møller Neergaard and Harry G. Mairson
Types, potency, and
idempotency: Why nonlinearity and amnesia make a type system
work
In Proc. 9th Int'l Conf. Functional Programming ACM Press,
September 2004
(c)ACM, 2004. This is the author's version of the
work. It is posted here by permission of ACM for your personal use. Not for
redistribution. The definitive version was published in ACM SIGPLAN
Notices, Volume 39, Issue 9 (September 2004)
DOI:
http://portal.acm.org/citation.cfm?doid=1016850.1016871
Useful type inference must be faster than normalization.
Otherwise, you could check safety conditions by running the program.
We analyze the relationship between bounds on normalization and type
inference. We show how the success of type inference is
fundamentally related to the amnesia of the type system: the
nonlinearity by which all instances of a variable are
constrained to have the same type.
Recent work on intersection types has advocated their
usefulness for static analysis and modular compilation. We analyze
system I (and some instances of its descendant, system E), an
intersection type system with a type inference algorithm. Because
system I lacks idempotency, each occurrence of a variable
requires a distinct type. Consequently, type inference is
equivalent to normalization in every single case, and time
bounds on type inference and normalization are identical. Similar
relationships hold for other intersection type systems without
idempotency.
The analysis is founded on an investigation of the relationship
between linear logic and intersection types. We show a lockstep
correspondence between normalization and type inference. The latter
shows the promise of intersection types to facilitate static analyses
of varied granularity, but also belies an immense challenge: to add
amnesia to such analysis without losing all of its benefits.
[ bib |
.ps |
.pdf.gz |
.pdf ]
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.
