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.
|forall 'a. forall 'b. ('a -> 'b) > forall 'a. ('a -> 'a) > forall ( ). (int -> int)|
(* 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.