adding Merge Sort and Binary Search

prvshah51 commented 2 years ago

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

cpitclaudel commented 2 years ago

This is great. Following up on what Mikael said:

It would be nice to separate things out more cleanly: relations, sorting, and searching
You can take the generic comparison type from https://github.com/dafny-lang/compiler-bootstrap/commit/d9a5734a47b9dd78b3af764ea913e7a19bc8c857 (datatype Cmp)
Down the line it would be nice to support sorting reference types, but we can address that later
I worry about the performance (sorting sequences instead of arrays). In particular, I think the current code has complexity (at least in C#) n² log(n), but we can probably add a "by method" later
The main entry point probably doesn't need to be a method

It would be nice to add docstrings on the top functions, too

robin-aws commented 2 years ago

@prvshah51 I've pushed several commits to remove more code we don't need (yet!), and made a few other changes to get it ready to merge IMO:

After discussion with @atomb I've removed Comparison.dfy and stuck to plain old (T, T) -> bool relations, which simplifies things for now.
Moved Relations.dfy to the top-level src directory (since we also have Functions.dfy there already)
Added an example that sorts and then searches, which also revealed that the "sorted" precondition on BinarySearch wasn't correct!

Let me know if you have any concerns, and @atomb / @MikaelMayer I'll leave it to you two to approve since I feel a little biased now that I've thrown my own commits on this. :)

robin-aws commented 2 years ago

@MikaelMayer I just noticed you had some style requests that were lost in the shuffle. I'll respond to the ones I see that still seem relevant, but please just provide a quick comment at the top level if there are others we missed.

Re: the naming convention for predicates, e.g. "IsTotalOrder" instead of "TotalOrder", that's potentially a good idea but the latter convention is already established here in predicates like Functions.Injective. I'd suggest if you still feel strongly about it that you cut a repo issue for discussion, similar to #47.

Re: "lessThan" instead of "less", I don't have a strong opinion so I'd be willing to change it, personally. @prvshah51?

prvshah51 commented 2 years ago

Re: "lessThan" instead of "less", I don't have a strong opinion so I'd be willing to change it, personally. @prvshah51?

Both options are fine with me.

robin-aws commented 2 years ago

I approve but I still don't feel comfortable having a comparison function called twice in a binary search.

I definitely don't love it either. Both of these implementations are far from ideal when it comes to efficiency at runtime. I'm personally much more dissatisfied with my own MergeSort here rather than the binary search: it's using s[..1] expressions to recurse, and with the current compilation behavior that involves making a new copy, so the runtime is far worse than log-linear.

This whole repository needs more work to ensure it compiles to efficient-enough code for each supported language (see #24). In fact we're not even guaranteeing it is compilable at all for each target - it doesn't work for Java and hence the existence of https://github.com/dafny-lang/libraries-without-variance.

In general, I consider it good forwards progress to have a verified but inefficient definition of a concept here, since many users can live with the inefficiency in their context. But I'm looking forward to adding a lot of by method's in the future! :)

dafny-lang / libraries

adding Merge Sort and Binary Search #49