A Polymorphic Environment Calculus and its Type-Inference Algorithm
A Polymorphic Environment Calculus and its Type-Inference Algorithm
复制标题
多态环境演算及其类型推断算法
DOI：
10.1023/a:1010010314528
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
S. Nishizaki
中科院分区：
文献类型：
--
作者：
S. Nishizaki
多态环境演算是一个多态的Lambda演算，它使我们能够像对待一等公民一样对待环境。在微积分中，环境被形式化为显式替换，并且替换被包括在微积分的项集合中。首先，我们介绍了一个非类型化的环境演算，并给出了该演算的一种语义，作为对lambda演算的翻译。其次，在Damas-Milner的ML-多态类型系统的基础上，提出了环境演算的多态类型系统。在ML中，多态只允许在let表达式中使用；在多态环境演算中，多态与环境组合一起提供。我们证明了类型系统的一个主题约简定理。第三，给出了多态环境演算的类型推理算法，并建立了它的可靠性、终止性和主型定理。
The polymorphic environment calculus is a polymorphic lambda calculus which enables us to treat environments as first-class citizens. In the calculus, environments are formalized as explicit substitutions, and the substitutions are included in the set of terms of the calculus. First, we introduce an untyped environment calculus, and we present a semantics of the calculus as a translation into the lambda calculus. Second, we propose a polymorphic type system for the environment calculus based on Damas-Milner's ML-polymorphic type system. In ML, polymorphism is allowed only in let-expressions; in the polymorphic environment calculus, polymorphism is provided with environment compositions. We prove a subject-reduction theorem for the type system. Third, a type-inference algorithm is given to the polymorphic environment calculus, and we establish its soundness, termination, and principal-typing theorem.