Although sophisticated polymorphic type systems have become a standard part of functional programming languages, such type systems have had little impact on imperative languages. This research is aimed at developing a new type discipline for a class of implicitly-typed imperative programming languages with subtyping, coherent global overloading, and polymorphism. Technical problems include preserving principal-typing and subject-reduction properties with polymorphic references, developing an appropriate notion of coherence, and finding algorithms to decide whether a set of subtyping and overloading constraints is satisfiable. A novel aspect of the work is the implementation of an incremental algorithm for on-line type inference, suitable for use in programming environments where partial definitions may be given and updated. The implementation is a structured editor generated automatically by the Synthesizer Generator from an attribute grammar specification. Incremental type recomputation is implicit in this paradigm.
