Many functions which we have defined do not need to know the type of their arguments in order to produce meaningful results. Such functions are thought of as having many forms and are thus said to be polymorphic. Perhaps the simplest example of a polymorphic function is the identity function, id, defined by fun id x = x. Whatever the type of the argument to this function, the result will obviously be of the same type; it is a homogeneous function. All that remains is to assign it a homogeneous function type such as X -> X. But what if the type X had previously been defined by the programmer? The clash of names would be at best quite confusing. We shall give the id function the type 'a -> 'a and prohibit the programmer from defining types called 'a, 'b, 'c and so on.
Exercise
Define a different function with type 'a -> 'a.
The pairing function, pair, is defined by fun pair x = (x, x). This function returns a type which is different from the type of its argument but still does not need to know whether the type of the argument is int or bool or a record or a function. The type is of course 'a -> ('a * 'a). Given a pair it may be useful to project out either the left-hand or the right-hand element. We can define the functions fst and snd for this purpose thus: fun fst (x, _) = x and fun snd (_, y) = y. The functions have types ('a * 'b) -> 'a and ('a * 'b) -> 'b respectively.
Exercise
The function fn x => fn y => x has type 'a -> ('b -> 'a). Without giving an explicit type constraint, define a function with type 'a -> ('a -> 'a).
Notice that parentheses cannot be ignored when computing types. The function paren below has type 'a -> (('a -> 'b) -> 'b) whereas the function paren' has type 'a -> 'a.
fun paren n = fn g => g n; fun paren' n = (fn g => g) n;
Exercise
What is the type of fn x => x (fn x => x)?
Standard ML will compute the type 'a -> 'b for the following function.
fun loop x = loop x;
The type 'a -> 'b is the most general type for any polymorphic function. In contrasting this with 'a -> 'a, the type of the polymorphic identity function, it is simple to realise that nothing could be determined about the result type of the function. This is because no application of this function will ever return a result.
In assigning this type to the function, the Standard ML type system is indicating that the execution of the loop function will not terminate since there are no interesting functions of type 'a -> 'b. Detecting (some) non-terminating functions is an extremely useful service for a programming language to provide.
Of course, the fact that an uncommon type has been inferred will only be a useful error detection tool if the type which was expected is known beforehand. For this reason, it is usually very good practice to compute by hand the type of the function which was written then allow Standard ML to compute the type and then compare the two types for any discrepancy. Some authors (e.g. Myers, Clack and Poon in [MCP93]) recommend embedding the type information in the program once it has been calculated, either by hand or by the Standard ML system, but this policy means that the program text can become rather cluttered with type information which obscures the intent of the program. However, in some implementations of the language the policy of providing the types for the compiler to check rather than requiring the compiler to infer the types may shorten the compilation time of the program. This might be a worthwhile saving for large programs.