Type assignment in programming languages
Type assignment in programming languages
复制标题
编程语言中的类型分配
DOI：
--
复制
发表时间：
1984
期刊：
影响因子：
--
通讯作者：
L. Damas
中科院分区：
文献类型：
--
作者：
L. Damas
这项工作的目的是为编程语言提出和研究一类类似于LCF系统的元语言ML的类型规则，这些规则基于类型推理系统来定义好类型表达式和程序的概念，并基于类型赋值算法来计算可以为这些相同的表达式或程序推断的一个或多个类型。以前关于ML类型学科的理论基础的工作将在这里重新检查和完成。它还在两个方向上进行了扩展，即处理标识符重载，以及处理涉及将存储作为第一类对象引用的语义。对于这里研究的每个理论，我们都给出了类型推理语义可靠性的证明，即类型良好的表达式对正确类型的对象求值，特别是它们不会导致运行时错误，比如试图将整数添加到列表中。还给出了用于计算可为表达式推断的一个或多个类型的算法以及算法的可靠性和完备性的证明，即算法准确地计算可为表达式实际推断的类型。
The purpose of this work is to present and study a family of polymorphic type disciplines for programming languages similar to the type discipline of ML, the metalanguage of the LCF system, which are based on the use of type inference systems to define the notion of well typed expressions and programs and on the use of type assignment algorithms to compute the type or types that can be inferred for those same expressions or programs. Previous work on the theoretical foundations of the ML type discipline is reexamined and completed here. It is also extended in two directions, namely to handle overloading of identifiers and also to cope with a semantics involving references to a store as first class objects. For each of the theories studied here we present proofs of the semantic soundness of type inference, i.e. that well typed expressions evaluate to objects of the correct type and that in particular they do not lead to run-time errors like trying to add an integer to a list. Algorithms for computing the type or types which can be inferred for expressions are also presented together with proofs of the soundness and completeness of the algorithms, i.e. that the algorithms compute exactly the types which can be actually inferred for the expressions.