Incremental Polymorphism
Incremental Polymorphism
复制标题
增量多态性
DOI：
10.1007/3540543961_19
复制
发表时间：
1991
影响因子：
2.7
通讯作者：
R. Nikhil
中科院分区：
文献类型：
--
作者：
Shail Aditya;R. Nikhil
Hindley/米尔纳多态类型系统已被许多编程语言采用，因为它提供了Lisp等编程语言的便利，沿着静态类型检查的正确性保证。然而，这些语言的编程环境仍然不如Lisp的灵活。特别是，Lisp中可能的增量式，自顶向下的程序开发风格被排除在外，因为类型推理系统通常被制定为“批处理系统”，必须在使用之前检查定义。这可能需要大部分的程序被重新编译时，一个小的编辑changesperformed.In本文中，我们试图在增量，自上而下的编程灵活性和静态类型检查的明显冲突的目标之间取得平衡。我们提出了一个增量式的输入机制，在这种机制中，顶级短语可以一个接一个地编译，以任何顺序，并重复（由于编辑）。我们表明，增量类型系统是健全的和完整的相对于更传统的“批处理系统”。该系统从Hindley/米尔纳类型系统的固有多态性中获得灵活性，并最大限度地减少簿记和重新编译的开销。我们的系统已经实施，并已被数十个用户使用了两年多。
The Hindley/Milner polymorphic type system has been adopted in many programming languages because it provides the convenience of programming languages like Lisp along with the correctness guarantees that come with static type-checking. However, programming environments for such languages are still not as flexible as those for Lisp. In particular, the style of incremental, top-down program development possible in Lisp is precluded because the type inference system is usually formulated as a “batch system” that must examine definitions before their uses. This may require large parts of the program to be recompiled when a small editing change is performed.In this paper, we attempt to strike a balance between the apparently conflicting goals of incremental, top-down programming flexibility and static type-checking. We present an incremental typing mechanism in which top-level phrases can be compiled one by one, in any order, and repeatedly (due to editing). We show that the incremental type system is sound and complete with respect to the more traditional “batch system”. The system derives flexibility from the inherent polymorphism of the Hindley/Milner type system and minimizes the overhead of book-keeping and recompilation. Our system is implemented and has been in use by dozens of users for more than two years.