In Standard ML, updatable cells are accessed via references. There is a type constructor, ref and a value constructor also called ref of type 'a -> 'a ref. Thus ref 1 is an int ref, ref 1.0 is a real ref, ref #"A" is a char ref, ref Empty is an exn ref and so on. We may have references to functions and even references to other references. In order to see that ref is non-functional we need only evaluate the expression (ref 0) = (ref 0) in order to discover that it evaluates to false. This is the value we should expect since we are comparing two freshly generated reference values.
Given a reference we must have a means of dereferencing it to retrieve the value which it references. If r is a real ref then !r is the real number which it references. The dereferencing operator behaves as though defined by fun ! (ref x) = x.
If r1 and r2 are references to values of the same type then we may test them for equality. This rule applies even when r1 and r2 are references to values of a type which does not admit equality (such as a function type or exn or an abstype). Notice though that in those cases where equality is defined upon the values that r1 = r2 is a distinctly different test from !r1 = !r2. We have that r1 = r2 implies !r1 = !r2 but not the other way around. Equality and dereferencing are the only built-in operations on references. In particular, arithmetic operations are not provided: it is not possible in Standard ML to increment a reference in order to move on to the next memory location.
There is a significant distinction to be made between comparing references and comparing values. Given the following bindings, a and b are equal but not a and c.
val a = ref 1; val b = a; val c = ref 1;
Notice that in Standard ML there is no way to declare a reference and omit the initial value. A declaration such as val n : int ref is not legal.
We now begin to see that the imperative features of the language can have an impact of the type-checking of programs. Carl and Elsa Gunter and Dave MacQueen write in [GGM91]:
In the Definition of Standard ML, a unary type constructor 'a F is said to admit equality if t F is an equality type whenever the parameter t is. A constructed type t F admits equality only if both t and F admit equality. This extends to n-ary type constructors in the obvious way. Unfortunately, this definition is incomplete for the inference of equality properties because of the presence of certain special type constructors that have stronger equality properties. For example, the type t ref admits equality regardless of whether t does.The paper then gives a treatment of equality types which uses a more discriminating test for admission of equality than that in the Definition of Standard ML [MTHM96].
Armed with this knowledge about references we are now able to tackle programming tasks which defeated us before. One use of references is to enable us to embellish our abstract data type for ordered sets with an equality test which is implemented as equality on sorted lists without repetitions. As before we commit to a particular ordering when we use the emptyset function. Adding elements to a set inserts them into a list, ordered by our chosen ordering. The problem of implementing an equality test on two sets as an equality test on two ordered lists is knowing whether the lists have been sorted using the same ordering. We cannot test the ordering functions with equality so we must adopt an indirect solution. Instead of storing only the function when we create an empty set we store a reference to the function. The benefit to be gained from this additional indirection is that in the equality test we can compare these references. When we cannot guarantee by this approach that the sets are ordered in the same way we raise an exception to signal their incompatibility.
abstype 'a ordered_set = Set of (('a * 'a) -> bool) ref * 'a list
with
fun emptyset (op <=) = Set (ref (op <=), [])
fun addset (x, Set (r as ref (op <=), s)) =
let fun ins [] = [x]
| ins (s as h::t) =
if x = h then s else
if x <= h then x :: s else h :: ins t
in Set (r, ins s)
end
fun memberset (x, Set (_, [])) = false
| memberset (x, Set (r as ref (op <=), h::t)) =
h <= x andalso (x = h orelse memberset (x, Set (r, t)))
exception Incompatible
fun equal (Set (r1, s1), Set (r2, s2)) =
if r1 = r2 then s1 = s2 else raise Incompatible
end;Exercise
Raising an exception when the two references are different is not necessary, it is enough to sort one of the sets using the ordering function from the other. Implement this extension.