MONADIC STATE - AXIOMATIZATION AND TYPE SAFETY

Type safety of imperative programs is an area fraught with difficulty and requiring great care. The SML solution to the problem, originally involving imperative type variables, has been recently simplified to t he syntactic-value restriction. In Haskell, the problem is addressed i n a rather different way using explicit monadic state. We present an o perational semantics for state in Haskell and the first full proof of type safety. We demonstrate that the semantic notion of value provided by the explicit monadic types is able to avoid any problems with gene ralization.