Stream: Coq devs & plugin devs

Topic: Typeclass resolution algorithm?


view this post on Zulip 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?

view this post on Zulip Notification Bot (Nov 05 2022 at 16:10):

A message was moved here from #Coq users > Typeclass resolution algorithm? by Karl Palmskog.

view this post on Zulip Karl Palmskog (Nov 05 2022 at 16:11):

moving this here since more of a Coq dev or plugin question

view this post on Zulip 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"

view this post on Zulip 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)

view this post on Zulip Bas Spitters (Nov 06 2022 at 07:57):

What needs to be sorted out about primitive projections?

view this post on Zulip 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.

view this post on Zulip 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".

  1. Records with primitive projections are fundamentally different from normal records: primitive projections cannot be partially applied. They have to be wrapped in functions ("compatibility constants") which can be partially applied (and Coq performs this wrapping). Moreover, reducing normal projections takes _two_ reduction steps instead of one: delta-reduce the projection to unfold it and expose a match, and iota-reduce the match against the input records.
  2. 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.

  3. 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Théo Zimmermann (Nov 06 2022 at 14:43):

Does this mean an a posteriori Qed then?

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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...

view this post on Zulip 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: Feb 05 2023 at 21:03 UTC