On Sun, 2009-08-09 at 21:09 +0200, Alain Frisch wrote:
> On 8/9/2009 8:56 PM, Elnatan Reisner wrote:
> > My other issue is that the description of (==) for mutable structures
> > doesn't specify that it is symmetric; reading the documentation
> > literally only implies that e1 is a substructure of e2. Even just adding
> > 'and vice versa' might clean this up:
> > |e1 == e2| is true if and only if physical modification of |e1| also
> > affects |e2 and vice versa|
> 
> It depends on what 'physical modification' and 'affect' mean. Clearly, 
> the documentation means toplevel modifications of the values (i.e. 
> modifying fields for record values, or elements for arrays or strings). 
> If one includes deep modifications, then your extended criterion does 
> not work either (think about two mutually recursive records).

You're right; thanks for pointing this out. But what does this mean for
physical equality? What does it really mean? Does [e1 == e2] mean e1 and
e2 are the same entity in memory---i.e., they are equal as C pointers?

> Note that (=) sometimes terminates for cylic values.
> 
> # type t = A of t | B of t;;
> type t = A of t | B of t
> # (let rec x = A x in x) = (let rec x = B x in x);;
> - : bool = false

Again, thanks for pointing this out. But can (=) ever evaluate to true
on cyclic structures?

-Elnatan