[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.