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 functionfnx =>fny => 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.

funparen n =fng => g n;funparen' n = (fng => g) n;

**Exercise**

What is the type offnx => x (fnx => x)?

Standard ML will compute the type 'a -> 'b for the following function.

funloop 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.