fun member (x, []) = false | member (x, h::t) = x = h orelse member (x, t);
We might like this function to have type 'a * 'a list -> bool but it does not. This cannot be a fully polymorphic function since we make an assumption about the values and lists to which it can be applied: we assume that equality is defined upon them. Our experience of the Standard ML language so far would lead us to conclude that this matter would be settled by the default overloading rule which would assign to this function the type int * int list -> bool. This reasoning, although plausible, is flawed.
The equality operator has a distinguished status in Standard ML. It is not an overloaded operator, it is a qualified polymorphic function. The reason that we make this distinction is that where possible equality is made available on new types which we define. This does not happen with overloaded operators because overloaded functions are those which select a different algorithm to apply depending on the type of values which they are given and it is not possible for the Standard ML language to `guess' how we wish to have overloaded operators extended to our new types.
The Standard ML terminology is that a type either admits equality or it does not. Those which do are equality types. When equality type variables are printed by the Standard ML system they are printed with two leading primes and so the type of the member function is displayed as ''a * ''a list -> bool. Types which do not admit equality in Standard ML include function types and structured types which contain function types, such as pairs of functions or lists of functions. The consequence is that a function application such as member(Math.sin, [Math.cos, Math.atan, Math.tan]) will be rejected as being incorrectly typed. Exceptions do not admit equality either so a function application such as member(Empty, [Overflow]) will also be rejected as being incorrectly typed.
Exceptions are defined not to admit equality but why should function types not admit equality? The answer is that the natural meaning of equality for functions is extensional equality; simply that when two equal functions are given equal values then they return equal results. It is an elevated view. Extensional equality does not look inside the functions to see how they work out their answers and neither does it time them to see how long they take. A programming language cannot implement this form of equality. The type of equality which it could implement is pointer equality (also called intensional equality) and that is not the kind which we want.
Equality types can arise in one slightly unexpected place, when testing if a list is empty. A definition which uses pattern matching will assign to null the fully polymorphic type 'a list -> bool.
fun null [] = true | null _ = false;
However, if instead we use the equality on a value of a polymorphic datatype, the type system of Standard ML will assume that an equality exists for the elements also. Any parametric datatype 'a t will admit equality only if 'a does. Thus a definition which uses equality will assign to null_eq the qualified polymorphic type ''a list -> bool.
fun null_eq s = s = [];
Searching for an element by a key will allow us to retrieve a function from a list of functions. The retrieve function has type ''a * (''a * 'b) list -> 'b.
exception Retrieve
fun retrieve (k1, []) = raise Retrieve
| retrieve (k1, (k2, v2)::t) =
if k1 = k2 then v2 else retrieve (k1, t);