A Type System for a Lambda Calculus with Assignments

Abstract

We present a Hindley/Milner-style polymorphic type system for var, an extension of the call-by-name -calculus with mutable variables and assignments. To match var`s explicit distinction between functional and imperative worlds, the type universe is stratified into two layers: one for applicative expressions and one for imperative state transformers. In inferring types for var-terms, the type system performs a simple effect analysis to statically verify the safety of coercing a state transformer to a pure value. We prove the soundness of the type system with respect to var`s untyped reduction semantics so that any well-typed program will evaluate to an answer, provided the evaluation terminates. We also discuss some practical aspects of the type system and present a type checker based on the well-known W algorithm.