Stream: MetaCoq

Topic: Prop


view this post on Zulip Jason Gross (Oct 23 2022 at 16:34):

Following up on https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/Non-squashed.20typing.20judgments.3F/near/305648084, is there a principle behind when MetaCoq puts things in Prop vs Type? ( / what is it?)

view this post on Zulip Meven Lennon-Bertrand (Oct 26 2022 at 13:29):

To answer your two questions at once: in PCUIC/Template, I would say we use Prop mainly when reusing parts of the standard library, but we could probably do without. And afaik this is not very principled. In SafeChecker, though, since we want to eventually extract our code, we use Prop (and squashing) to separate relevant and irrelevant arguments to functions.

view this post on Zulip Meven Lennon-Bertrand (Oct 26 2022 at 13:30):

So the "meta-theory" could probably be made HoTT compatible, at the cost of reimplementing quite a few things. In particular, for universes we use an efficient set implementation, which afaik exists only with Prop-valued predicates, and would probably prove quite painful to port…

view this post on Zulip Jason Gross (Oct 26 2022 at 13:32):

Yeah, you'd have to copy-paste the MSetAVL stuff from the stdlib to the development and replace Prop with Type...

view this post on Zulip Meven Lennon-Bertrand (Oct 26 2022 at 13:33):

Which might occur some non-trivial performance loss, because of universe constraints… But should in theory be feasible

view this post on Zulip Jason Gross (Oct 26 2022 at 13:34):

You could replace Prop with Set instead

view this post on Zulip Meven Lennon-Bertrand (Oct 26 2022 at 13:36):

Ah, right! Although then me must ensure that we keep quite a few things small. While this should be doable, I had a nasty surprise a while ago when noticing that (for probably silly but annoying to debug reasons) term cannot be put in Set

view this post on Zulip Théo Winterhalter (Oct 26 2022 at 13:40):

Right, since Set is predicative, it's unclear it would always work.

view this post on Zulip Jason Gross (Nov 02 2022 at 18:27):

Should instantiate_params_subst_spec (in Template.Typing) be in Type? (It's currently in Prop)

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:46):

It could be in Type indeed

view this post on Zulip Théo Winterhalter (Nov 23 2022 at 13:35):

But should it? It might become slower no?

view this post on Zulip Matthieu Sozeau (Nov 24 2022 at 11:33):

I think it's not going to be noticeable


Last updated: Mar 29 2024 at 13:01 UTC