support for pointer equality #90

Closed
xrchz opened this Issue Nov 10, 2015 · 10 comments

Projects

None yet

4 participants

@xrchz
Member
xrchz commented Nov 10, 2015

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
Member
SOwens commented Nov 10, 2015

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
Member
xrchz commented Nov 10, 2015

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
Member
SOwens commented Nov 10, 2015

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
Contributor
myreen commented Nov 10, 2015

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
Member
xrchz commented Nov 11, 2015

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
Member
xrchz commented Nov 11, 2015

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 xrchz self-assigned this Nov 16, 2015
@xrchz
Member
xrchz commented Dec 10, 2015

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
Contributor
mn200 commented Dec 10, 2015

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

@xrchz xrchz added a commit that referenced this issue Feb 4, 2016
@xrchz xrchz Make closure comparisons return true, remove Eq_closure.
As discussed in #90.

This commit changes the semantics only, proofs to be updated.
046fc8a
@xrchz xrchz added a commit that referenced this issue Feb 4, 2016
@xrchz xrchz Remove Eq_closure (#90): update compiler and backend semantics
Optimisations regarding purity analysis, and updates to proofs, to come.
42e553f
@xrchz xrchz added a commit that referenced this issue Feb 4, 2016
@xrchz xrchz Remove Eq_closure (#90): improve purity analysis in compiler
Can now treat Equality as a pure operation.
56f7922
@myreen
Contributor
myreen commented Sep 13, 2016

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 myreen added a commit that referenced this issue Nov 20, 2016
@myreen myreen Propagate rec. Equal to dataLang; GiveUp in wordLang
Progress on #90
986e9d1
@myreen myreen added a commit that referenced this issue Nov 20, 2016
@myreen myreen Fix a few broken proofs (rec. eq moves to wordLang)
Progress on #90

Some of proofs are still broken in mysterious ways:
 - bvl_to_bviProof: do_app_adjust, compile_exps_correct
 - clos_to_bvl: Op case of compile_exps_correct
8bb786c
@myreen
Contributor
myreen commented Feb 1, 2017

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.

@myreen myreen closed this Feb 1, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment