An error-tolerant type system for variational lambda calculus
An error-tolerant type system for variational lambda calculus
复制标题
变分 lambda 演算的容错类型系统
DOI：
10.1145/2364527.2364535
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Eric Walkingshaw
中科院分区：
文献类型：
--
作者：
Sheng Chen;Martin Erwig;Eric Walkingshaw
条件编译和软件产品线技术使得从单个软件项目生成大量不同的程序成为可能。由于可能的变体数量众多，单独键入这些程序通常是不可能的。我们以前的工作已经解决了这个问题的变分lambda演算（VLC），一个扩展的lambda演算的基本结构，用于引入和组织变化的类型系统。虽然我们的类型推断算法比单独推断每个变体的类型的蛮力策略更有效，但它不太鲁棒，因为如果任何一个变体包含类型错误，则整个变分表达式的类型推断将失败。在这项工作中，我们扩展了我们的类型系统操作VLC表达式包含类型错误。这个扩展直接支持定位病态类型的变量和变分程序的增量开发。它对变分类型的统一也有许多微妙的含义。我们表明，我们的扩展类型系统具有一个主要的类型属性和基本的统一问题是单一的。我们的统一算法计算导致结果类型的部分统一符，这些结果类型（1）包含尽可能少的变量中的错误，（2）是最一般的。最后，我们进行了实证评估，以确定此扩展的开销相比，我们以前的工作，证明了暴力的方法的改进，并探讨各种错误分布的影响的推理过程。
Conditional compilation and software product line technologies make it possible to generate a huge number of different programs from a single software project. Typing each of these programs individually is usually impossible due to the sheer number of possible variants. Our previous work has addressed this problem with a type system for variational lambda calculus (VLC), an extension of lambda calculus with basic constructs for introducing and organizing variation. Although our type inference algorithm is more efficient than the brute-force strategy of inferring the types of each variant individually, it is less robust since type inference will fail for the entire variational expression if any one variant contains a type error. In this work, we extend our type system to operate on VLC expressions containing type errors. This extension directly supports locating ill-typed variants and the incremental development of variational programs. It also has many subtle implications for the unification of variational types. We show that our extended type system possesses a principal typing property and that the underlying unification problem is unitary. Our unification algorithm computes partial unifiers that lead to result types that (1) contain errors in as few variants as possible and (2) are most general. Finally, we perform an empirical evaluation to determine the overhead of this extension compared to our previous work, to demonstrate the improvements over the brute-force approach, and to explore the effects of various error distributions on the inference process.