On-Line Polymorphic Type Inference in Imperative Languages

尽管复杂的多态类型系统已经成为函数式编程语言的标准部分，但这种类型系统对命令式语言的影响很小。本研究旨在为一类具有子类型、连贯全局重载和多态性的隐式类型命令式编程语言发展一种新的类型学科。技术问题包括使用多态引用保留主体类型和主题约简属性，开发适当的一致性概念，以及找到确定一组子类型和重载约束是否可满足的算法。这项工作的一个新颖方面是在线类型推断的增量算法的实现，适合在可以给出和更新部分定义的编程环境中使用。该实现是一个结构化编辑器，由Synthesizer Generator根据属性语法规范自动生成。增量型重计算隐含在这个范例中。

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.