Type Systems: Coping with Imperativity
If replicating the let definition
(renaming the defined variable x) for each use of x in M does not preserve the meaning of programs, then programs written using Milner style polymorphism may not be type correct. In an imperative language, this phenomenon can happen in several ways. First, the evaluation of M may have side effects. Second, the value of x may allocate mutable storage which is shared (a subtle form of side effect) when
is a single definition but split (among the various type instantions) when the definition is replicated. In an imperative language this splitting can be detected by mutating allocated storage.
To avoid this problem, we can restrict M to a form that guarantees replication does not change the meaning of programs. This restricted form prevents M from performing side-effects and from allocating shared mutable storage.
If we restrict M to a syntactic value (a constant, variable, or ?-expression) then no side effect or sharing of mutable storage can occur. The most modern languages that use Hindley-Milner polymorphism use this restriction. Standard ML uses a much more complicated and less useful restriction (that is incomparable to the syntactic value test).