Ali Caglayan (Sep 21 2021 at 11:49): Ali Caglayan (Sep 21 2021 at 11:49):It has been apparent in various PRs and CEPs that there are some open questions about how universes should work. So to start a discussion about some of the issues involved I want to propose the following and see what others think:
The sorts Prop, SProp and Type should all be polymorphic. That is there should be universe annotations for all of them. To retrieve the previous behaviour of one Prop and SProp, we would have a flag that enables prop resizing, allowing for a monomorphic behaviour on props. When this is disabled, Prop and SProp should live at the same universe level as Type. But this would also allow for subsingleton eliminators for Prop and SProp to be polymorphic.
Just some thoughts, curious what you think. cc @Pierre-Marie Pédrot @Hugo Herbelin
Ali Caglayan (Sep 21 2021 at 11:50):I also seem to recall some discussion of moving Prop closer towards behaving like hProp but I am not sure what the details are here.
Guillaume Melquiond (Sep 21 2021 at 12:07):I am confused by your proposal. My understanding is that universes are only meaningful in a predicative setting. Since Prop is impredicative, I don't see much point in making it polymorphic. And if you are suggesting to make Prop predicative, why would anyone still use Prop instead of Type? Because of proof irrelevance?
Ali Caglayan (Sep 21 2021 at 12:11):It is my understanding that the entire point of Prop is for erasure during extraction.
Ali Caglayan (Sep 21 2021 at 12:11):But I am suggesting that this can be done predicatively
Ali Caglayan (Sep 21 2021 at 12:12):Prop would be coq's hProp
Ali Caglayan (Sep 21 2021 at 12:12):but you could also have SProp which is not obtainable in a user defined way
Pierre-Marie Pédrot (Sep 21 2021 at 12:57):Short answer: this subject is an emerging topic of research under the name "sort polymorphism" around here. This mechanism would extend the ability to quantify over indices to a quantification over arbitrary sorts.
Pierre-Marie Pédrot (Sep 21 2021 at 12:58):There are a lot of issues, both theoretical (e.g. singleton elimination) and practical (e.g. unification).
Pierre-Marie Pédrot (Sep 21 2021 at 12:59):Prop serves various purposes, included but not limited to: impredicativity / proof-irrelevance / erasure.
Pierre-Marie Pédrot (Sep 21 2021 at 13:00):hProp is not Prop, it's incompatible with an erasable semantics.
Hugo Herbelin (Sep 21 2021 at 14:02):Ali Caglayan said:
The sorts Prop, SProp and Type should all be polymorphic.
Pierre-Marie Pédrot said:
This mechanism would extend the ability to quantify over indices to a quantification over arbitrary sorts.
Is is possible that you are both taking about different things? Rethinking XProp as subtypes of Type(α), one XProp(α) for each α, with some specific property (such as subsingleton for hProp, being generated by 0, truncation and dependent function type for SProp - or something like that, being generated by 0, 1, /\, acc, eq, truncation and dependent function type for Prop, or something like that) for @Ali Caglayan and (I'm less sure though) a form of quantification over a discret set of sorts (such as both over current SProp and the Types) for @Pierre-Marie Pédrot?
Karl Palmskog (Sep 21 2021 at 15:02):from a very practical point of view, Prop is currently used as an indicator that the body of constant "should" be made opaque (thus saving memory, making parallel asynchronous proving possible, etc.)
Karl Palmskog (Sep 21 2021 at 15:04):for any changes to Prop vs SProp vs Type, I think it's crucial to figure out what happens to the overall toolchain if big projects can/should suddenly make many of their constants transparent. In particular, I think there are already memory issues for UniMath due to avoiding Qed
Pierre-Marie Pédrot (Sep 21 2021 at 15:08):@Karl Palmskog this is not completely true, we have the evergreen issue of Qed-opaque proofs of singleton types that might block when eliminating into Type.
Pierre-Marie Pédrot (Sep 21 2021 at 15:09):Namely, eq and Acc.
Pierre-Marie Pédrot (Sep 21 2021 at 15:09):Also you can perfectly put end proofs in Type with Qed. UniMath doesn't do that for other reasons.
Pierre-Marie Pédrot (Sep 21 2021 at 15:10):(namely, why bother when any theorem can be stated as an equality)
Karl Palmskog (Sep 21 2021 at 15:11):completely agree that one can't have an iron-clad rule that (only) Prop-sorted terms must (always) be opaque. I'm just saying that for better or worse, practitioners often use it as a rule of thumb.
Karl Palmskog (Sep 21 2021 at 15:14):in fact, figuring out the tradeoffs of making something opaque or transparent is arguably difficult for large projects. I was hoping to get erasure at the Coq level (instead of just in OCaml) via MetaCoq to do evaluation without getting stuck on Acc or similar, but Matthieu said a while ago that they are not there yet.
Karl Palmskog (Sep 21 2021 at 15:27):from a proof engineering standpoint, Qed is an extremely helpful abstraction barrier in that it allows you to edit a proof script with a near-guarantee that it won't break the rest of the project, which can be crucial when porting proofs to new versions of Coq. If everyone suddenly went UniMath, porting big projects without insider knowledge could easily become a nightmare.
Paolo Giarrusso (Sep 21 2021 at 19:33):would UniMath be better off in Agda anyway?
Paolo Giarrusso (Sep 21 2021 at 19:39):better: it seems that outside of (im)predicativity, that style of programming works better in Agda than Coq, and viceversa, and each is a local optimum
Paolo Giarrusso (Sep 21 2021 at 19:41):e.g. Agda doesn’t use Qed but it has much better affordances for writing “(sort-of) raw proof terms”, which is more convenient when you need precise control of definitional equalities.
Paolo Giarrusso (Sep 21 2021 at 19:42):a bit more helpfully (and I’ll stop the OT): if Coq wants to support that style, it might need so many changes it wouldn’t be Coq any more.
Ali Caglayan (Sep 21 2021 at 21:55):But a lot of people want to write "raw proof terms" using tactics. This is something agda cannot do.
Ali Caglayan (Sep 21 2021 at 21:56):But the discussion of Qed seems to be getting off topic.
Ali Caglayan (Sep 21 2021 at 21:56):There are a lot of issues, both theoretical (e.g. singleton elimination) and practical (e.g. unification).
Can we elaborate on these?
Ali Caglayan (Sep 21 2021 at 21:57):hProp is not Prop, it's incompatible with an erasable semantics.
Then isn't everything that is erasable also everything that is Qedable?
Pierre-Marie Pédrot (Sep 21 2021 at 22:14):By erasable I mean that there is a realizability intepretation / extraction process where the type can be simply replaced by unit. It's pretty much unrelated to Qed-able because there are cases of the latter where the user knows how to retrieve a canonical computable instance out of a Qed proof, but extraction does not know that.
Pierre-Marie Pédrot (Sep 21 2021 at 22:18):For instance, equality is erasable (if you assume UIP, which is the case in standard extraction) but you can't make it Qed except if you have e.g. decidable equality on the corresponding type
Pierre-Marie Pédrot (Sep 21 2021 at 22:19):Same issue with Acc replacing UIP with some variant of Markov's principle.
Ali Caglayan (Sep 29 2021 at 15:41):Also another place where prop resizing came up was here: https://github.com/coq/ceps/pull/55
Last updated: Sep 09 2024 at 04:02 UTC