How ML Deduces Types?

(Adapted from Ullman, Elements of ML Programming, and prepared by Lin Chi Wing)

ML is quite good at discovering the types of variables, the types of function parameters, and the types of values returned by functions. The subject of how ML does so is quite complex, but there are a few observations we can make that will cover most of the ways types are discovered. Knowing what ML can do helps us know when we must declare a type and when we can skip type declarations.

1. The types of the operands and result of arithmetic operators must all agree. For example, in the expression (a+b)*2.0, we see that the right operand of the * is a real constant, so the left operands are real. If the use of + produces a real, then both of its operands are real. Thus, a and b are real. They will also have a real value any other place they are used, which can help make further type inferences.

2. When we apply an arithmetic comparison, we can be sure the operands are of the same type, although the result is a Boolean and therefore not necessarily of the same type as the operands. For example, in the expression a<=10, we can deduce that a is an integer.

3. In a conditional expression, the expression itself and the sub-expressions follow the then and else must be of the same type.

4. If a variable or expression used as an argument of the function is of a known type. Similarly, if the function parameter is of known type, then the variable or expression used as the corresponding argument must be of the same type.

5. If the expression defining the function is of a certain type, then the function returns a value of that type.

A Concrete Example:

Consider the following function comb(n,m), which is used to compute the value of nCm, that is, the number of choices that one has in selecting m different items from a total of n items:

(1)	fun comb(n,m) = (* assumes 0<= m <= n *)
(2)		if m=0 orelse m=n then 1
(3)             else comb(n-1,m) + comb(n-1,m-1);

                val comb = fn : int * int -> int

In line (2), we see that in the base case the result returned by the function is the integer 1. Thus, in all cases the function returns an integer. In line (3) we see that the expression n-1 and m-1 are computed. Since one operand of each subtraction is the integer 1, the other operands, n in one case and m in the other, must also be integers. Thus, both arguments of the function are integers, or strictly speaking, the (one) argument of the function is of type int * int, that is, a pair of integers.

Another way we could have discovered that m and n are integers is to look at line (2). We see that m is compared with integer 0, so m must be an integer. We also see n is compared with m, and since we already know m is an integer, we know the same about n.