Stream: Coq devs & plugin devs

Topic: Generalizing only over used section polymorphic universes


view this post on Zulip 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:

Do I miss something subtle at the current stage? What do you think?

Incident questions:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Hugo Herbelin (Jul 20 2021 at 15:08):

not for Qed-terminated proofs.

Couldn't the "future" prepared in declare.ml also return these used hypotheses? (misunderstanding)

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:08):

no, it needs access to the body

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:09):

Qed-terminated proofs should behave as axioms mostly

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:09):

you have to assume that you may never know the body

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 15:10):

we don't delay univ polymorphic proofs so no problem there

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:11):

hm, we could if they were fully specified

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:11):

I'd advise against making the two code paths straying further away

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 15:27):

there is little point in raising anomalies instead of errors in the kernel imo

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 15:36):

they are not synonyms

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 15:51):

it might essentially require retypechecking in the worst case

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Hugo Herbelin (Jul 20 2021 at 15:59):

Maybe it is important to keep sections apart from safe_typing???

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 16:01):

Beware with the revstruct, we're doing weird stuff with universes.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Hugo Herbelin (Jul 20 2021 at 16:14):

The minimal set of constraints would have to be computed outside the kernel.

view this post on Zulip Hugo Herbelin (Jul 20 2021 at 16:15):

Isn't it what UState.restrict does?

view this post on Zulip Hugo Herbelin (Jul 20 2021 at 16:16):

The kernel would only check inclusion.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 16:20):

right

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 16:20):

then for constraints we just restrict, that's not a problem

view this post on Zulip Hugo Herbelin (Jul 20 2021 at 16:21):

IIUC, you then mean that would work for levels but not algebraic?

view this post on Zulip Hugo Herbelin (Jul 20 2021 at 16:22):

What does restrict with algebraics?

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 16:23):

algebraics are handled at the time of adding constraints, they are not visible to restrict

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 16:24):


this thread is kinda confusing, talking about 2 or 3 different things with no transitions

view this post on Zulip 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, ... ?

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 20 2021 at 16:26):

(outside of the kernel obviously)

view this post on Zulip 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

view this post on Zulip Hugo Herbelin (Jul 20 2021 at 16:27):

@Enrico Tassi had a proposal at the ceps 51 which I tried to implement.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Jul 20 2021 at 16:42):

you're the implementor
you have the power

view this post on Zulip 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.

view this post on Zulip 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
  ...

Maybe more anecdotically, to accentuate the parallel with constr and makes comparisons easier, maybe Level.Var could be renamed Level.Rel?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Hugo Herbelin (Jul 21 2021 at 10:14):

OK


Last updated: Oct 16 2021 at 02:03 UTC