Stream: Coq users

Topic: Removing cumulativity


view this post on Zulip Notification Bot (Sep 20 2023 at 13:14):

27 messages were moved here from #Coq users > Understanding the injection tactic by Karl Palmskog.

view this post on Zulip Yannick Zakowski (Sep 20 2023 at 13:58):

Paolo Giarrusso said:

The most realistic strategy, there, is to fork stdlib containers to be universe-polymorphic. We have our own at Bedrock

Is this fork publicly available?

view this post on Zulip Paolo Giarrusso (Sep 20 2023 at 14:08):

Not currently, sadly (and "fork" might not be accurate — @Janno reimplemented quite a bit), but we might want to change that cc @Gregory Malecha @Janno .

view this post on Zulip Pierre-Marie Pédrot (Sep 20 2023 at 14:25):

The problem with extraction is due indeed to template-poly, but that is only indirectly related to Prop ⊆ Type.

view this post on Zulip Pierre-Marie Pédrot (Sep 20 2023 at 14:26):

(also, we could in theory make extraction compatible with template-poly, it's just annoying)

view this post on Zulip Théo Winterhalter (Sep 20 2023 at 14:26):

Right, isn't Haskell extraction compatible with it?

view this post on Zulip Pierre-Marie Pédrot (Sep 20 2023 at 14:27):

no idea but I'd be surprised, it's a problem that happens early (at erasure)

view this post on Zulip Théo Winterhalter (Sep 20 2023 at 14:30):

Oh ok, for some reason it felt like when extraction fails because of template poly, the error message suggests extracting to Haskell instead.

view this post on Zulip Guillaume Melquiond (Sep 20 2023 at 14:59):

Yes, the issue exists with Haskell too, but since evaluation is lazy there, it never triggers. (Since the result of snd is a proof term, it will never be needed, and thus the call to snd will never be evaluated in Haskell, contrarily to OCaml.)

view this post on Zulip Gregory Malecha (Sep 20 2023 at 15:24):

It would not be difficult to release our library under some permissive license if people feel that would be helpful in making the transition.

view this post on Zulip Meven Lennon-Bertrand (Sep 20 2023 at 15:33):

I think there are many homegrown such variants (I know that MetaCoq has one, we have some such bits in our logical relation project too), it might make sense to try and homogenize over a single, well maintained univ-poly alternative to the stdlib?

view this post on Zulip Gregory Malecha (Sep 20 2023 at 16:47):

For our use cases, we have fully universe polymorphic definitions as well as non-polymorphic, functorized definitions which we use to avoid some of the costs of universe polymorphism in high performance paths.

view this post on Zulip Gregory Malecha (Sep 20 2023 at 16:49):

I also believe that coq-extlib has universe polymorphic definitions for things like monads and the like.

view this post on Zulip Karl Palmskog (Sep 20 2023 at 16:56):

at risk of sounding like a broken record, we'd like to get a library like this into the Platform ASAP, and hopefully over time it could accommodate more projects. I think this is more viable than hoping (or working towards) changing Stdlib itself

view this post on Zulip Paolo Giarrusso (Sep 20 2023 at 18:58):

Agreed, we "just" need somebody to volunteer as maintainer. At least, to pick a scope smaller than stdlib2, and to pick the overloading mechanism to use.

view this post on Zulip Karl Palmskog (Sep 20 2023 at 19:18):

do you want to ask internally at Bedrock, or would it make sense to publicly advertise for volunteers like we did for VsCoq1 maintainers?

view this post on Zulip Jason Gross (Sep 22 2023 at 16:46):

I thought extraction fully erases props, not just replacing them with unit? What's an example where you actually get non-compiling code / a segfault with snd? (Is there an issue on the issue tracker about this?)

view this post on Zulip Jason Gross (Sep 22 2023 at 16:49):

Also, if we want to switch the stdlib to be universe polymorphic by default, we'll probably have to fix the tactic incompatibilities, like that congruence is much weaker when universe polymorphism is on as are pattern, destruct, and induction

view this post on Zulip Jason Gross (Sep 22 2023 at 16:53):

Jason Gross said:

I thought extraction fully erases props, not just replacing them with unit? What's an example where you actually get non-compiling code / a segfault with snd? (Is there an issue on the issue tracker about this?)

I guess https://github.com/coq/coq/issues/13486#issuecomment-734496576


Last updated: Oct 13 2024 at 01:02 UTC