Bas Spitters (Nov 05 2022 at 15:07): Bas Spitters (Nov 05 2022 at 15:07):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?
Notification Bot (Nov 05 2022 at 16:10):A message was moved here from #Coq users > Typeclass resolution algorithm? by Karl Palmskog.
Karl Palmskog (Nov 05 2022 at 16:11):moving this here since more of a Coq dev or plugin question
Paolo Giarrusso (Nov 05 2022 at 16:14):IIRC, the last response was "we need to sort out primitive projections and drop the compatibility layer for those"
Paolo Giarrusso (Nov 05 2022 at 16:16):(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)
Bas Spitters (Nov 06 2022 at 07:57):What needs to be sorted out about primitive projections?
Paolo Giarrusso (Nov 06 2022 at 12:54):I was thinking of https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Quotients/near/288811182.
Paolo Giarrusso (Nov 06 2022 at 13:43):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.
Bas Spitters (Nov 06 2022 at 14:08):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.
Paolo Giarrusso (Nov 06 2022 at 14:39):I like that paper too! It introduces a type-safe alternative to Opaque that _actually_ disables conversion, which is pretty impressive!
Théo Zimmermann (Nov 06 2022 at 14:43):Does this mean an a posteriori Qed then?
Pierre-Marie Pédrot (Nov 06 2022 at 15:20):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.
Pierre-Marie Pédrot (Nov 06 2022 at 15:21):(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.)
Paolo Giarrusso (Nov 06 2022 at 15:21):Their system is pretty different, but I want to say it gives you what I'd ask from a posteriori Qed...
Paolo Giarrusso (Nov 06 2022 at 15:36):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: Apr 20 2024 at 07:01 UTC