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?)
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.
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…
Yeah, you'd have to copy-paste the MSetAVL stuff from the stdlib to the development and replace
Which might occur some non-trivial performance loss, because of universe constraints… But should in theory be feasible
You could replace
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 is predicative, it's unclear it would always work.
instantiate_params_subst_spec (in Template.Typing) be in
Type? (It's currently in
It could be in Type indeed
But should it? It might become slower no?
I think it's not going to be noticeable
Last updated: Jan 30 2023 at 18:04 UTC