A Type System for a Lambda Calculus with Assignment

Kung Chen and Martin Odersky

Theoretical Aspects of Computer Science, Sendai, Japan
April 1994


We present a Hindley/Milner-style polymorphic type system for
$\lamvar$, an extension of the call-by-name $\lambda$-calculus with
mutable variables and assignments.  To match $\lamvar$'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 $\lamvar$-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 $\lamvar$'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.