11 Representation Invariants

Some values of the concrete type don't make sense as values of the concrete abstract type. For example, our ListSet implementation prohibited duplicates.

The representation invariant (RI) distinguises valid concrete values from invalid concrete values.

To document the RI, you write a comment above the representation type

(** AF: ...
    RI: The list may not contain duplicates *)
val t = 'a list

It should be written before you write the function. It should be hidden behind the abstraction barrier.

The invariant may temporarily be violated inside the body of an operation, as long as it is restored by the end of the operation. This is the same way that a loop invariant can be violated as long as it is restored by the end of the loop. One example of this is in our ListSet's union operator:

let union s1 s2 =
    s1 @ s2 |> dedup

Here, we originally construct the list s1 @ s2, before we remove the duplicates by calling dedup.