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

Universal equality mergeable WIP #393

Merged
merged 8 commits into from
Mar 18, 2019
Merged

Universal equality mergeable WIP #393

merged 8 commits into from
Mar 18, 2019

Conversation

pchiusano
Copy link
Member

This adds the builtin:

(Universal.==) : a -> a -> Boolean

And renames Nat.== to Nat.equal, Float.== to Float.equal, etc. So it's expected that you'll just use == everywhere and have TDNR take care of it. An optimizer might put in the monomorphic versions if they're faster, but programmer shouldn't have to sweat that IMO.

The implementation works for all types using the same notion of equality used to compute Unison hashes (alpha equivalence of the normalized value). So it compares values structurally. Functions it compares based on their hash, followed by comparison of any partially applied arguments. There's one trick, which is that functions may be applied to themselves, creating a cycle. See CyclicEq in Unison.Util for the typeclass that handles this - the general idea is that the equality check needs to keep some state of what it's seen before to break the cycle. And then this is the interesting case of the CyclicEq implementation for Value.

There's still a few things to fill in, but it seems to work fine and I'd like to merge to keep it from diverging from master (I already had to deal with conflicts).

Known issues:

  • We'd ideally like to give Universal.== a more constrained type, so that functions which are parametric get the same free theorems. Something like forall a . Eq a => a -> a -> Boolean. This doesn't require full-blown typeclasses. For v1 of Unison, these constraints might be "magic" but for the future we might figure out a way of letting users define their own.
  • == on Effect values will currently bomb - this needs filling in, and it requires comparing the IR inside the continuations for equality, which is straightforward but hasn't been done yet. Comparing Effect values for equality is a pretty weird thing to do (and we had no way of doing it previously) but we should still fill this in for completeness.

@pchiusano pchiusano changed the title Universal equality Universal equality mergeable WIP Mar 15, 2019
@francisdb francisdb mentioned this pull request Mar 15, 2019
@pchiusano
Copy link
Member Author

@aryairani and I just discussing, came up with a simple scheme to avoid too much breakage as we evolve the set of builtins. Am going to add to this PR.

Have two maps, one of type Map Reference Type, which only increases monotonically, unless we decide to garbage collect it. This will live in Builtin.hs. Then there's a map Map Name Reference which is used for initializing the namespace of new branches (need the same sort of thing for types). This could also live in Builtin.hs I suppose. The idea is that old references always refer to the same thing, even as Unison's builtins evolve.

Note: will need to do the same thing in the mapping from Reference to IR, have that be a monotonic map.

Also discussed having a way to deprecate builtins - make it a Map Reference (Type, DeprecationStatus) that lets you surface to the user that their program typechecks but can't be run anymore because it relies on deprecated builtins.

@atacratic
Copy link
Contributor

About the structural equality: does (2 + 2) == 4 in this scheme? (And what does == resolve to in that expression?)

@runarorama
Copy link
Contributor

@atacratic In that case, 2+2 will evaluate strictly to 4, so it ends up being 4 == 4.

@aryairani
Copy link
Contributor

@atacratic (2+2)==4 but '(2+2) != '4, I’d expect.

@aryairani
Copy link
Contributor

@atacratic It would resolve to Universal.== as things stand.

@atacratic
Copy link
Contributor

OK cool. I was confusing myself, thinking that Universal.== was somehow being passed unevaluated arguments.

@atacratic
Copy link
Contributor

(Comparing effect values sounds useful for testing. "Question 1: does this computation return the value I expect? Question 2: did it have the effects along the way that I expect?")

@pchiusano
Copy link
Member Author

@aryairani actually, do you want to add the upgrade path stuff to this branch? I don't think I'll get to it for a couple days and I think you have a clearer idea of what to do.

I also think it could be better to address with a separate PR, since I feel like we are going to want to start adding version prefixes to the builtin Reference values and that's going to be a pretty substantive change.

@aryairani
Copy link
Contributor

@pchiusano My preference is simply to avoid merging the altered references (Nat.equal, etc.) into master.

We could just:

  1. back out the reference changes in this PR (in Builtins.builtins0, IR.decompileIR, IR.underapply), meaning you have to fully qualify Universal.==
  2. do a second PR which decouples those names from references and renames away Nat.==, Int.==, Float.==.

I'm happy to handle 1. or 2. or both, just lmk.

@pchiusano
Copy link
Member Author

I think I was stuck on 1 because some tests started failing as they use == unqualified and now two things match. But I think just update those tests to not use TDNR, and rename the monomorphic versions back to their original names.

The other refactoring can be separate PR.

@aryairani
Copy link
Contributor

Makes sense.

@pchiusano
Copy link
Member Author

I’ll do 1, we can merge, then you can do 2 at your leisure. 😀

@aryairani
Copy link
Contributor

Sounds good, I'll do 2. tomorrow.

@pchiusano
Copy link
Member Author

Okie dokie, reverted the names to what they were before and updated the tests that were failing, just adding a use Universal == at the top of any failing tests.

@pchiusano
Copy link
Member Author

pchiusano commented Mar 18, 2019

@aryairani you can take a look at 80b459a if you want, it renames Nat.equal back to Nat.==, etc. I'll merge in the morning if you don't beat me to it.

@aryairani
Copy link
Contributor

@pchiusano Pls revert in IR.decompileIR too and then probably good to go.

@pchiusano
Copy link
Member Author

@aryairani thanks for catching that, shoulda verified with grepping, looks good now -

$ rg Nat.equal
$ rg Float.equal
$ rg Text.equal
$ rg Int.equal
$

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants