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

[ new ] Data.Tree.AVL.*.Relation.Unary.Any #1385

Merged
merged 31 commits into from
Apr 12, 2021
Merged

[ new ] Data.Tree.AVL.*.Relation.Unary.Any #1385

merged 31 commits into from
Apr 12, 2021

Conversation

gallais
Copy link
Member

@gallais gallais commented Dec 29, 2020

A first batch of relations and properties for Data.Tree.AVL
This introduces a breaking change. K&_ used to be defined like so:

K&_ :  {v} (V : Value v)  Set (a ⊔ v)
K& V = Σ Key (Value.family V)

and it is now its own standalone record:

record K&_ {v} (V : Value v) : Set (a ⊔ v) where
  constructor _,_
  field key   : Key
        value : Value.family V key

The advantage is that V can be reconstructed from a Pred (K& V) p type
which means that instead of having to pass it explicitly everywhere I can
have way cleaner types because a lot of things can be:

  • reconstructed for function calls
  • inferred to be equal for implicitly generalised variables

I'm happy with the current status. It's not a huge PR and yet it provides a
slice of the functionalities I want that is both wide & deep enough to function
as a sanity check on the design. The only thing I would consider experimental
is Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties.

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
@gallais gallais changed the title [ new ] Data.Tree.AVL.Indexed.Relation.Unary.Any [ new ] Data.Tree.AVL.*.Relation.Unary.Any Dec 29, 2020
Really happy with how much simpler the types are following the
introduction of K&_
Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not a huge PR

Yup only 600 new lines of code, definitely not huge 😆

@MatthewDaggitt MatthewDaggitt added this to the v1.5 milestone Dec 30, 2020
@gallais
Copy link
Member Author

gallais commented Dec 30, 2020

Yup only 600 new lines of code, definitely not huge

By only having one of the .Any.Properties files (and a small one at that),
and similarly only one of the .All files. :D

I only noticed the issue with K&_ after writing the Map version of the Any module.
In it I was getting unsolved metas because in the AVL one Agda was failing to detect that
some Value v arguments where equal and so the implicit generalisation was introducing
multiple copies. With the new K&_, everything works just fine.

It's more or less at the same moment I realised I could use Pred (K& V) p instead of
the nasty ∀ {k} → Value.family V k → Set p I had settled on until then.

@gallais
Copy link
Member Author

gallais commented Jan 3, 2021

Well, that took longer than expected. And led to many more changes than I had anticipated.
Which means I'll admit that this PR is now fairly large. :D

@MatthewDaggitt
Copy link
Contributor

@gallais is it okay with you if I push this to v1.6?

I'd quite like to have some time to go through the new additions, and in particular I'm a bit worried about the addition of begin-irrefl_ to the reasoning modules, as 1) it doesn't function the same way as the rest of the reasoning combinators and 2) it's not clear that there's actually a contradiction going on underneath and 3) its not backwards compatible.

@gallais
Copy link
Member Author

gallais commented Jan 12, 2021

Sure!

@MatthewDaggitt MatthewDaggitt modified the milestones: v1.5, v1.6 Jan 12, 2021
@MatthewDaggitt
Copy link
Contributor

@gallais I would really like to merge this in as it's a great piece of work, but I am still a bit dubious about the inclusion of begin-irrefl. As it's not an integral part of this PR, would you mind if I stripped it out to unblock this PR? If you're still keen to include it, we can then make a separate PR with it in, in which we can better discuss the pros and cons?

@gallais
Copy link
Member Author

gallais commented Apr 9, 2021

I think I have a plan to get us out of this pickle.

@MatthewDaggitt
Copy link
Contributor

I think I have a plan to get us out of this pickle.

Ooh, exciting 😁

@MatthewDaggitt
Copy link
Contributor

Thanks @gallais, I agree it is an improvement as it no longer breaks backwards compatibility with Reasoning.Base.Triple, and I also agree that the combinator is very convenient and it does remove a fair bit of code.

However I'm still reluctant to include this combinator. The reasoning APIs' primary purpose is to improve the readability of proofs, but in my opinion begin-irrefl_ actively harms readability:

  • Firstly, there is no indication that there's a contradiction being used underneath the hood. Knowing whether or not a proof uses contradiction is fairly crucial to understanding it.
  • Secondly, unlike when using the other combinators, there is no way to infer the final type of the reasoning proof simply by looking at it. From the reader's perspective the final type is magicked out thin air by the (invisible) contradiction.

I would argue that it's better to keep the contradiction explicit in the code?

Other opinions welcome!

@gallais
Copy link
Member Author

gallais commented Apr 11, 2021

I think begin-irrefl is clearer than:

flip contradiction (<-irrefl refl) $ begin (...)

I guess we could make the return type to force the use of ⊥-elim
as documentation that there's an explosion somewhere in there but I'm
not particularly convinced.

@JacquesCarette
Copy link
Contributor

Rather than begin-irrefl_, what about by-contradiction_ ? This would take care of @MatthewDaggitt 's first point. It doesn't fully take care of the second, though it becomes less surprising since we all know we can conjure anything we want via ⊥-elim.

Tongue-in-cheek: also have conjure-by-contradiction with 2 arguments, the first the conjured type, the second the falsity proof, that might work.

@MatthewDaggitt
Copy link
Contributor

Hmm, yup I'd be on-board with something that had contradiction in it. Would begin-irrefl-contradiction_ or begin-contradiction-by-irrefl_ be too long?

@MatthewDaggitt
Copy link
Contributor

Okay, as this is the only outstanding PR/issue blocking the v1.6 release candidate, I've temporarily removed the new combinator from this PR. Once Travis goes green, I'll merge this in and then open a new PR with the combinator restored where we can continue this discussion.

@MatthewDaggitt MatthewDaggitt merged commit d0841d1 into agda:master Apr 12, 2021
@gallais gallais deleted the avl-any branch June 7, 2021 14:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants