Disjoint union is like set union, but each element is ``tagged'' with the set that it originally came from. The disjoint union of two types is a type defined by:
We can think of inl and inr as the ``tags'' associated with elements of the union.
The ML syntax for the disjoint union of A and B is
A + B. The ML constructors for disjoint union types are
inl and inr. ML also has selectors to retrieve
elements from a disjoint union. The functions are predicates that tell which ``side'' of the union an
element belongs to.
The functions and
return the original
or
values of
an element of the union. Note that outr cannot be applied to an
element in the ``left'' side and vice versa.