统一以函数为优先与以参数为优先的双向类型系统
Unifying Function- and Argument-First Bidirectional Type Systems
浏览论文内容
中文总结 AI 辅助
本文统一了以函数为优先与以参数为优先的双向类型系统，开发了带新型双向类型系统的\ucf00\ucf01\ucf0b及对应算法，经Abella证明器验证其可靠性与完备性。
中文摘要 AI 辅助
双向类型将类型综合与类型检查融合为单一过程。现有双向类型系统可分为两类风格：给定函数应用时，双向类型算法先综合函数的类型，再检查参数是否匹配该综合得到的参数类型，我们称之为「以函数为优先」；或先综合参数的类型，再检查函数是否匹配该综合得到的参数类型，我们称之为「以参数为优先」。这两类风格不仅在类型系统与类型算法的形式化方式上存在显著差异，还会导致不兼容的类型能力，迫使语言设计者选择其中一种风格并放弃另一种的类型能力。本文中，我们统一了这两种风格，并为高阶多态开发了带有新型双向类型系统的\ucf00\ucf01\ucf0b。统一的核心思路有两点：一是为每个函数应用标注少量信息，用于表示采用以函数为优先还是以参数为优先的类型方式，允许语言设计者甚至程序员自行选择切换两种风格；二是借鉴带颜色类型与盒式类型的思路重新构建以函数为优先和以参数为优先的类型系统，这类思路可灵活指定类型中需综合或用于检查的部分。我们还基于Zhao等人的工作列表方法开发了类型算法。\u03bb^{BH}的（声明式）类型系统被证明是可靠的，且涵盖了两类代表性的以函数为优先与以参数为优先的系统；我们的类型算法被证明对\u03bb^{BH}的类型系统可靠，且对两类代表性系统完备。我们使用Abella定理证明器对这些元定理进行了机械证明。
英文摘要
Bidirectional typing mixes type synthesis and type checking into a single process. Existing bidirectional type systems can be classified into two styles based on whether, given a function application, a bidirectional typing algorithm synthesizes the function's type first and typechecks the argument against the synthesized argument type, or it synthesizes the arguments' types first and typechecks the function against the synthesized arguments' types. We call the former _function-first_ and the latter _argument-first_. Not only do the two styles significantly differ in how the type systems and typing algorithms are formalized, but also they lead to incompatible typeabilities, forcing a language designer to select one style and to give up the other's typeabilities. In this paper, we unify the two styles and develop \lang with a new bidirectional type system for higher-rank polymorphism. Key ideas of the unification are twofold. Each function application is annotated with a bit of information to represent whether function- or argument-first typing is used, to allow a language designer (or even a programmer) to switch between the two styles at their discretion. We reformulate the function- and argument-first type systems by using ideas from colored types and boxy types, which can specify which part of a type should be synthesized or used for checking in a flexible manner. We also develop a typing algorithm based on the worklist approach by Zhao et al. The (declarative) type system of $λ^{BH}$ is shown to be sound and to subsume two representative function- and argument-first systems. Our typing algorithm is shown to be sound with respect to the type system of $λ^{BH}$ and complete with respect to representative function- and argument-first systems. We mechanically prove the metatheorems using the Abella theorem prover.
发表机构
- Kyoto University（京都大学）
机构由 AI 辅助整理，请以论文原文为准。
