Abstracting gradual typing
Abstracting gradual typing
复制标题
抽象渐进式打字
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
É. Tanter
中科院分区：
文献类型：
--
作者：
Ronald Garcia;Alison M. Clark;É. Tanter
语言研究人员和设计师已经扩展了各种类型的系统来支持逐渐键入，这使语言能够无缝地结合动态和静态检查。这些努力一致地表明，设计与静态类型系统的令人满意的逐渐对应物具有挑战性，而这一挑战只会随着类型系统的复杂性而增加。渐进的系统设计人员需要更多的正式工具来帮助他们概念化，结构和评估其设计。在本文中，我们提出了一个新的正式基础，以逐步键入，利用抽象解释中的原理，从而使渐进类型的语义在预先存在的静态类型方面具有语义。抽象逐渐键入（简称AGT）产生了一致性的正式描述 - 逐渐键入方法的基石之一 - 这是通过直觉和临时推理而开发的现有一致性概念。鉴于语法指导的静态键入判断，AGT方法会引起相应的逐渐键入判断。然后，基础静态学科的类型安全性证明可以诱导通过源语言键入派生定义的渐进程序的动态语义。 AGT方法没有诉诸于外部合理的铸造微积分：相反，通过推论在降低证据期间判断一致判断的证据，自然而然地出现了运行时间检查。为了说明这种方法，我们为具有记录子类型的语言逐渐开发了一种新颖的对应物。用AGT方法设计的渐进语言可以通过构造Siek及其同事制定的逐渐键入的精制标准满足。
Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. In this paper, we propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency---one of the cornerstones of the gradual typing approach---that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the type safety proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not resort to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof reduction. To illustrate the approach, we develop a novel gradually-typed counterpart for a language with record subtyping. Gradual languages designed with the AGT approach satisfy by construction the refined criteria for gradual typing set forth by Siek and colleagues.