Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Physical Equality is not predictable #4941

Closed
vicuna opened this Issue Dec 16, 2009 · 2 comments

Comments

Projects
None yet
1 participant
@vicuna
Copy link
Collaborator

vicuna commented Dec 16, 2009

Original bug ID: 4941
Reporter: RolandGilead
Status: closed (set by @xavierleroy on 2009-12-30T14:52:59Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 3.11.0
Fixed in version: 3.12.0+dev
Category: ~DO NOT USE (was: OCaml general)
Related to: #4942

Bug description

"On mutable structures, e1 == e2 is true if and only if physical modification of e1 also affects e2."
In the attached file, one type obeys this rule, the other does not.
Either it needs to be fixed or the documentation changed because if and only if means both statements are true or both statements are false. It's just the definition of iff(if and only if).

The attached file was originally run via the toplevel, so running it that way will show more but compiling and running it will show enough. The 25 that gets printed twice is from two different values, only one of which was altered to show the 25. The true and false that are printed are the results of structural and physical equality tests, respectively.

trC and trD are created by using the same parameters to the same function and changing trC affects trD and tr1(the tree both subtrees come from) yet physical equality tests between trC and trD fail.

In a way it is also a violation of functional programming principles, one is returned values which are different even though the parameters are the same.

Additional information

Physical equality is rendered much less useful by being unpredictable.
If == doesn't work, one would have to make a type which contains a unique universal id(i.e. a pointer, which is what everyone thinks == does behind the scenes).

{contents: 'a; uuid: int}

File attachments

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Dec 16, 2009

Comment author: ertai

Physical equality is a very subtle beast. Here you got trapped by the fact that constructors allocate and thus leads to phisically different values.

assert (Some 42 != Some 42);;

More precisely consider some mutable state

let r = ref 42;;
let s1 = Some r;;
let s2 = Some r;;

(* s1 and s2 are physically different, even if mutating r affects s1 and s2 *)
assert (s1 != s2);;
r := 21;;
assert (s1 = Some (ref 21)) ;;
assert (s2 = Some (ref 21)) ;;

In your program you reallocate a RTree constructor in returnRsubtree where returning 'x' would
lead to what you expect.

It is a bit like this function:
let copyOpt = function Some x -> Some x | None -> None;;
assert (s != copyOpt s);;

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Dec 30, 2009

Comment author: @xavierleroy

All right, there is a potential misunderstanding on the clause "On mutable structures" and I'll improve the wording of the documentation should be improved. But you're going off on a tangent from there... Reminding us what "if and only if" means was definitely unnecessary.

To clear things up:

  • "==" is specified only when its arguments are of a mutable type: references, arrays, records with mutable fields, objects with mutable instance variables. There, as stated in the manual, "e1 == e2 is true if and only if physical modification of e1 also affects e2."

  • In your example, trC and trD both have type "tree", which is not mutable.
    (There is no way to change a RLeaf into a RTree in-place.) So, whether trC == trD is unspecified and actually depends on the choices made by the compiler w.r.t. allocation and sharing of data structures.

  • Both trC and trD contain a reference to tr1, which is of a mutable type. So, of course, if you mutate tr1 through the reference found in trC, you will "see" that mutation through trD as well: it's just that trC and trD share the same ref to tr1, and this is true by construction of your example.

Hope this clears things up.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.