Type safety conditions

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:

1.

to detect all violations of types;

2.

to compile as many programs as possible; and

3.

to provide a type system which is intuitive for programmers.

This last complication is a serious concern. A programming language which infers types should not make the types of functions so complex that a programmer can no longer have reasonable conviction about the type to expect to see reported by the compiler. Why do we consider this to be important? Because the type information computed by the system is excellent diagnostic information which can be used to debug programs without ever executing them. Consider the following function which is intended to dereference a list of references and apply a function to each. This is a version of map for reference values, called rap.

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.

NEXT ·  UP ·  PREVIOUS ·  CONTENTS ·  INDEX