A Semantics for Static Type Inference
A Semantics for Static Type Inference
复制标题
静态类型推断的语义
DOI：
10.1006/inco.1994.1018
复制
发表时间：
1994
影响因子：
1
通讯作者：
G. Plotkin
中科院分区：
文献类型：
--
作者：
G. Plotkin
摘要Curry的F演绎系统是ML等程序设计语言静态类型推理算法的基础。如果将自然的“通过转换保存类型”规则添加到Curry的系统中，它将变得无法确定，但相对于各种模型类是完整的。我们证明了库里系统本身的完备性，相对于一个扩展的模型概念，它验证了约简，但不验证了转换。给出了两种证明：一种是使用术语模型，另一种是由类型表达式建立的模型。还考虑了对具有多态或交集类型的系统的扩展。
Abstract Curry′s system for F-deducibility is the basis for static type inference algorithms for programming languages such as ML. If a natural "preservation of types by conversion" rule is added to Curry′s system, it becomes undecidable, but complete relative to a variety of model classes. We show completeness for Curry′s system itself, relative to an extended notion of model that validates reduction but not conversion. Two proofs are given: one uses a term model and the other a model built from type expressions. Extensions to systems with polymorphic or intersection types are also considered.