Paolo Giarrusso (Jan 24 2022 at 11:41): Paolo Giarrusso (Jan 24 2022 at 11:41):Pierre-Marie Pédrot said:
and in the long run, the Metacoq-vs-Iris catastrophe is in the tubes
@Pierre-Marie Pédrot you mean https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and https://github.com/coq-community/coq-ext-lib/pull/123#discussion_r784960565 ?
Pierre-Marie Pédrot (Jan 24 2022 at 11:45):yep
Paolo Giarrusso (Jan 24 2022 at 11:47):@Jason Gross showed how one might fight universe inference there, but if Notation "@ 'fmap' M becomes necessary I can't help thinking there must be a better way
Pierre-Marie Pédrot (Jan 24 2022 at 11:48):that particular issue is about template poly, but the same kind of problem may arise from arbitrary use of mono universes
Pierre-Marie Pédrot (Jan 24 2022 at 11:48):it's a manifestation of "the global universe state is not modular"
Pierre-Marie Pédrot (Jan 24 2022 at 11:50):(here despite the appearances, template polymorphism is helping precisely because it provides a poor-man universe polymorphism)
Paolo Giarrusso (Jan 24 2022 at 11:51):TLDR for others: Coq's template polymorphism can't really deal with Monad list
Pierre-Marie Pédrot (Jan 24 2022 at 11:53):... but it can with Monad (fun A => list A) (don't ask, don't tell)
Kenji Maillard (Jan 24 2022 at 11:54):Do I understand correctly that in these issues around universe levels for lists making the list inductive universe polymorphic would provide a theoretical solution ? In practice it may not be feasible because 1) it requires changing the stdlib and 2) it will probably break many developments (because of tactics incompatibilities, performance...). Am I overlooking other issues ?
Paolo Giarrusso (Jan 24 2022 at 11:55):@Kenji Maillard correct
Paolo Giarrusso (Jan 24 2022 at 11:57):the usual alternative is eta-expanding list, but here you'd have to eta-expand occurrences generated by both TC search and by Haskell-style programming. Jason's trick convinced me that you could get something done with enough effort, but it involves things like Notation "@ 'fmap' M := (@fmap (fun T => M T)). so it's not very ergonomic.
Paolo Giarrusso (Jan 24 2022 at 12:00):and I'm not entirely sure why Coq can't automatically eta-expand partially-applied list, is it just that it's not transparent and would break clients anyway?
Gaëtan Gilbert (Jan 24 2022 at 12:09):it could be implemented but the work needs to be done
and it has to be done in unclear how many places
note that it's not just eta-expand, it's eta-expand with fresh universes
Last updated: Apr 16 2024 at 21:01 UTC