|
Assaf J. Kfoury and J. B. Wells
Principality and type
inference for intersection types using expansion variables
Theoret. Comput. Sci., 311(1-3):1-70, 2004
Supersedes [80]. For omitted proofs, see the
longer report [33]
Principality of typings is the property that for
each typable term, there is a typing from which all
other typings are obtained via some set of
operations. Type inference is the problem of finding
a typing for a given term, if possible. We define an
intersection type system which has principal typings
and types exactly the strongly normalizable
lambda-terms. More interestingly, every
finite-rank restriction of this system (using
Leivant's first notion of rank) has principal
typings and also has decidable type inference. This
is in contrast to System F where the finite rank
restriction for every finite rank at 3 and above has
neither principal typings nor decidable type
inference. Furthermore, the notion of principal typings
for our system involves only one operation,
substitution, rather than several operations (not
all substitution-based) as in earlier presentations
of principality for intersection types (without rank
restrictions). In our system the earlier notion of
expansion is integrated in the form of
expansion variables, which are subject to
substitution as are ordinary variables. A
unification-based type inference algorithm is
presented using a new form of unification,
beta-unification.
[ bib |
.pdf |
.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.
|
