AI 中文总结
提出Fresco这一用于一等多态性的新型双向类型推断方法,借助骨架让局部类型信息在函数与参数间双向流动,幽灵代表未知信息,用户可通过冻结定制信息流方向,实现了表达性和可预测性推断并给出相关规范与算法。
AI 中文摘要
双向类型检查利用函数与参数之间的局部信息流。传统双向类型检查仅支持单向信息流,通常是从函数到参数,不足以推断一等多态性。现有改进信息流的工作要么对混合信息流支持有限,要么需要特殊机制损害可预测性。我们提出Fresco,一种用于一等多态性的新型双向类型推断方法。Fresco通过骨架使局部类型信息在函数和参数之间来回流动,幽灵表示未知类型信息,并允许用户通过冻结定制信息流方向。Fresco灵活的信息流实现了一等多态性的表达性和可预测性推断。我们为Fresco提供声明式规范、一个关于声明式系统健全且完备的简单类型推断算法,以及一个将Fresco进一步推广以推断模态效果类型的原型实现。
英文摘要
Bidirectional typing makes use of local information flow between functions and arguments. Conventional bidirectional typing only supports unidirectional information flow, typically from functions to arguments, which is insufficient to infer first-class polymorphism. Existing work on improving information flow either has limited support for mixed information flow or requires ad hoc mechanisms that harm predictability. We propose Fresco, a novel bidirectional type inference approach to first-class polymorphism. Fresco enables local type information to flow back and forth between functions and arguments via skeletons, with ghosts representing unknown type information, and allows users to customise the direction of information flow by freezing. The flexible information flow of Fresco enables expressive and predictable inference for first-class polymorphism. We provide a declarative specification for Fresco, a simple type inference algorithm that is sound and complete with respect to the declarative system, and a prototype implementation that further generalises Fresco to infer modal effect types.