Comments (12)
A separate issue might be, also/independently, to reconsider the refactoring, not in favour of reverting the changes, but in enhancing the definitions in Algebra.Definitions.RawMagma
to be fully-fledged top-level record
s, rather than proxying via Σ
-types? Sigh...
from agda-stdlib.
redevelop the RawMagma machinery (I don't see myself being able to do this for v2.0, so barring someone else's heroic effort, one of the above approaches needs to be taken otherwise).
This seems like the right thing to do. Looking at it, it shouldn't be that hard as it's not yet widely used. I'll see what I can put together.
from agda-stdlib.
If the pattern synonym is not in scope unqualified then it should not be used to resugar.
from agda-stdlib.
If the pattern synonym is not in scope unqualified then it should not be used to resugar.
So is this an agda
bug? an emacs
issue?
Can it be locally/temporarily hacked with a DISPLAY
pragma?
As for the original PR #1948 which introduced the pattern synonym for backwards compatibility, can such things be marked as deprecated
? (I wasn't sure at the time)
And, now that it has been merged in to master
, I suppose a follow-up PR which removes all the other uses of the redundant synonym might be in order? But how to trigger a warning to other users? And how to fix @Taneb 's problem? It's typical to import Data.Nat.Base
unqualified, which introduces the synonym...
from agda-stdlib.
If the pattern synonym is not in scope unqualified then it should not be used to resugar.
The issue is, it's very easy and common to have both the actual constructor, _,_
, and the pattern synonym in scope, if someone imports both Data.Nat.Base
and Data.Product.Base
without an import list (I do this a lot)
So is this an
agda
bug? anemacs
issue?
It could be called an agda
bug, but I wouldn't be surprised if it's deliberate behaviour reasonable in some contexts.
Can it be locally/temporarily hacked with a
DISPLAY
pragma?
I don't think so? If I'm reading the Agda docs right, pattern synonyms have an implicit DISPLAY
pragma
from agda-stdlib.
So is this an agda bug? an emacs issue?
A design bug in the standard library?
For now, pattern synonyms are untyped (cf. agda/agda#2069) and so their resugaring also is.
from agda-stdlib.
So is this an agda bug? an emacs issue?
A design bug in the standard library?
Well, I introduced it... so I'd welcome a steer towards how best to fix it without having to tackle the RawMagma
definition first.
For now, pattern synonyms are untyped (cf. agda/agda#2069) and so their resugaring also is.
Yes. But see above.
from agda-stdlib.
OK, so after experimenting a bit, there seems to be a spectrum of 'solutions' to the problem, according to how much effort they require on the user's part vs that of the developer(s):
- add
hiding (less-than-or-equal)
to all client imports ofData.Nat.Base
; this is probably the easiest for the time being, but is perhaps maximally irritating to users; - deprecate the pattern synonym, and remove all uses of it from the library; this isn't a solution per se, unless coupled with the first suggestion; but would at least speed up adoption of the new representation; NB developing new proofs for the modules in which it was previously used is proving (sic) more tiresome than I had hoped/expected... :-(
- remove the pattern synonym entirely, which may break client code unexpectedly, so needs careful documentation as a breaking change (this may end up being the
simplestmoststraightforward thing to do, however, modulo the above); - redevelop the
RawMagma
machinery (I don't see myself being able to do this for v2.0, so barring someone else's heroic effort, one of the above approaches needs to be taken otherwise).
Any offers as to which you/we/users might prefer/be able to tolerate as an interim stopgap? Any other alternatives?
from agda-stdlib.
Add an extra cornercase to Agda so that we don't resugar pattern synonyms marked as DEPRECATED?
But of course the ergonomics would still be bad for people not living on the Agda bleeding edge.
Edit:
Ah but IIRC we don't really handle deprecated pattern synonyms? (at least it's the case for syntax: agda/agda#6915)
And we don't actually have DEPRECATED, we only have WARNING_ON_USAGE. 😧
from agda-stdlib.
@gallais yes I found it was indeed ok to 'deprecate' pattern synonyms via WARNING_ON_USAGE
, but that it would have required an Agda hack for such definitions to avoid the display folding (and at that point, really started to tear my hair out at the 'cure' being worse than the disease...)
from agda-stdlib.
@MatthewDaggitt thanks for picking this up!?
one reason I hadn't mustered the energy to do this was feeling too burnt out to deal with the choices needed after the discussion with @JacquesCarette on the associated issue trail #2115 ... back to #1919 ...
... but maybe your solution is (simply!) the right way to go!?
I guess I couldn't/can't see far enough ahead to see if your solution avoids creating any hostages to fortune downstream... but that may very well be (my aiming for) the perfect being the enemy of the good (enough)... ;-)
from agda-stdlib.
And ... hard not to feel that all of this arises for the sake of the original decision to avoid the breaking change of removing less-than-or-equal
completely... sigh?
from agda-stdlib.
Related Issues (20)
- Add bundles for lattice-like and module-like morphisms
- Document `variable` block indentation style HOT 5
- [DRY] what's the best way to `public`ly re-export properties/structure? HOT 5
- Use the Monoid structure of Endomorphisms to define powering HOT 1
- [DRY] More redundant `zero` fields in `Algebra.Structures`
- Why is `Data.List.Relation.Binary.Subset.Setoid.Properties` not parametrized on the `Setoid` as a whole HOT 5
- What's the 'right' notion of equality between functions? HOT 7
- [DRY] Refactor `Algebra.Solver.*Monoid` (or deprecate entirely?)
- Rename `WeaklyDecidable`? HOT 4
- Add `Algebra.Properties.IdempotentCommutativeMonoid`
- Naming of new functions `tail∘inits` and `tail∘tails` HOT 5
- comments on lib-2.1 candidate 1 HOT 9
- Unify general algebraic definitions of Divisibility and Primarity with those in Nat and Integer HOT 7
- Style for lower/upper case for initial letter in denotations HOT 7
- Restore missing proofs from `Algebra.Operations.CommutativeMonoid`
- 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.Nat.Properties.≤-total should be implemented with _<ᵇ_ HOT 14
- Data.List.upTo/applyUpTo can be made faster HOT 5
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.