J. B. Wells
The essence of principal typings
In Proc. 29th Int'l Coll. Automata, Languages, and
Programming, volume 2380 of LNCS, pages 913-925 Springer-Verlag, 2002
Let S be some type system. A typing in S
for a typable term M is the collection of all of
the information other than M which appears in the
final judgement of a proof derivation showing that
M is typable. For example, suppose there is a
derivation in S ending with the judgement
A|-M:tau meaning that M has
result type tau when assuming the types of free
variables are given by A. Then (A,tau) is a
typing for M.
A principal typing in S for a term M is a
typing for M which somehow represents all other
possible typings in S for M. It is important not
to confuse this notion with the weaker notion of
principal type often mentioned in connection
with the Hindley/Milner type system. Previous
definitions of principal typings for specific type
systems have involved various syntactic operations
on typings such as substitution of types for
type variables, expansion, lifting,
etc.
This paper presents a new general definition of
principal typings which does not depend on the
details of any particular type system. This paper
shows that the new general definition correctly
generalizes previous system-dependent definitions.
This paper explains why the new definition is the
right one. Furthermore, the new definition is used
to prove that certain polymorphic type systems using
for all-quantifiers, namely System F and the
Hindley/Milner system, do not have principal
typings.
[ 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.
