The Standard ML type discipline will reject certain attempts at function definitions. Sometimes these are obviously meaningless but there are complications. Mads Tofte writes in [Tof88]:
At first it seems a wonderful idea that a type checker can find programming mistakes even before the program is executed. The catch is, of course, that the typing rules have to be simple enough that we humans can understand them and make the computers enforce them. Hence we will always be able to come up with examples of programs that are perfectly sensible and yet illegal according to the typing rules. Some will be quick to say that far from having been offered a type discipline they have been lumbered with a type bureaucracy.It is Mads Tofte's view that rejecting some sensible programs which would never go wrong is inevitable but not everyone is so willing to accept a loss such as this. Stefan Kahrs in [Kah96] discusses the notion of completeness--programs which never go wrong can be type-checked--which complements Milner's notion of soundness--type-checked programs never go wrong [Mil78].
We will now consider some programs which the type discipline of Standard ML will reject. We have already noted above that the function (fn g => (g 3, g true)) is not legal.
We saw earlier [*] that it was not possible to define certain kinds of self-applying functions in Standard ML. Other pathological functions also cannot be defined in Standard ML. Consider the ``absorb'' function.
fun absorb x = absorb;
This function is attempting to return itself as its own result. The underlying idea is that the absorb function will greedily gobble up any arguments which are supplied. The arguments may be of any type and there may be any number of them. Consider the following evaluation of an application of absorb.
| absorb true 1 "abc" | = | (((absorb true) 1) "abc") |
| = | ((absorb 1) "abc") | |
| = | (absorb "abc") | |
| = | absorb |
The absorb function cannot be given a type, because there is no type which we could give to it. However, absorb has a near-relative--create, shown below--which could be given type 'a -> 'b in some type systems, but will be rejected by Standard ML.
fun create x = create x x;
As with absorb, there seems to be no practical use to which we could put this function. Once again consider an application.
| create 6 | = | (create 6) 6 |
| = | ((create 6) 6) 6 | |
| = | (((create 6) 6) 6) 6 | |
| = | ... |