Yannick Zakowski (Mar 06 2023 at 12:47): Yannick Zakowski (Mar 06 2023 at 12:47):Hello,
I'm afraid I am not the first one to ask questions of this flavor, but I am trying to solve universe inconsistencies that I have met for some time in the ctrees library, and I'm a bit at a loss.
These inconsistencies seem to depend on the interaction between several other libraries, and in particular a (relatively) small first case can be exhibited with only the itree library and the relation-algebra one: https://github.com/DeepSpec/InteractionTrees/issues/254
However, after turning a couple of sensible definitions universe polymorphic, I end up in a situation where things break more or less depending on order of imports, inlining, and so on, without having much of an idea of what might be going on.
Would anyone have a little well of wisdom to make progress to diagnosis and hopefully solve this kind of problem?
MackieLoeffel (Mar 06 2023 at 13:00):Maybe you are already familiar with this, but one common problem that I am aware of is https://github.com/coq-community/coq-ext-lib/issues/124 . This issues arises quite easily, so maybe relation-algebra accidentally constraints some universes of common types that are then used by other definitions?
Yannick Zakowski (Mar 06 2023 at 13:06):Ah thanks for the pointer! I need to read this in details, that seems indeed very relevant. Coincidentally I've been meaning to cut ext-lib off from itrees, that might be a good time to do so...
Paolo Giarrusso (Mar 06 2023 at 13:18):But that's not really an ext-lib bug. Can you entirely avoid higher-kinded abstractions like Kleisli/Monad? Or can you avoid their instances for template-polymorphic datatypes like option and list?
Meven Lennon-Bertrand (Mar 06 2023 at 13:20):MackieLoeffel said:
Maybe you are already familiar with this, but one common problem that I am aware of is https://github.com/coq-community/coq-ext-lib/issues/124 . This issues arises quite easily, so maybe relation-algebra accidentally constraints some universes of common types that are then used by other definitions?
Reading through this makes me wonder: how much of these issues boil down to product types being equivariant rather than contravariant on their domains? The problems showing up specifically for higher-order abstractions and being possibly fixable by η-expansion makes me think this is relevant
Yannick Zakowski (Mar 06 2023 at 13:22):Paolo Giarrusso said:
But that's not really an ext-lib bug. Can you entirely avoid higher-kinded abstractions like Kleisli/Monad? Or can you avoid their instances for template-polymorphic datatypes like option and list?
No I definitely cannot, and I don't expect cutting ext-lib to solve the issue, I just hope it'll narrow it better for me to understand what is happening. I for instance am quite confused to see the problematic constraints involve ext-lib's MonadFix, where as far as I can think we should not depend on at all.
Paolo Giarrusso (Mar 06 2023 at 13:22):The root is about template polymorphism being pretty broken: all uses of a partially applied template-polymorphic datatype share the same universe.
Paolo Giarrusso (Mar 06 2023 at 13:23):IIRC, eta-expanding gives a place to store different instances
Pierre-Marie Pédrot (Mar 06 2023 at 13:23):it should definitely be worthwhile to try to fix this by η-expanding template poly on the fly, I've been thinking about that for a while
Pierre-Marie Pédrot (Mar 06 2023 at 13:24):I'm not even sure it'd be that hard
Paolo Giarrusso (Mar 06 2023 at 13:24):A problem is hiding this from ltac matches
Pierre-Marie Pédrot (Mar 06 2023 at 13:25):Patterns are a different kind of beast, though.
Pierre-Marie Pédrot (Mar 06 2023 at 13:26):I mean that we're already doing a lot of fancy quotients in the upper layers (with relative success)
Pierre-Marie Pédrot (Mar 06 2023 at 13:27):In practice we might be able to pull it off without breaking too much stuff
Paolo Giarrusso (Mar 06 2023 at 13:27):if this is one of the successful cases instead of primitive projections, yes it'd be great, if there isn't a more fundamental fix
Pierre-Marie Pédrot (Mar 06 2023 at 13:27):(the alternative is to force partially applied template poly inductives to have an instance)
Paolo Giarrusso (Mar 06 2023 at 13:28):@Meven Lennon-Bertrand that _might_ be relevant if you're talking of universe variance, but I'm not sure if _subtyping_ constraints using a shared universe would be fine; you should check out https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 for more details
Meven Lennon-Bertrand (Mar 06 2023 at 13:37):Paolo Giarrusso said:
Meven Lennon-Bertrand that _might_ be relevant if you're talking of universe variance, but I'm not sure if _subtyping_ constraints using a shared universe would be fine; you should check out https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 for more details
AFAIKT, if you have list : Type@{list.u0} -> Type@{list.u1} and F : (Type@{F.u0} -> Type@{F.u1}) -> Y and write F (fun X : Type@{i} => list X) you get the following constraints: F.u0 = i <= list.u0, list.u1 <= F.u1 (the equality comes from equivariance on domains), while if you do not η-expand, you get instead F.u0 = list.u0, list.u1 <= F.u1, and the first equality is what kills you. In a setting with contravariance on domains (as any good subtyping should have), you'd get F.u0 <= list.u0, list.u1 <= F.u1, which is equivalent to the first set of constraints, without the extra generated i.
Meven Lennon-Bertrand (Mar 06 2023 at 13:37):So what η-expansion buys you with its extra instance is exactly contravariance on domains
Meven Lennon-Bertrand (Mar 06 2023 at 13:40):This trick is used elsewhere in the code: if the elaborator chokes on a X -> Y <= X' -> Y' constraint because it cannot get X' = X, it tries again after having η-expanded the function f of type X -> Y to fun x : X' => f x, which now has type X' -> Y' whenever X' <= X(rather than an equality)
Paolo Giarrusso (Mar 06 2023 at 14:21):that backtracking makes definition commute _less_ than we'd like, so you'd probably want the extra flexibility unconditionally (arguably, even in the existing use, but that's an existing a separate discussion because of the performance cost and questions about use-cases).
Re "contravariant subtyping", I thought that make things undecidable already in System F-omega_sub?
Pierre-Marie Pédrot (Mar 06 2023 at 14:22):it's not completely crazy subtyping, we don't have unions or intersections
Pierre-Marie Pédrot (Mar 06 2023 at 14:22):(that said it's not true in the Set model and I wouldn't be surprised if it contradicted mildly classical axioms)
Yannick Zakowski (Mar 07 2023 at 09:51):Ok I'm not yet to the point of properly understanding the Template polymorphism and other clever parts mentioned above, but a couple of more naive questions:
Print Universes Subgraph (u) to print all the constraints involving u? At least the direct neighbours in the graph if not the smallest CC containing it? It's quite paintful to explore the full graph to find all the relevant variables before being able to prune it (and even worse, if I understand correctly I can't provide constant universes such as Coq.Relations.Relation_Operators.7 to the Subgraph?) Pierre-Marie Pédrot (Mar 07 2023 at 10:03):For the second point, it boils down to the typing rules of template poly. It's a limited (and ad-hoc) form of universe poly, so e.g. if you write
Inductive Box (A : Type) := box : A -> Box A.
the typing rule of Box is morally the one you'd get writing
#[universes(polymorphic)]
Inductive Box@{u} (A : Type@{u}) := box : A -> Box A.
In particular Box A does not create a universe constraint. Unfortunately this polymorphism is local, i.e. it doesn't extend to any other construction of the language. So if you write
Definition myBox := Box.
this definition is totally monomorphic, so you get one fixed universe for the argument. By contrast, unfolding myBox would make the expression polymorphic.
Pierre-Marie Pédrot (Mar 07 2023 at 10:04):Otherwise said, template poly inductive types and their constructors are "special".
Yannick Zakowski (Mar 07 2023 at 10:10):Ah this is great, thanks a lot!
Yannick Zakowski (Mar 07 2023 at 10:48):Wait no I'm actually confused: I read you as this monomorphisation by Definition as being a quirk of the template polymorphism, but the same happens with the more general universe polymorphic one doesn't it?
Inductive Box (A : Type) := box : A -> Box A.
#[universes(polymorphic)] Inductive Box'@{u} (A : Type@{u}) := box' : A -> Box' A.
#[universes(polymorphic)] Inductive Box''@{u v} (A : Type@{u}) : Type@{v} := box'' : A -> Box'' A.
(* Mono, one universe fixed *)
Definition myBox := Box.
(* Mono, one universe fixed *)
Definition myBox' := Box'.
(* Mono, two universes fixed *)
Definition myBox'' := Box''.
Am I missing your point?
Gaëtan Gilbert (Mar 07 2023 at 11:11):you can do Polymorphic Definition but not template polymorphic
Pierre-Marie Pédrot (Mar 07 2023 at 11:12):@Yannick Zakowski the same applies if you mix univ poly / mono definitions indeed, but my point was about the fact that inlining can reduce the amount of universe breakage.
Last updated: Oct 13 2024 at 01:02 UTC