27 messages were moved here from #Coq users > Understanding the injection
tactic by Karl Palmskog.
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?
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 .
The problem with extraction is due indeed to template-poly, but that is only indirectly related to Prop ⊆ Type.
(also, we could in theory make extraction compatible with template-poly, it's just annoying)
Right, isn't Haskell extraction compatible with it?
no idea but I'd be surprised, it's a problem that happens early (at erasure)
Oh ok, for some reason it felt like when extraction fails because of template poly, the error message suggests extracting to Haskell instead.
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.)
It would not be difficult to release our library under some permissive license if people feel that would be helpful in making the transition.
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?
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.
I also believe that coq-extlib has universe polymorphic definitions for things like monads and the like.
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
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.
do you want to ask internally at Bedrock, or would it make sense to publicly advertise for volunteers like we did for VsCoq1 maintainers?
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?)
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
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