Comments (14)
Ah sorry, I originally labeled it a refactoring before re-labeling it a performance bug and removing the
refactoring label. I had not noticed you had added it back and so assumed my shaky connection meant that
github had not taken my attempted update into account.
from agda-stdlib.
Given your comment about ≤?
, is there an alternative, but still generic, implementation of ≤-total
going via Decidable _≤_
rather than TotalOrder
?
from agda-stdlib.
@jamesmckinna I don't understand your question. I noticed this problem when I wrote some code generic over a TotalOrder
(a record containing a proof that an order is total, i.e. every pair of elements is comparable - ≤-total
witnesses this for ℕ
). Data.Nat.Properties
exports ≤-totalOrder
, an instance of this record, using ≤-total
.
We could define ≤-total
in terms of _≤?_
and ≰⇒≥
, but this requires some annoying reordering of Data.Nat.Properties
. Here's what this might look like:
≤-total : Total _≤_
≤-total m n with m ≤? n
... | yes m≤n = inj₁ m≤n
... | no m≰n = inj₂ (≰⇒≥ m≰n)
from agda-stdlib.
We could define
≤-total
in terms of_≤?_
and≰⇒≥
, but this requires some annoying reordering ofData.Nat.Properties
.
I think that was the suggestion, and I think it's worth the reorganisation.
from agda-stdlib.
Yes, sorry if my comment was too oblique... @gallais is correct. Cf. my v2.0 refactorings of Data.Nat.DivMod
in #2182 ...
Moreover, the proof you offer, modulo the equivalence of _≤?_
and _<ᵇ_
, is morally the/a reimplementation of the issue's title, or not?
But I did even wonder if such a (re-)definition should moreover be under Relation.Binary.*
(somewhere as Properties
or Consequences
of being a DecPoset
?), and then that proof be instantiated in Nat
-specific terms?
Not sure why the reordering of Data.Nat.Properties
should be so annoying, other than the fact that refactoring/reimplementation might have such dependency reordering as a knock on consequence?
from agda-stdlib.
@gallais does this qualify as a bug
though?
from agda-stdlib.
I'm not sure how much we should change things wrt efficiency. What I mean is that it makes a lot of sense to have (at least) two different definitions of many concepts, one 'conceptually clean' and one 'efficient'. There's quite a number of things in (for example) Data.Rational
that would be better off existing in two version. A number already do.
I think it's a false choice to "choose" between certain definitions. Rather we should have parallel hierarchies of definitions (and equivalence proofs). I'd be happy with, say, Data.Rational.Efficient
(and same for Data.Integer
and likely many more).
There was a reason for that paper on "Realms"!!
from agda-stdlib.
@JacquesCarette in this case, there shouldn't be anything downstream of ≤-total
depending on its implementation. If we provide a choice between ≤-total
and ≤-total-fast
, there'd be no reason for a user to use ≤-total
over ≤-total-fast
, other than perhaps avoiding a single extra import. I'd be more inclined to accept your argument in cases where we do prove properties using specific implementation details (such as Data.Nat.Base._⊔_/_⊔′_
, where we do exactly that)
from agda-stdlib.
I would be strongly against -fast
suffixes: the fast version should IMO
be the default and we can have a -spec
variant for the equivalent but
more proof-friendly version.
from agda-stdlib.
I wasn't advocating using a -fast
suffix! I was trying to argue against having two different versions at all
from agda-stdlib.
Again, re:labelling this issue, not sure why this is a bug
, while at the same time arguing for improved reimplementation is not refactoring
???
from agda-stdlib.
@gallais 's comment on the PR #2440 suggests that this would be a breaking
change...(wrt intensional/reduction behaviour), so: v3.0?
from agda-stdlib.
So while I was probably misguided to rant about spec vs fast on this particular issue, it still seems that there is an issue (but with reduction behaviour). Though I must admit that I'm getting increasingly sad when we do have code that does that (depend on reduction behaviour). Having said that, I do understand that Agda may not be quite ready to deal elegantly with implementation-obliviousness.
from agda-stdlib.
@JacquesCarette writes:
... Though I must admit that I'm getting increasingly sad when we do have code that does that (depend on reduction behaviour). Having said that, I do understand that Agda may not be quite ready to deal elegantly with implementation-obliviousness.
I absolutely agree, and/but what I'm not clear about is whether we should be more diligent as contributors/reviewers in trying to enforce this: eg I'm increasingly fastidious about replacing uses of ⊥-elim
and related things (which exploit the definition of negation as an implication, and hence privilege function application as an implicit short-cut definition) in favour of explicit appeals to contradiction
etc.
A long time ago, I read a very good piece (where? google can't seem to help me find this... a mailing list somewhere?) by Frank Atanassow explicitly critiquing the use of dependent types in programming precisely because of the almost inevitable temptation/necessity of exposing implementations in types...
... and even longer ago, two authors argued for the use of dependent types in programming precisely because of its ability to (better!) support Wadler's idea of allowing pattern matching to cohabit with data abstraction, not least because such analyses tend/have tended to focus on extensional behaviour (wrt reduction) rather than complexity-sensitive intensional behaviour... so it seems we still have a long way to go ;-)
from agda-stdlib.
Related Issues (20)
- Proofs in `Data.Vec.Properties` take general properties as inputs HOT 23
- Unsolved metas in `Data.List.Properties` cf. discussion on #2415, #2359, #2365 HOT 3
- [DRY] Refactor the various definitions of 'pointwise' equality on functions/`Function`s/pointwise `Algebra`s HOT 2
- Data.List.upTo/applyUpTo can be made faster HOT 5
- Linear-time implementation of `Data.Nat.Properties.≤′⇒≤`? HOT 3
- Regression in the documentation of installation HOT 1
- Refactor ` Data.Nat.GeneralisedArithmetic` HOT 2
- Derived operators in the theory of `Relation.Binary.Structures.IsTotalOrder` HOT 5
- Deploy doc rendering for v2.1 HOT 2
- Add `Algebra.Definitions.RawGroup` and `Algebra.Properties.Group.*` HOT 5
- Get rid of inconsistent `homo` name in algebra hierarchy? HOT 5
- Release v2.1.1 HOT 22
- Reflection.AST.Definition doesn't compile in release candidate HOT 6
- two proofs suggested for `Data.List.Membership.Setoid.Properties` HOT 2
- Equivalence of characterisations of `Data.List.Membership.Setoid._∉_` HOT 1
- somethig like a typo in lib-2.1.1-rc2 HOT 5
- `Relation.Binary.Definitions._Respects₂_` seems to exchange 'left' and 'right' in its left/right projections? HOT 2
- Find all single letter publicly-exported modules and make sure they are private HOT 5
- [DRY?] Direct definition vs. generic combinators, ctd. in `Algebra.Definitions.RawMonoid` HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from agda-stdlib.