Perhaps we might appear to have made too much of the problem of computing types. It may seem to be just a routine task which can be quickly performed by the Standard ML system. In fact this is not true. Type inference is computationally hard [KTU94] and there can be no algorithm which guarantees to find the type of a value in a time proportional to its ``size''. Types can increase exponentially quickly and their representations soon become textually much longer than an expression which has a value of that type. Fortunately the worst cases do not occur in useable programs. Fritz Henglein states in [Hen93],
... in practice, programs have ``small types'', if they are well typed at all, and Milner-Mycroft type inference for small types is tractable. This, we think, also provides insight into why ML type checking is usable and used in practice despite its theoretical intractability.
Exercise
Compute the type of y o y if y is x o x and x is pair o pair.
Exercise
(This exercise is due to Stuart Anderson.) Work out the type of the function fun app g f = f(f g). What is the type of app app and what is the type of app(app app)?
Exercise
Why can the following function app2 not be typed by the Hindley-Milner type system? [The formal parameter f is intended to be a curried function.]fun app2 f x1 x2 = (f x1) (f x2);