In order to exploit the principle that “expressions are freely composed as far as they are type consistent”, primitive functions used to compose expressions should accept expressions of various types. The primitive :: to construct a list has the following type.

# op ::;
val it = fn : [’a. ’a * ’a list -> ’a list]

op prefix convert infix binary operator into a function that takes a pair. This typing indicates that :: is a function that takes a value of type ’a and a value of type ’a list, which is a list type whose element type is ’a, and returns a list of the same type. In this typing, ’a represents an arbitrary type. The notation [’a.$\mathrm{\cdots }$] indicates that ’a in $\mathrm{\cdots }$ can be replaced with any type, and corresponds to universally quantified formula $\forall a.\mathrm{\cdots }$ in logic. These types that quantifies over type variables are called polymorphic types, and functions having a polymorphic type are called polymorphic functions.

Functions defined by composing polymorphic functions are often polymorphic functions.

# fun cons e L = e :: L;
val cons = fn : [’a. ’a -> ’a list -> ’a list]

In this way, ML compiler infers a most general polymorphic type for an expression. To understand this mechanism, consider the following function.

fun twice f x = f (f x);

twice takes a function and an argument and apply the function to the argument twice. Since f is applied to x, the type of x must be the same as the argument type of f. Moreover, since f is applied again to the result of f, the result type of f must be the same as its argument type. The most general type satisfying these constraint is the following.

[’a. (’a -> ’a) -> ’a -> ’a]

ML indeed infers the following typing for twice.

# fun twice f x = f (f x);
val twice = fn : [’a. (’a -> ’a) -> ’a -> ’a]

ML’s principle in program construction – “expressions are composed as far as they are type consistent” – is made possible by this polymorphic type inference mechanism. twice can be combined with any function and a value as far as the function return the same type as its argument and that the value has the argument type of the function. This freedom and constraint is automatically guaranteed by the inferred typing of twice.