Subtyping recursive types
Subtyping recursive types
复制标题
递归类型的子类型化
DOI：
10.1145/99583.99600
复制
发表时间：
1991
影响因子：
0.5
通讯作者：
L. Cardelli
中科院分区：
文献类型：
--
作者：
R. Amadio;L. Cardelli
我们研究子类型和递归类型的相互作用，在一个简单的类型λ演算。这里的两个基本问题是两个（递归）类型是否在子类型关系中，以及一个术语是否有一个类型。为了解决第一个问题，我们涉及到各种类型等价和子类型的定义，这些定义是由一个模型、一个无限树上的排序、一个算法和一组类型规则引起的。我们的规则，算法和树的语义之间的合理性和完整性。我们还证明了健全性和限制形式的完整性模型。为了解决第二个问题，我们表明，每一对类型的子类型关系，我们可以关联一个术语，其外延是唯一确定的强制两种类型之间的映射。此外，我们推导出一个算法，当给定一个术语与隐式的pronuncons，可以推断其最小的类型只要有可能。
We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, we relate various definitions of type equivalence and subtyping that are induced by a model, an ordering on infinite trees, an algorithm, and a set of type rules. We show soundness and completeness among the rules, the algorithm, and the tree semantics. We also prove soundness and a restricted form of completeness for the model. To address the second question, we show that to every pair of types in the subtype relation we can associate a term whose denotation is the uniquely determined coercion map between the two types. Moreover, we derive an algorithm that, when given a term with implicit coercions, can infer its least type whenever possible.