support for pointer equality

[xrchz]

We could add an equality primitive (from some intermediate language down) that does not do the check for closures if it encounters pointer-equal data, and compile to using this primitive for equality when the compiler knows closure will not occur. Such knowledge could be added immediately after type inference.

Note: changing the current semantics of equality to return false if it encounters closures, and removing the Eq_closure exception does not work, because a traversal still needs to be done upon encountering pointer-equal objects to check for closures.

Other alternatives:

• Add a pointer-eq primitive to the source language, with semantics: if they are equal, it non-deterministically can be false or true, otherwise it must be false.
• Add a pointer-eq primitive to the source language that is only targeted by the translator. The semantics is to raise a type error if it encounters closures, but otherwise return true or false correctly. Problem: type soundness for this operator is difficult.
• Add an "annotated equality" primitive to the source language (or optional annotation on the current primitive). Annotated equality raises a type error if the arguments are not of the given type. Then, optimisation can be done when the type clearly does not contain closures. (To make this easier: no polymorphic annotations, no guarantee of optimisation when possible.)

(The motivation for this is that it is probably going to be important for efficiency on HOL Light code.)

[SOwens]

On 2015/11/10, at 13:19, Ramana Kumar notifications@github.com wrote:

Perhaps a better option: change the current semantics of equality to return false if it encounters closures, and remove the Eq_closure exception. Then this can be implemented with optimisations upon encountering pointer-equal objects.

Don’t you mean for it to return true if it encounters closures? You need pointer equality to imply structural equality.

-Scott

[xrchz]

It looks like Scott's suggestion might be the perfect one! To summarise: Change the semantics of the existing equality primitive in the source semantics to return true whenever it encounters a closure. In other words, replace Eq_closure by Eq_val true in the definition of do_eq. Then it is safe to return Eq_val true when encountering equal pointers.

[SOwens]

I’m not sure whether it should be the only equality or if we should have two versions. It is deeply weird for (fn x => x) = (fn x => x + 1) to be true.

Now that we have an oracle, could we instead expose a pointer equality primitive?

-Scott

On 2015/11/10, at 14:20, Ramana Kumar notifications@github.com wrote:

It looks like Scott's suggestion might be the perfect one! To summarise: Change the semantics of the existing equality primitive in the source semantics to return true whenever it encounters a closure. In other words, replace Eq_closure by Eq_val true in the definition of do_eq. Then it is safe to return Eq_val true when encountering equal pointers.

— Reply to this email directly or view it on GitHub.

[myreen]

My opinion: we shouldn't have many different structural equality primitives. I'm in favour of just having one. The one that does weird things with closures (returns true if at least one of the arguments is a closure). This is simple and allows for good implementations.

Whether we have pointer equality is a separate issue. I'm not a big fan, unless it becomes necessary.

[xrchz]

Plan is to add a non-deterministic PointerEq primitive to BVL, which gets resolved at wordLang (so only BVL through BVP have an equality oracle), and use this test in the code for equality in the clos_to_bvl translation. When compiling into BVL, the oracle can be anything. When compiling into wordLang, the correct oracle must be chosen.

[xrchz]

Before doing the above, change the top-level semantics of do_eq to remove the Eq_closure exception (and return true for closures, as described earlier).

[xrchz]

The pure predicate in exh_to_pat should be updated (to always treat equality as pure) after equality can no longer raise an exception. (And any other predicates on syntax doing the same thing, maybe clos_remove will do this too.)

[mn200]

As discussed in person, the current definition of clos semantics has bad equalities raising an exception, so clos_remove treats all equalities as suspect.

[myreen]

If I remember correctly from discussion about this, the plan is to move the implementation of recursive equality from BVL into wordLang, where pointer equality is naturally accessible.

I just realised that an additional benefit of moving equality to wordLang is that the IsBlock primitive can be deleted from closLang, BVL, BVI and dataLang. This has the knock on effect of us not requiring a bit to distinguish fixed-width numbers from empty constructors (nil, true, false, etc.). In other words: we'll have one more bit in every fixed num.

[myreen]

The current WordLang code for Equal does pointer equality testing internally. I believe this is far as we wanted to go with this issue. I'm closing the issue.