弱包含约束用于类型诊断的增量算法
cmp-lg
2008-02-03 v2 计算与语言
摘要
我们引入了对高阶并发约束语言进行类型检查所需的约束，并用增量算法求解。我们的约束系统通过约束 x⊆y（表示"x 至少具有 y 的结构"）扩展了有理统一，该约束由树之间的弱实例关系建模。这一实例概念经过精心选择，比通常的实例概念更弱，从而使半统一保持可判定。半统一曾多次被用来连接类型推断中产生的统一问题与计算语言学中考虑的问题。正如多态递归通过半统一问题对应于包含，我们的类型约束问题对应于语言学中特征图的弱包含。特征图的 WhatsIt 的可判定性问题已由 Dörre 解决。与 Dörre 的方法不同，我们的算法是完全增量的，不引用有限状态自动机。我们的算法也更加灵活。它允许多种扩展（记录、排序、析取类型、类型声明等），使其适用于完整编程语言的类型推断。
引用
@article{arxiv.cmp-lg/9506002,
title = {Weak subsumption Constraints for Type Diagnosis: An Incremental Algorithm},
author = {Martin Mueller and Joachim Niehren},
journal= {arXiv preprint arXiv:cmp-lg/9506002},
year = {2008}
}
备注
Presented at CLNLP'95. An improved version is available under the name "A Type is a Type is a Type" from the Authors