Is there still any hope that unifall will be integrated into the main branch, or did people run out of ideas to unify the algorithms?
A message was moved here from #Coq users > Typeclass resolution algorithm? by Karl Palmskog.
moving this here since more of a Coq dev or plugin question
IIRC, the last response was "we need to sort out primitive projections and drop the compatibility layer for those"
(maybe because unifall caused too many changes of those, and giving a sensible spec to primitive projections with the compatibility layer isn't really possible)
What needs to be sorted out about primitive projections?
I was thinking of https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Quotients/near/288811182.
I'm not a Coq dev and don't have updates on the unifall plans (I only answered because nobody else had), but I can try to say sth about primitive projections. Complicated details follow, but the TLDR is still "this is too messy for unifall to deal with".
Coq goes to extreme lengths to hide this difference, but doesn't succeed 100%. In particular, a primitive projection proj <parameters> record
can be represented in three forms: as a compatibility constant, as a "folded" primitive projection, and as an unfolded one; those are all syntactically different, sometimes will not unify, and Set Printing All
does not show whether a primitive projection is folded or unfolded.
Reducing a folded primitive projection takes _two_ steps instead of one — the folded primitive projection must first be delta-reduced/"unfolded" to an unfolded primitive projections, and only then can it iota-reduce.
Coq devs agree things need to change — at least, by collapsing folded and unfolded primitive projections together.
https://github.com/coq/ceps/pull/57 and https://github.com/coq/coq/issues/5698 have some extra information.
Interesting!
Aside, I like this paper on unfolding and cubical type theory by my colleagues (https://arxiv.org/abs/2210.05420). It would be great if a more principled understanding of unfolding could help here, but I haven't given it much thought.
I like that paper too! It introduces a type-safe alternative to Opaque
that _actually_ disables conversion, which is pretty impressive!
Does this mean an a posteriori Qed
then?
It's not quite the same thing as Qed, rather, it's a type-enforced kind of opacity. You'd see in the type of expressions whether you need a body to unfold for the expression to type-check.
(I'm personally convinced that the kind of "partial elements" that proved to be critical to the cubical approach to be the next big thing in type theory.)
Their system is pretty different, but I want to say it gives you what I'd ask from a posteriori Qed
...
I find the whole paper very accessible (almost no CT required) :+1:
Moreover, while their theory is pretty different, the key idea for preserving subject reduction seems to be unsealing must be _transitive_: for instance, unfolding vector concatenation must also unfold natural addition to preserve subject reduction. I fear switching Coq to their theory might be hard, but I wonder if it'd be easier to lift this idea + term-level with_transparent [definitions] t
term constructors.
Last updated: May 31 2023 at 15:01 UTC