[Prev][Next][Index][Thread]
Two papers on "local type inference"
The following papers are available electronically through:
http://www.cs.indiana.edu/hyplan/papers/lti.ps.gz
http://www.cs.indiana.edu/hyplan/papers/lti-fsub.ps.gz
Enjoy,
Benjamin Pierce
------------------------------------------------------------------------
LOCAL TYPE INFERENCE
Benjamin C. Pierce
Indiana University
David N. Turner
An Teallach Limited
IU CSCI Technical Report #493
We study two partial type inference methods for a language combining
subtyping and impredicative polymorphism. Both methods are LOCAL in
the sense that missing annotations are recovered using only
information from adjacent nodes in the syntax tree, without
long-distance constraints such as unification variables. One method
infers type arguments in polymorphic applications using a local
constraint solver. The other infers annotations on bound variables in
function abstractions by propagating type constraints downward from
enclosing application nodes. We motivate our design choices by a
statistical analysis of the uses of type inference in a sizable body
of existing ML code.
------------------------------------------------------------------------
LOCAL TYPE ARGUMENT SYNTHESIS
WITH BOUNDED QUANTIFICATION
Benjamin C. Pierce
Indiana University
David N. Turner
An Teallach Limited
IU CSCI Technical Report #495
In the above paper, we introduced a LOCAL TYPE ARGUMENT SYNTHESIS
method for inferring type arguments in polymorphic applications using
a local constraint solver. This method handled both impredicative
polymorphism and subtyping, but (for simplicity of the exposition) did
not treat BOUNDED QUANTIFICATION, where subtyping and quantification
interact via upper bounds on type variables.
We show here how our local type argument technique can be extended to
Cardelli and Wegner's Kernel Fun variant of Fsub.