A co-contextual formulation of type rules and its application to incremental type checking
A co-contextual formulation of type rules and its application to incremental type checking
复制标题
类型规则的上下文表述及其在增量类型检查中的应用
DOI：
10.1145/2814270.2814277
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
M. Mezini
中科院分区：
文献类型：
--
作者：
Sebastian Erdweg;Oliver Bračevac;Edlira Kuci;Matthias Krebs;M. Mezini
类型规则将类型与给定类型上下文的表达式关联起来。当类型检查器自顶向下遍历表达式树时，它会使用可用的附加上下文信息扩展类型上下文。这样，类型上下文在其他独立的子表达式中协调类型检查，从而抑制了类型检查的并行化和增量化。我们提出了一种类型规则的共上下文公式，它只接受一个表达式作为输入，并产生一个类型和一组上下文需求。协同上下文类型检查器自下而上地遍历表达式树，并合并独立检查的子表达式的上下文需求。我们描述了一种从常规的基于上下文的公式系统地构建类型规则的共上下文公式的方法，并展示了共上下文类型规则如何产生增量类型检查。使用我们的方法，我们为PCF和引入记录、参数多态性和子类型的扩展派生增量类型检查器。我们的性能评估表明，协同上下文类型检查的性能与标准的基于上下文的类型检查相当，并且增量化可以显著提高性能。
Type rules associate types to expressions given a typing context. As the type checker traverses the expression tree top-down, it extends the typing context with additional context information that becomes available. This way, the typing context coordinates type checking in otherwise independent subexpressions, which inhibits parallelization and incrementalization of type checking. We propose a co-contextual formulation of type rules that only take an expression as input and produce a type and a set of context requirements. Co-contextual type checkers traverse an expression tree bottom-up and merge context requirements of independently checked subexpressions. We describe a method for systematically constructing a co-contextual formulation of type rules from a regular context-based formulation and we show how co-contextual type rules give rise to incremental type checking. Using our method, we derive incremental type checkers for PCF and for extensions that introduce records, parametric polymorphism, and subtyping. Our performance evaluation shows that co-contextual type checking has performance comparable to standard context-based type checking, and incrementalization can improve performance significantly.