Implementing type safety

A number of methods of combining polymorphic definition and imperative features were proposed by Mads Tofte [Tof90] and Standard ML adopts the simplest of them. A persuasive argument is provided by Andrew Wright [Wri95] that relatively little expressiveness is lost in making this choice. Tofte's approach divides expressions into the categories of expansive and non-expansive. The essence of the idea is that only non-expansive expressions may be polymorphic.

What is a non-expansive expression? We may characterise it as a value and thus Standard ML is said to have `value polymorphism'. More precisely, a non-expansive expression is

• a constant;
• an identifier;
• a record where the labels are associated with non-expansive expressions;
• an application of any constructor except ref to a non-expansive expression; and
• any fn expression

and anything of this form supplemented with parentheses, type constraints and derived forms. Any other expression is deemed expansive, even if it does not use references.

The following value declarations are not permitted since they contain expansive expressions of polymorphic type.

(* All rejected by the compiler *)

val r = rev [];
val r = ref [];
val r = ref (fn x => x);
val concat = foldr (op @) [];

Notice that the value polymorphism applies even for purely functional programs which make no use of the imperative features of the language. When confronted with a polymorphic expression which is rejected because it contains a free type variable (at the top level) there are several possible solutions. One is to simplify the expression to remove any unneeded function applications--such as replacing rev [] with []--and another solution is to add an explicit type constraint if the desired result is monomorphic. For expressions which denote polymorphic functions the introduction of an explicit fn abstraction solves the problem. For example, concat can be written thus

val concat = fn s => foldr (op @) [] s;

or using the derived form for this which we saw [*].

The following value declarations are legal because their (monomorphic) types can be determined.

let  val r = rev []  in  val s = implode r  end;
let  val x = ref []  in  val s = 1 :: !x  end;

The following imperative version of the rev function (on page [*]) contains only occurrences of expansive expressions within the body of a fn abstraction (recall that the fun keyword is a derived form which includes a fn abstraction). This function reverses lists in linear time and is thus called fastrev.

fun fastrev l =
  let
    val left = ref l and right = ref []
  in
    while not (List.null (!left)) do
       (right := hd (!left) :: !right;
        left := tl (!left));
    !right
  end;

The Standard ML system will compute the type 'a list -> 'a list for this function, just as it did for the functional version of list reversal.

NEXT ·  UP ·  PREVIOUS ·  CONTENTS ·  INDEX