10.8. Frozen types🔗

(Also mentioned above under automated proof search.) A frozen type wraps a composite type. A value of a frozen type can not have its fields be modified, and can not be compared by reference. Frozen types can be used to make a procedure appear deterministic to callers, even when it allocates mutable objects that survive the call.

A reads clause specifies that a procedure always returns the same value, if the read references have the same values and if the explicit input arguments, which excludes the heap, are the same. A procedure that returns a newly created object, which has a reference counter that depends on the counter of the input heap, can thus never satisfy a reads clause. For this purpose Laurel allows erasing the counter from a reference value. A Laurel Frozen type takes a regular reference type, and produces a type that is the same except that it does not support reference equality or mutation of its fields. Record types are composite types that are frozen by default.

The following sketch (syntax illustrative — reads clauses, records, and Frozen are still being designed) shows why the erasure matters. Each procedure declares an empty reads clause, claiming its result depends on nothing in the heap:

record Tuple { var fst: int; var snd: int }
composite MutableTuple { var fst: int; var snd: int }

procedure makeRecord() reads {} returns (r: Tuple)
{ return Tuple(1, 2) };                  // ok: records are frozen, no reference identity

procedure makeFrozen() reads {} returns (r: Frozen<MutableTuple>)
{ ... };                                 // ok: the counter is erased, so the result is heap-independent

procedure makeMutable() reads {} returns (r: MutableTuple)
//                      ^^^^^^^^ fails: the new object's identity depends on the heap counter
{ return new MutableTuple(1, 2) };

makeRecord and makeFrozen satisfy the empty reads clause because neither result carries a heap-dependent reference counter, so calling either twice with the same inputs yields equal results. makeMutable returns a fresh MutableTuple whose reference identity is drawn from the heap's allocation counter, so its result differs between calls and cannot satisfy an empty reads clause.