Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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.