Refined Criteria for Gradual Typing
Refined Criteria for Gradual Typing
复制标题
逐步打字的细化标准
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
J. Boyland
中科院分区：
文献类型：
--
作者：
Jeremy G. Siek;Michael M. Vitousek;M. Cimini;J. Boyland
Siek 和 Taha [2006] 创造了“渐进类型”一词来描述一种在单一语言中集成静态和动态类型的理论，该理论 1) 让程序员控制哪些代码区域是静态类型或动态类型，2) 使代码能够在两种类型规则之间逐渐演变。自 2006 年以来，“渐进类型”一词变得相当流行，但其含义已被淡化为包含与静态和动态类型集成相关的任何内容。这种淡化部分是原始论文的错误，原始论文对逐渐打字的含义提供了不完整的形式描述。在本文中，我们在沙子上画了一条清晰的线，其中包括一个新的形式属性，称为渐进保证，它将仅在类型注释方面有所不同的程序的行为联系起来。我们认为渐进保证为渐进类型语言的设计者提供了重要的指导。我们调查了渐进式打字文献，根据渐进式保证对设计进行了批评。我们还报告了渐进式 Lambda 演算的渐进保证成立的机械化证明。
Siek and Taha [2006] coined the term gradual typing to describe a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines. Since 2006, the term gradual typing has become quite popular but its meaning has become diluted to encompass anything related to the integration of static and dynamic typing. This dilution is partly the fault of the original paper, which provided an incomplete formal characterization of what it means to be gradually typed. In this paper we draw a crisp line in the sand that includes a new formal property, named the gradual guarantee, that relates the behavior of programs that differ only with respect to their type annotations. We argue that the gradual guarantee provides important guidance for designers of gradually typed languages. We survey the gradual typing literature, critiquing designs in light of the gradual guarantee. We also report on a mechanized proof that the gradual guarantee holds for the Gradually Typed Lambda Calculus.