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 Prop
with Type
...
Which might occur some non-trivial performance loss, because of universe constraints… But should in theory be feasible
You could replace Prop
with Set
instead
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
Right, since Set
is predicative, it's unclear it would always work.
Should instantiate_params_subst_spec
(in Template.Typing) be in Type
? (It's currently in Prop
)
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: Mar 29 2024 at 13:01 UTC