We desire a type system which permits secure, type-safe, implementation of imperative routines without simply imposing the unnecessarily harsh restriction that the programmer may only make references to monomorphic values. Such a restriction would mean that the previous ordered set and lazy expression examples would not be allowable. The problem of designing a permissive type system for imperative programming has proved to be one of the most difficult in the history of programming language design. The essential tension comes from several conflicting desires:
fun rap f  =  | rap f (h::t) = f !h :: rap f t;
We would expect the compiler to calculate the type ('a -> 'b) -> (('a ref list) -> ('b list)) for the rap function. Instead the type calculated is (('a ref -> 'a) -> 'b -> 'c) -> 'b list -> 'c list. This type is obtained because ! is a function and its application does not bind more tightly than the application of the function f. Function application associates to the left in Standard ML and so the subexpression f !h denotes (f !) h rather than f (!h) as intended. It is difficult to see how this error could have been made more evident to the programmer than by the calculation of the very unusual type for the function.