Comments (12)
IMHO the two questions are not really of the same nature: there are no HITs in Coq today, and given the amount of implementation work it represents, and AFAIK has not started (only theory and prototypes are being developed, I believe), it won't be for tomorrow. So stdlib2 has no real choice there.
On the question of canonical structures vs typeclasses, on the other hand, the two options are there, and have been carried out in large libraries. So I think it is one of the missions of stdlib2 to study the pros and cons of each solution, and understand when we want to use each, at least in the scope of stdlib2 itself.
whether stdlib2 should take current Coq as gospel truth and be implemented with it in mind, or if it should rather be implemented with the spirit of Gallina/Coq in mind
Probably something in-between. Like the spirit of Coq in mind, but with a strong sense of reality ;) I want stdlib2 to be well suited for the system as it is (modulo some changes, see the work on plugins and rebindable tactics), even if it's surely not taken as gospel truth :) Of course, the library is expected to evolve with the system...
from stdlib2.
Isn't this just a parametricity translation? In any case, I don't think this should be included in the stdlib. We should rather provide a tool that generates such relations. I believe it is being done with Elpi, Mtac2, Ltac2, maybe Template-Coq and others already.
from stdlib2.
I think there is value in having these included even if they are auto-generated for some types. I am guessing that if we counted the uses of eqListA
from current stdlib, we would find it is rather popular. The most compelling use case IMO is lifting equivalence relations on user-defined types to standard-library containers of these types, for use in specifications of procedures that operate on the elements in the container. If different developments make different variants of these definitions, they will need to be translated between manually.
from stdlib2.
Personally, I'm in favor of this. I'm wondering about the logical conclusion of this though. If you pick an equivalence relation that isn't the same (provably) as libniz equality, then you are going to end up with setoids everywhere in your formalization. I embarked on a deep dive around this in grad school and came up with the realization that it gets really verbose pretty quickly. MathClasses (@spitters and @mattam82) achieves this.
Another way (as far as I understand) is using HITs. Sadly, I haven't heard much clamoring for them lately.
from stdlib2.
Perhaps the real question here is what should be the intended semantics of stdlib2?
Should it be vanille type theory, HoTT, or perhaps HoTT with classical axioms.
@SkySkimmer is working on an extension of Coq with proof irrelevance, I could imagine that similar techniques would allow an extension of Coq with quotient types.
from stdlib2.
Stdlib2 will be using Coq's theory (not extending it). Of course, some facts about axioms (like the paradoxes in Logic
today) will be relevant.
I see work on extensions of the theory (like sProp) as orthogonal, but of course they could lead to some simplifications in the library.
from stdlib2.
from stdlib2.
I've heard many reports that setoids don't scale well in terms of performance, so I'm not sure about using them. But we could easily specialize to structures with decidable equality as a first step (which is almost what the current stdlib targets if you exclude real numbers).
from stdlib2.
from stdlib2.
It is essential for stdlib2 to work now, on current versions of Coq (e.g. 8.9+), that isn't a contentious point. I think the question that I am getting at is whether stdlib2 should take current Coq as gospel truth and be implemented with it in mind, or if it should rather be implemented with the spirit of Gallina/Coq in mind. (Currently, my personal answer to this question is the later).
I see HITs as one question around this (though it is a non-issue in the immediate future given the working on 8.9 requirement). There are things that they (to my understanding) simplify dramatically, e.g. quotient types, but Gallina doesn't have them now. Should we (as library writers) say "there would be substantial benefit in adding them" and push for them or should we say "they don't exist now and we're weary to of evolving Gallina". @spitters given your work with them, what are your feelings about them? (though that is a little bit off topic)
Another (more immediate since there are alternatives) instance of this similar question is canonical structures vs type classes. Canonical structures are faster and more precisely defined (big plus there) and type classes (I and others) would argue are substantially easier to use (big plus there). So what is the right way to go? Performance dictates that we go with canonical structures, but type classes provide a simple interface and performance and inference might be able to be improved over time.
from stdlib2.
@maximedenes I agree about HITs. They don't exist now, and so there's not really any choice in the matter. stdlib2 will not use them (until they exist, if they ever do).
On the broader aspect, you have good insight into what is feasible for "some changes". At the moment, these changes are at the level of engineering, not at the level of the theory. However, this isn't always the case. One might argue that with some amount of work type classes could be strictly better than canonical structures (or vice versa) does that fit within the scope of "some changes"? Probably not given that the answer is not known, but it might be known to someone.
With setoids (as you pointed out) there is a non-trivial relationship between the theory and the performance. In my past experience with monads, the abstraction (of monads) is amazingly powerful, but the reasoning is crippled without setoids. I would claim (perhaps aggressively) that a monad library without support for setoids is essentially useless. If setoids are expensive, this begs the question about performance vs completeness. Do we include monads because they are so useful and accept slow reasoning about them? Do we exclude monads (leaving them to other libraries) because we can't make them fast? What impact would the later choice have? Would it mean we end up with 3 different (incompatible) definitions of Monad
(e.g. what we have now with ExtLib, coq-haskell, etc.)? That seems like it would fracture the libraries, is avoiding that a motivation of stdlib2? If not, why make it standard?
So, this has evolved into a more meta discussion, but it is a discussion worth having if we opt for a monolithic standard library vs a minimal prelude and smaller libraries. Both have benefits and drawbacks.
from stdlib2.
@gmalecha Coordination efforts to have a shared definition can happen out of the standard library if for some reason it is considered that this definition doesn't have its place in the standard library (either because it is not yet clear what is the right choice, or because it is not of general enough interest, etc). We could aim to have such community-maintained standard library extensions (and then we go back to the question discussed in coq-community/manifesto#15).
from stdlib2.
Related Issues (17)
- Stdlib2 license HOT 4
- Plan for backwards compatibility and deprecation HOT 3
- Policy for the superficial layout (spacing, newlines, ...). HOT 5
- Make the roadmap of the library more explicit and add dates HOT 5
- discussion of modularity mechanisms HOT 7
- Finite maps and finite sets HOT 3
- Universes HOT 10
- Naming conventions HOT 10
- Compatibility with std++ ? HOT 3
- Should auto-generated schemes be moved inside there own modules/records HOT 2
- It seems I have a short proof of P=NP - check it HOT 2
- What should go in the prelude? HOT 6
- all functions should come with parametricity proofs HOT 2
- Strict behavior for hint databases HOT 8
- What should go in stdlib? HOT 10
- Add a README and a CONTRIBUTING guide even before there is code.
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 stdlib2.