Types and imperative programming

Thus far everything seems to have gone very well but there are problems just ahead when we consider the interaction of references and polymorphism. There is an ordering ``>'' corresponding to ``degree of polymorphism'' such that the following relation holds between the types of polymorphic functions.

Given a reference to a polymorphic function, an assignment could make the type of the function which is referenced less polymorphic as allowed by the ``>'' ordering. However, such behaviour could lead to expressions which can be statically type-checked but which would produce a run-time type error when executed. A short example is given below.

(* rejected due to type-checking *)

let
  val r = ref (fn x => x)
in
  (r := (fn x => x + 1);  !r true)
end;

If the function r was assigned the polymorphic type forall 'a.(('a -> 'a) ref) then the assignment and the dereferenced function application would both be correctly typed but the program would ``go wrong'' at run-time by attempting to add a boolean value to an integer. The type system of Standard ML does not allow programs to go wrong in this way and thus the example must be rejected by a compiler.

NEXT ·  UP ·  PREVIOUS ·  CONTENTS ·  INDEX