Algebraic reconstruction of types and effects
Algebraic reconstruction of types and effects
复制标题
类型和效应的代数重建
DOI：
--
复制
发表时间：
1991
期刊：
影响因子：
--
通讯作者：
D. Gifford
中科院分区：
文献类型：
--
作者：
P. Jouvelot;D. Gifford
我们提出了第一个算法，用于在多态类型语言中存在第一类过程的情况下重建表达式的类型和效果。效果是表达式动态行为的静态描述。正如类型描述表达式计算什么一样，效果描述表达式如何计算。在存在效应的情况下，类型的重构更加复杂，因为效应的代数对效应和类型都产生了复杂的约束。在本文中，我们展示了如何在存在此类约束的情况下使用一种称为代数重建的新算法进行重建，证明它是合理且完整的，并讨论其实际意义。这项研究得到了 DARPA 根据 ONR 合同 N00014-89-J-1988 的支持。
We present the rst algorithm for reconstructing the types and e ects of expressions in the presence of rst class procedures in a polymorphic typed language. E ects are static descriptions of the dynamic behavior of expressions. Just as a type describes what an expression computes, an effect describes how an expression computes. Types are more complicated to reconstruct in the presence of e ects because the algebra of e ects induces complex constraints on both e ects and types. In this paper we show how to perform reconstruction in the presence of such constraints with a new algorithm called algebraic reconstruction, prove that it is sound and complete, and discuss its practical import. This research was supported by DARPA under ONR Contract N00014-89-J-1988.