-
-
Notifications
You must be signed in to change notification settings - Fork 62
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
What do we do about equality? #16
Comments
It might be worth considering a notion of equality that recurs through immutable data structures like Same idea as |
There's a syntax part of this, a semantics part, and a library part. Regarding semantics of |
regarding
|
The name we pick for |
+1 for |
|
To answer (2), yes, for |
My primary use for |
Here, here. Is he saying |
|
Something that I think is weird is that an immutable |
Mutable objects are a strange case. If I have two vectors |
As another point in the design space, Pyret has several notions of equality. In summary:
IIUC, Racket lacks a general "Always Equal" for mutable values: a test to identify that mutations to one value will also mutate the other. Currently, |
Re @jeapostrophe's comment on I have a vague notion that the cost of Another use-case is weak But maybe we will come up with an equality test that avoids the problems with |
For this reason exactly, I think it'd be good to introduce a And, uh, I think this would eventually motivate migrating to yet another list representation, this time using cons cells that are not mutable and do not have object identity. But maybe one step at a time... With that in mind, this is how I figure the equality functions can be renamed and recontextualized:
|
I think in nearly all cases where I really think we should avoid introducing additional equality operators and concentrate on changing or removing the existing ones. I'd much rather change |
For an equality function that uses structural equality on immutable values, but reference equality on mutable values, is I would propose making However if If (Edit: okay it wouldn't quite be that simple, there would also need to be |
In the current Rhombus:
I think this is not ideal.
My preference is: |
One potential confusion with Maybe |
What if instead of making |
@jackfirth What should be the answer of
? |
I'd be fine with that being false, and telling people if they want to mix comparisons of exact and inexact values, they could use this: is_numerically_equal(1, exact_to_inexact(1)) Exactness-insensitive numerical equality tests make up a very tiny fraction of all equality tests. I'm not too worried about them requiring some explicitness. |
Hmm, I'm not too sure that's a good thing, as quite likely a large portion of the users (in particular students) will expect this result to be true. This can lead to serious silent bugs too. I would be okay with |
I think of it as a type mismatch. Two things of different disjoint types can't be equal, similar to how |
My current(*) personal preference:
Roughly based on the principle of least surprise: names should be intuitive enough and not do what you would not expect them to do (which is less stringent than "they should do what you expect them to do"). (*) Ask me next month for different answers. |
|
That would definitely create surprises, given how much more expensive exact arithmetic is.
I'm not at all sure this is true, and I think this must depend on what kind of program you're writing. While there are pitfalls to the convention that More generally, I'm surprised at how often opinions in this thread dismiss the status quo, as if the only reason Racket has |
My current(*) perference:
Meanwhile:
I still worry that the behavior of (*) Ask me again after you ask @Metaxal. |
Right. The key function interface doesn't provide a theoretical guarantee either. But to be fair, practically, you need to work much harder to break the invariant when you use the key function interface. In contrast, for binary relation interface, it can be broken easily, sometimes even unintentionally. That being said, we could treat the binary relation interface as "unsafe operations" and the key function interface as "safe operations".
The existing unsafe operations in Racket seems to indicate that the approach is viable. |
Currently, all classes in Rhombus automatically get structural equality by default unless they contain mutable fields. That's what 99% of use cases need anyway. |
Re: nondeterminism, we could consider it analogous to streams where a user could write a random stream. In this case, due to the memoization that is part of the Scheme standard for streams, the stream will still be deterministic in actual use. Similarly, if memoization is considered part of the specification rather than just an optimization, we could guarantee determinism. |
Mandating memoization would double the memory consumption of all collections at the very least, if not all values in the program. |
Yes that's true, it would certainly increase the memory requirement. There may be ways to mitigate this in practice, e.g. see "meh-less not meh-mo". It may even be possible to do this sharing of memoized representatives proactively in some way, maybe in cooperation with or in a process analogous to garbage collection. E.g. at the time when a representative for a value is computed, it can see if that representative is already "pointed to" by another value, and if so, reuse it. The garbage collector would not release the representative as long as at least one value is represented by it. |
That might be feasible, but I'm still not totally sure what goal it accomplishes. Are we trying to make it easier to make correct equality implementations, or impossible to make incorrect equality implementations? If it's the former, that can be done on top of a normal binary relation interface quite easily without burdening all data structures with extra memory and performance costs. If it's the latter, fundamentally that's not possible to do in Rhombus because we want interop with Racket to be possible and because the key function interface (even with memoization) still permits buggy key function implementations. |
Yes, I would say both of those. For the former, the key interface is much simpler. For the latter, I'd recommend that we explore designs in their ideal form to see whether we can bring the whole language ecosystem to a better place, what that would take, and whether it's worth it. If it came to it, a "python 3" style transition for the Racket language might be a good thing both from the perspective of Rhombus as well as Racket.
Could you give an example of what you mean here? |
After some discussion with @rocketnia, the unreduced rational number case isn't quite as bad as I first thought. Greatest-Common-Divisor algorithms exist that are faster than the factoring I had in mind. So the The |
What key function would I specify to compute if two graphs are isomorphic? |
A nonlinear example is a good choice to scrutinize. We could construct a hash representing the adjacency list representation of the graph, and that would then reduce to hash equality, assuming hashes are a key type. edit: Ah but you are asking about isomorphism -- not sure about that. One consideration is that using isomorphism as the definition for equality would prevent us from checking the stronger claim of equality using the generic equality predicate. So in this case, it may be reasonable to define a custom binary isomorphism predicate rather than use |
Not remotely efficient but we could construct the set of all isomorphic graphs, assuming sets are a key type. All isomorphic graphs would construct the same set. But looks like this problem is known to be hard. |
After chatting with @AlexKnauth, I'd like to catch up a bit.
Alex and I talked about this a bit between us, but for everyone else's sake, I actually was referring to other containers here (collections and just plain structs). The issue I was talking about was that the way these container types exist in Racket today with
I sympathize with this concern, but I hope it's clear that the built-in types in the The kind of decoupling you're going for is similar to the value I see in the
Alex and I did some thinking about whether we could come up with a more interesting general class of counterexamples. One example Alex found was that comparing lambda calculus terms for alpha-equivalence might have a quadratic cost if More generally, the question of whether the set of available key types is are complete enough is a lot like the question of whether a programming language is complete enough for its purpose. I believe it can indeed be designed like a language, not like the "ad-hoc workarounds" @sorawee is worried about. I think it actually gets rather complete very fast -- in fact, as soon as you have a built-in orderless map type, which lets you build a lot of other things set-theory-style. After that point, I think the benefit of adding more key types will be mainly for optimizations. That said, there might be some stragglers. Few programming languages have every possible feature. I don't know if what I'm about to say will make sense to anyone but me, but once we have a pretty complete language of key types, the rest of the stragglers could be almost like the ambient side effects of that language. This analogy shows up particularly well if we consider comparison mechanisms which have extra outputs or extra inputs.
So there might be a general way of finding counterexamples by asking what it would mean to have an extensible effect system in which users define creative new comparison mechanisms. Maybe the users who define these new mechanisms will just need to use "unsafe" binary comparison techniques, thus justifying the existence of those techniques for them to use. But also, the same users might appreciate that they don't have to migrate every type in the language to have it support their new entrypoints, because many of the types will just be In this sense, if
Yeah, I think the guarantees @countvajhula is going for aren't much to hope for. Rhombus doesn't exactly look like it's going to have a sophisticated type system for expressing mathematical proofs of algebraic laws, so all of its generic instances, not just this one, are going to allow a lot of misbehavior. There was at least one person early on proposing for Rhombus to be an ocap-secure language with good control of side effects, but that's not the direction most of us seem to be expecting it to go. The "guarantees" are nice in the limited sense of helping guide people toward writing well-behaved code. Beyond that, the only reason I would consider the
Absolutely. And that's honestly a great way to avoid having every value in the program need a memoized
One possible cop-out answer is that graphs could be a built-in type. :) Another possible cop-out answer is that people probably expect the generic equality interface to take somewhere around linear time, maybe quadratic time at worst, so hiding a whole graph comparison behind the generic equality operation might actually be a bad idea. But in the end, I think that in the Racket ecosystem, something that has an intense need for optimization like that should be able to use the FFI. So if you end up opting for something like binary comparison -- not quite as easy to get right as |
A minor point, but I think you can convert to deBruijin in better than
O(n^2) and then use that as the key, since structural equality would be
alpha comparison at that point. The indicies don't change for
subexpressions when they are put into larger expressions, so you need to
compute things only once.
Robby
|
Converting to deBruijin for a single term is fast. I don't know the actual asymptotic complexity off the top of my head but I expect it's pretty close to linear. But converting to deBruijin for all the sub-terms of a term, at the time of construction, from the bottom up, is more expensive. (lambda (x) (lambda (y) (x y)))
-> deBruijn
(lambda (lambda (1 0))) That can be fast because the conversion can use an environment as it goes from the top down. But from the bottom up it's not as clean: a = x
b = y
c = (a b)
d = (lambda (y) c)
e = (lambda (x) d)
-> deBruijn
a = x ; free variables stay named, only bound variables get indices
b = y
c = (a b)
d = (lambda (x 0))
; couldn't just reuse the deBruijn for c, it had to traverse it to find the y
e = (lambda (lambda (1 0)))
; couldn't just reuse the deBruijn for d, it had to traverse it again to find the x This is an example where it doesn't make sense to compute the |
Yeah, @mflatt said on Discord:
The De Bruijn index canonicalization is a counterexample where this is not easily done because the process is not context-free. |
Thanks to friends from my lab, here are two more examples:
|
Oh, the funny list doesn't work, since the key function doesn't need to produce a funny list. It could just produce the product. |
Some papers to read (thanks to Josh Horowitz and Remy Wang):
On page 2 of COMPLEXITY CLASSES OF EQUIVALENCE PROBLEMS REVISITED, |
That's fascinating and very relevant. Thank you Josh and Remy! 😆 |
The results on page 10-11 are also interesting. Subgroup equalityGiven two sets S and T, which are subsets of a finite group G, we wish to determine if the subgroup generated by S is equal to the subgroup generated by T. This can be done in polynomial time. It suffices to check generating elements. I.e., see if for each element in S (resp T), the element is a member of the subgroup generated by T (resp S). Checking for membership of a subgroup generated by a set can be done in polynomial time when G is given by its multiplication table representation (see Complete problems for deterministic polynomial time; https://www.sciencedirect.com/science/article/pii/0304397576900682) There's no known polynomial time complete invariant for subgroup-generating subset. |
I need to step away from this discussion for a bit to organize the upcoming ABE Congress next weekend on Jan 14 (which you are all invited to). But for the meeting tomorrow, I'd like to summarize some points and suggest action items for consideration:
This appendix could be a starting point to follow in tabulating the analyses and benchmark results. See you all tomorrow. |
Re "Mathematically, the key approach is not less expressive than using a binary comparator", that depends on the definition of expressiveness that you are using. Expressiveness via (unrestricted) Turing reduction allows you to use unbounded resource. But there are other kinds of reductions that take resources into account. E.g., polynomial-time reduction and log-space reduction. Language-wise, expressiveness could also take "ergonomics" into account (see e.g. "essential features" in https://www.sciencedirect.com/science/article/pii/016764239190036W). "Ergonomics" is another thing that is worth considering, too. |
This example is due to David Eppstein (https://cstheory.stackexchange.com/a/10704/68269). I find this to be very convincing and easy to understand than other examples. For any positive integers x and y, define x == y to be: x = y OR x = pq and y = pr where p, q, r are all primes with p < q and p < r. These are equivalence classes in this relation: class 1: 1 A naive way to compute whether x == y is to compute the class labels and compare them (i.e., class label is the key function)
However, the A better way is to utilize
|
Awesome example, and a highly relevant StackExchange thread for seeing other examples as well!
A nitpick: Integer factorization may not be known to be in P, but isn't known to be NP-complete either. I think that's still difficult enough to make the point. :) |
That's a great example and it certainly makes a point. But we have to ask ourselves what we are designing for -- is it to support the ability to have maximum performance in all cases, never mind that in practice these cases will be slower than they could be due to poorly written hash functions, high boilerplate and documentation-lookup related tax on the developer (a cost that many in the community have brought up, despite the high quality of docs -- this speaks to the complexity of the language rather than any failing on the part of documentation authors), and possibly even error-prone and invalid equality relations? Or would we prefer to have potentially better performance in the vast majority of cases (good by default, professionally written hash functions, high rate of success in hash preverification due to soundness and uniformity, highly optimized key type comparison used by 99% of values in the language -- remember that even without many of the proposed optimizations, and despite all this talk of performance, the key approach is currently ahead on benchmarks), more robust guarantees that may be assumed in the language (equivalence relation invariants that could support optimizations we haven't even thought of), and low developer overhead from not having to worry about writing hash functions and reading complicated docs? The key approach is dramatically simpler and comes with stronger guarantees. And after all, nothing is preventing users in these corner cases from writing binary equality predicates for their own use -- writing a simple function is all it takes. They don't need to extend the generic equality operator for that. Yet, these characterizations are only intended to make a different point -- that there are many ways of looking at something, and looking at things in one way vs another way might produce different conclusions. And these are the kinds of discussions and considerations I'd encourage more of, as I think that would help us reach the best solutions and, equally importantly, feel confident that we are making the right decisions -- whatever those decisions turn out to be! Having found myself often in the role of defending a particular position (though it isn't a role I've sought), I think I've now said and done all I should on that front. I have great faith in the core developers and everyone on this thread, so unless there are any objections, I will step down as active editor of the equality extension proposal. I am happy to resume the role if I am called upon to do so, and, as always, remain committed to helping in any way I can 🙂 |
Racket newcomers are immediately confronted with four equality operators:
equal?
, which does what you'd expect most of the time=
, which does what you'd expect if you're used to IEEE numberseq?
, which looks like "the magic fast pointer comparison / reference equality operator"eqv?
, which just looks bizarreI think we should simplify this in
racket2Rhombus. Here's a hypothetical straw proposal:equal?
and=
eqv?
eq?
to something likesame-object-reference?
and tuck it away in the corner of the docs, to make it clearer that you should only use this if you have a very good reason toIs this feasible? Can we do better?
The text was updated successfully, but these errors were encountered: