Type Systems: Coping with Imperativity
We can incorporate the value restriction in our type system by refining the definition of CLOSE so that it does not generalize the free type variables when then rhs of a definition is not a syntactic value.
Let us extend our polymorphic -calculus language to imperative form in the same way that we did for Jam by adding the type constant unit, the unary type constructor ref, the unary operations ref: * ? ref * and !: ref * ? * , and the binary operation ? : ref * ? * ? unit.
The following polymorphic imperative program generates a run-time type error even though it can be statically typed checked using our rules omitting the value restriction.
in { (? x cons(true,null);
In the absence of the value restriction, this program is typable, because x has polymorphic type ref *, enabling each occurrence of x in the let body to be separately typed. Hence the first occurrence of x has type ref bool while the second has type ref int.
The value restriction prevents polymorphic generalization in this case, preserving type soundness.