Hugo Herbelin (Jul 20 2021 at 15:00): Hugo Herbelin (Jul 20 2021 at 15:00):There was a discussion in 13477 about polymorphic generalization over universe variables in sections which, currently, is mandatorily over the whole polymorphic part of the graph of universes of the section. Any objections to trying to implement a polymorphic generalization working by default only over the universes which actually occur?
A tentative way to proceed is the following:
*_entry_secunivs in the different Entries.*_entry telling which subgraph of the universe graph of the section has to be keptdeclare.ml fills this field by calling Vars.universes_of_constr (to collect used universes of a constant) and UState.restrict (to extract the subgraph of the universe section, as given, afaicu, in Section.all_poly_univs)*_secunivs field in the different Declarations.*_body and Cooking.result to propagate this information in the environmentsection_segment_of_entry, use the latter field to intersect the universes of the last section with the subgraph relative to all sections for this constant (at the same time as we do it for section variables)Do I miss something subtle at the current stage? What do you think?
Incident questions:
Proof using for universes? Could for instance the syntax @{i j} in a section be reused for telling which existing universes to use?*_entry_secctx=None in and the code of check_section_variables)? Pierre-Marie Pédrot (Jul 20 2021 at 15:02):This looks like looking for trouble kernel-wise with little benefit. I'd like to see an actual use case before deploying such a heavy machinery.
Pierre-Marie Pédrot (Jul 20 2021 at 15:03):It's not even clear it will be efficient since you'll have to compute transitive closures if I'm not mistaken.
Pierre-Marie Pédrot (Jul 20 2021 at 15:05):couldn't the computation of the used hypotheses moved outside the kernel
not for Qed-terminated proofs.
Gaëtan Gilbert (Jul 20 2021 at 15:07):you will have to ensure that the added constant is checked in an env with only the allowed univs/constraints, or do some analysis to ensure that checking in the full env is equivalent
There seems to be also a question of syntax. What would be an anologous of Proof using for universes? Could for instance the syntax @{i j} in a section be reused for telling which existing universes to use?
we need not stick with that syntax everywhere, we could do Proof using var1 var2 (universes a b c | a < c) for instance (not sure if the constraints go into proof using)
Hugo Herbelin (Jul 20 2021 at 15:08):not for Qed-terminated proofs.
Couldn't the "future" prepared in (misunderstanding)declare.ml also return these used hypotheses?
Pierre-Marie Pédrot (Jul 20 2021 at 15:08):no, it needs access to the body
Pierre-Marie Pédrot (Jul 20 2021 at 15:09):Qed-terminated proofs should behave as axioms mostly
Pierre-Marie Pédrot (Jul 20 2021 at 15:09):you have to assume that you may never know the body
Gaëtan Gilbert (Jul 20 2021 at 15:10):we don't delay univ polymorphic proofs so no problem there
Pierre-Marie Pédrot (Jul 20 2021 at 15:11):hm, we could if they were fully specified
Pierre-Marie Pédrot (Jul 20 2021 at 15:11):I'd advise against making the two code paths straying further away
Hugo Herbelin (Jul 20 2021 at 15:24):Computation of variables: I agree, global_vars_set need to be called and checked against declared in the kernel but the error message could be treated outside the kernel (with the kernel returning an anomaly instead if the computation is wrong). Also, there could be only one path in the kernel, i.e. treating the computation done in the case None outside of the kernel. (More generally, the redundancies in the kernel do not help to make it simple.)
Pierre-Marie Pédrot (Jul 20 2021 at 15:25):I think this changed recently though, at some point I remember raising anomalies and I believe @Enrico Tassi reverted that.
Gaëtan Gilbert (Jul 20 2021 at 15:27):there is little point in raising anomalies instead of errors in the kernel imo
Enrico Tassi (Jul 20 2021 at 15:28):No, in the end I did not finish https://github.com/coq/coq/pull/14297 because on one hand I could easily work around it, and on the other end it was not a little change, IIRC
Enrico Tassi (Jul 20 2021 at 15:29):The code is still there if someone wants to pick it up, but I closed the PR since it was stale.
Hugo Herbelin (Jul 20 2021 at 15:32):My feeling was that the error message in Term_typing.check_section_variables was more talking about the surface language (Proof using) and thus more relevant for declare.ml or proof_using or pretyping, than about checking.
Hugo Herbelin (Jul 20 2021 at 15:34):Incidentally, the two terminologies "delayed" and "opaque" seem competing. That's also a point making the code difficult to follow. Is there a preference for one of them?
Enrico Tassi (Jul 20 2021 at 15:35):Use opaque. At some point I'd like to remove delayed from the kernel, and have only the document manager know the difference between an axiom and a delayed proof.
Gaëtan Gilbert (Jul 20 2021 at 15:36):they are not synonyms
Hugo Herbelin (Jul 20 2021 at 15:47):About always providing a type, why not to do it now? That would simplify things kernel-wise, no?
Hugo Herbelin (Jul 20 2021 at 15:48):At worst, keeping a boolean somewhere for printing purpose so that we remember if the user had given a type explicitly or not.
Hugo Herbelin (Jul 20 2021 at 15:49):This looks like looking for trouble kernel-wise with little benefit. I'd like to see an actual use case before deploying such a heavy machinery.
It is not clear to me that it is a more heavy machinery than what already exists for hypotheses.
Pierre-Marie Pédrot (Jul 20 2021 at 15:50):checking for the presence of a hypothesis in the term is easy, checking a transitively implied dependency is harder
Pierre-Marie Pédrot (Jul 20 2021 at 15:51):it might essentially require retypechecking in the worst case
Hugo Herbelin (Jul 20 2021 at 15:52):You mean that taking the subgraph of a graph only by looking at some nodes of interest requires transitivity?
Hugo Herbelin (Jul 20 2021 at 15:56):A propos, what is the purpose of replicating the structure of the revstruct in the Section.entries (compared to just the number of entries to drop)? Is it for "double-checking", or to be more explicit about what is done?
Hugo Herbelin (Jul 20 2021 at 15:57):I'm asking the question wrt the approach where section variables are normal entries put in the revstruct.
Hugo Herbelin (Jul 20 2021 at 15:58):By doing so, information which has to be kept in the Section.t could be found directly in the revstruct.
Hugo Herbelin (Jul 20 2021 at 15:59):Maybe it is important to keep sections apart from safe_typing???
Hugo Herbelin (Jul 20 2021 at 16:00):But at the same time, it seems that it would make things simpler to let safe_typing explicitly know that some fields of the revstruct are destined to be eventually discharged.
Pierre-Marie Pédrot (Jul 20 2021 at 16:01):Beware with the revstruct, we're doing weird stuff with universes.
Pierre-Marie Pédrot (Jul 20 2021 at 16:01):Sections need to track the exact set of universes added, which AFAIK is not easily obtainable from the revstruct.
Gaëtan Gilbert (Jul 20 2021 at 16:02):I don't know about this plan of calling section variables constants, I thought we would just have a new Var node
Hugo Herbelin (Jul 20 2021 at 16:12):it might essentially require retypechecking in the worst case
By having section variables be constants, we could also type-check a constant at once in its restricted context.
I mean, a segment would typically have this form: SectionMarker, Universe i, Constraint c, [ctx ⊢ Variable x], [ctx ⊢ Constant d], ...where each ctx is a subset of the section context (similar to const_hyps, and even a list of section contexts, one by section level). At the time of type-checking d, we first check that its ctx is a subcontext (including universes) of the section context, then type-check it in this context rather than in the full section context. Cooking is then as before (successively abstracting over each level of ctx).
Do I miss details at this point?
Pierre-Marie Pédrot (Jul 20 2021 at 16:13):this looks sound to me, but it's introducing more implicit behaviours and you can't easily synthetize the minimal set of constraints if I give you just the body
Hugo Herbelin (Jul 20 2021 at 16:14):The minimal set of constraints would have to be computed outside the kernel.
Hugo Herbelin (Jul 20 2021 at 16:15):Isn't it what UState.restrict does?
Hugo Herbelin (Jul 20 2021 at 16:16):The kernel would only check inclusion.
Pierre-Marie Pédrot (Jul 20 2021 at 16:16):probably not, because it's very hard to get a minimal set if I just give you the body and the original set, you need to reinfer everything
Gaëtan Gilbert (Jul 20 2021 at 16:19):"minimal" is not always meaningful for universe constraints (consider a <= max(b,c))
however it is meaningful for universe levels (exactly the ones appearing)
Pierre-Marie Pédrot (Jul 20 2021 at 16:20):right
Gaëtan Gilbert (Jul 20 2021 at 16:20):then for constraints we just restrict, that's not a problem
Hugo Herbelin (Jul 20 2021 at 16:21):IIUC, you then mean that would work for levels but not algebraic?
Hugo Herbelin (Jul 20 2021 at 16:22):What does restrict with algebraics?
Gaëtan Gilbert (Jul 20 2021 at 16:23):a given term can be well-typed iff a <= max(b,c)
then there is no unique minimal set of constraints between levels to check it
Gaëtan Gilbert (Jul 20 2021 at 16:23):algebraics are handled at the time of adding constraints, they are not visible to restrict
Gaëtan Gilbert (Jul 20 2021 at 16:24):this thread is kinda confusing, talking about 2 or 3 different things with no transitions
Hugo Herbelin (Jul 20 2021 at 16:25):Then, I'm going back to a previous point (representation of section variables):
I thought we would just have a new Var node
Then a split of named_context into goal_context and section_context, with safe_push_named going to the section_context, the named_context moved outside the kernel, the VarRef referring to the new node, ... ?
Pierre-Marie Pédrot (Jul 20 2021 at 16:25):something like that, the hard part being that we must track the association var -> varref
Pierre-Marie Pédrot (Jul 20 2021 at 16:26):(outside of the kernel obviously)
Gaëtan Gilbert (Jul 20 2021 at 16:27):yeah something like that
with
type variable = { sec_var : bool; id : Id.t }
type kind = ... | Var of variable | ...
type globref = ... | VarRef of variable
maybe
Hugo Herbelin (Jul 20 2021 at 16:27):@Enrico Tassi had a proposal at the ceps 51 which I tried to implement.
Hugo Herbelin (Jul 20 2021 at 16:29):That in a goal context, there is an extra table telling which goal variables are the replication of a section variable. Basically, this is not different to telling that some variables of the context are replications of the form x := Var{sec_var=true; id=x} where we hide that x has a body.
Hugo Herbelin (Jul 20 2021 at 16:33):I was talking about a Const node because Var {sec_var=true;id} would be cheaper to implement as a Const node than by modifying the syntax.
Gaëtan Gilbert (Jul 20 2021 at 16:42):you're the implementor
you have the power
Hugo Herbelin (Jul 20 2021 at 16:48):I'm ready here to implement but if what I implement is consistent with what others have in mind, that would be good.
Hugo Herbelin (Jul 21 2021 at 08:57):@Gaëtan Gilbert : would it make sense to slightly modify the level of abstraction on which to focus when dealing with polymorphic constraints and that the type UContext.t absorbs in its definition the Name.t array which most of the time comes with it, i.e. in the style:
module UContext =
struct
type t = Name.t array * Instance.t constrained
let make x = x
let names (names, _) = names
let instance (_, (univs, _cst)) = univs
let constraints (_, (_univs, cst)) = cst
...
so that the analogy with AUContext is clearer, i.e.:
global_level_1 as name_1, ..., global_level_n as name_n |- graph(global_level_1, ..., global_level_n)
vs
name_1, ..., name_n |- graph(rel 1, ..., rel n)
where, in both cases the "names" are only for printing (in the style of the names in constr)
and in particular so that it is clearer that Polymorphic_entry and Polymorphic are essentially the same, the former representing binders with global levels and the second with de Bruijn indices
so that Monomorphic_entry and Polymorphic_entry uniformly take a single argument
Maybe more anecdotically, to accentuate the parallel with constr and makes comparisons easier, maybe Level.Var could be renamed Level.Rel?
Hugo Herbelin (Jul 21 2021 at 09:07):Actually, more radically, about UContext vs AUContext, what does it bring to have a de Bruijn abstract representation for universe graphs? Since all internal names are always fresh and (compared to lambda-calculus) there is no higher-order reduction and no need for alpha-conversion, is there a technical reason for using indices rather than global names or is it mostly for the sake of "elegance" and canonicity of the representation?
Gaëtan Gilbert (Jul 21 2021 at 09:08):@Gaëtan Gilbert : would it make sense to slightly modify the level of abstraction on which to focus when dealing with polymorphic constraints and that the type UContext.t absorbs in its definition the Name.t array which most of the time comes with it
yes
Gaëtan Gilbert (Jul 21 2021 at 09:08):Maybe more anecdotically, to accentuate the parallel with constr and makes comparisons easier, maybe Level.Var could be renamed Level.Rel?
beware, constr rel is 1 based but univ var is 0 based
Gaëtan Gilbert (Jul 21 2021 at 09:10):Actually, more radically, about UContext vs AUContext, what does it bring to have a de Bruijn abstract representation for universe graphs? Since all internal names are always fresh
name freshness for this purpose is hard to guarantee at kernel level AFAIK
also substituting with lookup in an array is probably faster than with lookup in a Level.Map.t
Gaëtan Gilbert (Jul 21 2021 at 09:11):also it makes it harder to confuse them with global universes, eg when debugging if you see a Var you know some substitution was skipped
Pierre-Marie Pédrot (Jul 21 2021 at 09:18):constr rel is 1 based but univ var is 0 based
and rels are indices when universe variables are levels
Hugo Herbelin (Jul 21 2021 at 10:10):Gaëtan Gilbert said:
yes
Then, do you prefer Name.t array * Instance.t constrained or to include the names in some new kind of instance with names?
Gaëtan Gilbert said:
also substituting with lookup in an array is probably faster than with lookup in a Level.Map.t
also it makes it harder to confuse them with global universes, eg when debugging if you see a Var you know some substitution was skipped
OK to me.
About freshness, isn't an absolute file name and a fresh int, as it is now, enough?
Hugo Herbelin (Jul 21 2021 at 10:13):Pierre-Marie Pédrot said:
constr rel is 1 based but univ var is 0 based
and rels are indices when universe variables are levels
Ah, de Bruijn levels, indeed. Would it simplify discharge_abstract_universe_context to use indices?
Gaëtan Gilbert (Jul 21 2021 at 10:14):Then, do you prefer Name.t array * Instance.t constrained or to include the names in some new kind of instance with names?
the first one
Hugo Herbelin (Jul 21 2021 at 10:14):OK
Last updated: Jun 05 2023 at 10:01 UTC