Representation independence and equality

We will now consider replacing the implementation of the Set structure which uses functions by one which uses lists as the underlying concrete representation for the set. For convenience we will assume that we already have a structure containing utilities for lists such as a membership predicate.

structure Set :> Set =
   type ''a set = ''a list
   val emptyset = []
   val addset = op ::
   val memberset = ListUtils.member

We might feel fearful of making this change because--unlike functions over equality types--lists of values from equality types can themselves be tested for equality. Equality on lists is not the same as equality on sets and so we might fear that this implementation of Set would have the disadvantage that it allows sets to be tested for equality, giving inappropriate answers. Such fears are misplaced. The equality on the type ''a set is hidden by the use of the Set signature. Tight lipped, the signature refers to ''a set as a type, with no indication that it admits equality. Thus we see that signatures are to be interpreted literally and not supplemented by other information which is obtained from peeking inside the structure to see how types have been defined. The terminology for this in Standard ML is that signatures which are attached using a coercion `:>' are opaque , not transparent .

The question of whether or not signatures should be opaque is typical of many questions which arise in programming language design. The exchange being made is between the purity of a strict interpretation of an abstraction and the convenience of software re-use. Transparent signatures may save a significant amount of work since the software developer is able to exploit some knowledge about how a structure has been implemented. This saving may have to be paid for later when a change of data representation causes modifications to be made to other structures.


Reimplement the 'a susp datatype [*] as a structure Susp. You will notice that in the body of the structure neither the local .. in .. end nor the abstype .. with .. end are necessary. The effects of hiding the 'a hitchcock datatype and hiding the equality on 'a susp values can both be achieved through the use of a signature.