一句话：提出适用于多态子类型的一致子类型推广定义，并构建支持隐式高阶多态的渐进类型演算。
一致子类型用于渐进类型系统验证类型转换，但 Siek 与 Taha 的原始定义不足以处理多态子类型。本文提出一致子类型的推广定义，使之适用于多态子类型并包含原始定义，为先前的高阶渐进类型系统提供新见解。作者设计了一个支持隐式（高阶）多态的渐进类型演算，给出声明式与双向算法式版本，算法版采用 Dunfield 与 Krishnaswami 的技术处理实例化。文章证明该演算满足渐进类型精化准则的全部静态方面，并研究带静态与渐进类型参数的扩展，以支持某种动态准则；在一致性猜想下将动态渐进保证归约到 λB 的开放问题。除部分算法系统与扩展的手工证明外，元理论均在 Coq 中机器化验证。
Consistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek and Taha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types à la System F also induce a subtyping relation that relates polymorphic types to their instantiations. However, Siek and Taha’s definition is not adequate for polymorphic subtyping. The first goal of this article is to propose a generalization of consistent subtyping that is adequate for polymorphic subtyping and subsumes the original definition by Siek and Taha. The new definition of consistent subtyping provides novel insights with respect to previous polymorphic gradual type systems, which did not employ consistent subtyping. The second goal of this article is to present a gradually typed calculus for implicit (higher-rank) polymorphism that uses our new notion of consistent subtyping. We develop both declarative and (bidirectional) algorithmic versions for the type system. The algorithmic version employs techniques developed by Dunfield and Krishnaswami for higher-rank polymorphism to deal with instantiation. We prove that the new calculus satisfies all static aspects of the refined criteria for gradual typing. We also study an extension of the type system with static and gradual type parameters, in an attempt to support a variant of the dynamic criterion for gradual typing. Assuming a coherence conjecture for the extended calculus, we show that the dynamic gradual guarantee of our source language can be reduced to that of λ B, which, at the time of writing, is still an open question. Most of the metatheory of this article, except some manual proofs for the algorithmic type system and extensions, has been mechanically formalized using the Coq proof assistant.
DOI 原文 ·
@article{paperbot696,
title = {Consistent Subtyping for All},
author = {Ningning Xie and Xuan Bi and Bruno C. D. S. Oliveira and Tom Schrijvers},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {42},
number = {1},
year = {2019},
doi = {10.1145/3310339}
}