15.3.2 Finite Domains as Abstract Data Structures

A concrete finite domain consists is a finite set of elements of some type 'a. A domain is an abstract data structure for a concrete finite domain. It has the following type:

<type domain>=

%% type element = 'a
   %% type domain = unit(toIndex:element->int
   %%                    toElement:int->element
   %%                    size:Size

Every domain Dom has a function Dom.toIndex that maps elements of the concrete domain to integer indexes . Furthermore, it provides an inverse function Dom.toElement.