A Gradual Interpretation of Union Types
A Gradual Interpretation of Union Types
复制标题
Union类型的逐步解读
DOI：
10.1007/978-3-319-66706-5_19
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
É. Tanter
中科院分区：
文献类型：
--
作者：
Matías Toro;É. Tanter
工会类型允许捕获一个术语的可能性，可能是几种可能无关类型的类型。联合类型的传统静态方法没有标记和标记的工会，它们在使用中具有双重优势。受到最新的使用抽象解释来了解逐渐键入的工作的启发，我们为工会类型提供了一种新颖的设计，称为渐进联合类型。逐渐的联合类型结合了带有动态检查支持的标记和未标记联合类型的优点。渐进的联合类型被视为逐渐打字的学科，是限制的不精确类型，表示有限数量的静态类型。我们应用了Garcia等人的抽象渐进分型（AGT）方法。得出一种支持渐进工会和传统，完全不知名的语言的语言的静态和动态语义。我们发现，逐渐的工会与未知类型相互作用，以一种要求分层的AGT方法的方式，依靠两个不同的抽象解释的组成来保留最佳性。得益于抽象的解释框架，由此产生的语言是安全的，并且满足了渐进语言的精致标准。我们还展示了如何将这种语言编译到三人组的演员表，并证明汇编保留了该语言的语义和属性。
Union types allow to capture the possibility of a term to be of several possibly unrelated types. Traditional static approaches to union types are untagged and tagged unions, which present dual advantages in their use. Inspired by recent work on using abstract interpretation to understand gradual typing, we present a novel design for union types, called gradual union types. Gradual union types combine the advantages of tagged and untagged union types, backed by dynamic checks. Seen as a gradual typing discipline, gradual union types are restricted imprecise types that denote a finite number of static types. We apply the Abstracting Gradual Typing (AGT) methodology of Garcia et al. to derive the static and dynamic semantics of a language that supports both gradual unions and the traditional, totally-unknown type. We uncover that gradual unions interact with the unknown type in a way that mandates a stratified approach to AGT, relying on a composition of two distinct abstract interpretations in order to retain optimality. Thanks to the abstract interpretation framework, the resulting language is type safe and satisfies the refined criteria for gradual languages. We also show how to compile such a language to a threesome cast calculus, and prove that the compilation preserves the semantics and properties of the language.