Cambridge University Press 1.1 Time Clock User Manual


 
26 CHAPTER 3. FURTHER CAML
α
β
(α, β)sum
inl
inr
This is similar to a union in C, but in CAML the copies of the component types
are kept apart and one always knows which of these an element of the union belongs
to. By contrast, in C the component types are overlapped, and the programmer is
responsible for this book-keeping.
3.4.1 Pattern matching
The constructors in such a definition have three very important properties:
They are exhaustive, i.e. every element of the new type is obtainable either
by inl x for some x or inr y for some y. That is, the new type contains
nothing besides copies of the component types.
They are injective, i.e. an equality test inl x = inl y is true if and only if
x = y, and similarly for inr. That is, the new type contains a faithful copy
of each component type without identifying any elements.
They are distinct, i.e. their ranges are disjoint. More concretely this means in
the above example that inl x = inr y is false whatever x and y might be.
That is, the copy of each component type is kept apart in the new type.
The second and third properties of constructors justify our using pattern match-
ing. This is done by using more general varstructs as the arguments in a function
expression, e.g.
#fun (inl n) -> n > 6
| (inr b) -> b;;
it : (int, bool) sum -> bool = <fun>
This function has the property, naturally enough, that when applied to inl n it
returns n > 6 and when applied to inr b it returns b. It is precisely because of
the second and third properties of the constructors that we know this does give
a welldefined function. Because the constructors are injective, we can uniquely
recover n from inl n and b from inr b. Because the constructors are distinct,
we know that the two clauses cannot be mutually inconsistent, since no value can
correspond to both patterns.
In addition, because the constructors are exhaustive, we know that each value
will fall under one pattern or the other, so the function is defined everywhere.
Actually, it is permissible to relax this last property by omitting certain patterns,
though the CAML system then issues a warning: