Henning Makholm and J. B. Wells
Type
inference, principal typings, and let-polymorphism for first-class mixin
modules
In Proc. 10th Int'l Conf. Functional Programming, pages
156-167 ACM Press, September 2005
A mixin module is a programming abstraction
that simultaneously generalizes
lambda-abstractions, records, and mutually
recursive definitions. Although various mixin module
type systems have been developed, no one has
investigated principal typings or developed
type inference for first-class mixin modules,
nor has anyone added Milner's
let-polymorphism to such a system.
This paper proves that typability is NP-complete for
the naive approach followed by previous mixin module
type systems. Because a lambda-calculus extended
with record concatenation is a simple
restriction of our mixin module calculus, we also
prove the folk belief that typability is NP-complete
for the naive early type systems for record
concatenation.
To allow feasible type inference, we present
Martini, a new system of simple
types for mixin modules with principal
typings. Martini is conceptually simple,
with no subtyping and a clean and balanced
separation between unification-based type inference
with type and row variables and constraint solving
for safety of linking and field extraction. We have
implemented a type inference algorithm and we prove
its complexity to be O(n2), or O(n) given a
fixed bound on the number of field
labels. (Technically, there is also a factor of
alpha(n), but alpha(n)<= 4 for
n<1010^100 (a “googolplex'').) To prove the
complexity, we need to present an algorithm for
row unification that may have been
implemented by others, but which we could not find
written down anywhere. Because Martini has
principal typings, we successfully extend it with
Milner's let-polymorphism.
[ bib |
.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.
