Higher-Order and Symbolic Computation, 13(3)239-278
A Polymorphic Environment Calculus and its Type-Inference AlgorithmShin-Ya Nishizaki, Department of Computer Science, Graduate School of Information Science and Engineering, Tokyo Institute of Technology, 2-12-1, O-okayama, Meguro-ku, Tokyo, 152-8552, Japan
|
Abstract: 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.
Keywords: environment calculus, first-class environments, polymorphism, principal-typing theorem, type-inference algorithm, explicit substitutions, lambda calculus |
This article can be downloaded [here].