Hugo Herbelin (Jul 29 2021 at 11:38): Hugo Herbelin (Jul 29 2021 at 11:38):Hi, on a way trying to address ceps #51, I spent some time on cooking.ml. Is anyone working and having plans with it already? In any case, I would like to share a rather big factorization I could do of the code, having all the technical work (adding term and universe parameters to generalized globals, substituting vars by rels for both terms in universes, abstracting over the section context of local both terms and universes) concentrated in one function working on a refined formulation of what were called abstr_info and work_list. I'd be curious of opinions about it before proposing it as a PR. It is mostly one commit, with some documentation, but it is for instance difficult to judge it the documentation is clear enough.
If time allows, I'd be tempted to continue with some small cleaning of safe_typing and term_typing. Has anyone planned related projects, or would like to work on such kind of cleaning/documentation project, so that others can eventually enter and understand the structure of the code more easily?
Hugo Herbelin (Jul 29 2021 at 11:52):This kind of cleaning/documentation would suspectingly help the work on MetaCoq's "safechecker".
Pierre-Marie Pédrot (Jul 29 2021 at 12:01):Regarding safe_typing, I have some stuff pending for a long time about monomorphic universes and kernel side-effects, which are blocked for technical reasons on issues related to the higher layers (namely the STM). I don't know if this would interact much with your cleanup though.
Hugo Herbelin (Jul 29 2021 at 13:51):Do you have the branch online?
Hugo Herbelin (Jul 29 2021 at 13:54):By the way, was there a problem with #9380? I feel that we may gain a lot at factorizing the code around universes: it looks like we are doing always similar treatments which could be treated more uniformly.
Hugo Herbelin (Jul 29 2021 at 13:55):About term_typing, I don't know why there is a detour by Cooking.result. It looks like a useless and easy cut to eliminate.
Hugo Herbelin (Jul 29 2021 at 13:57):I don't know why the main typing functions are called translate rather than infer (or check). This looks like obfuscating their meaning to me.
Pierre-Marie Pédrot (Jul 29 2021 at 13:57):@Hugo Herbelin IIRC the problem with that PR was that it was duplicating monomorphic constraints in several places. We should strive to remove them from all kernel datatypes except the environment, because that's the only place where they make sense (barring private monomorphic constants)
Pierre-Marie Pédrot (Jul 29 2021 at 13:57):duplicating pieces of global state is not only error-prone, it's also inefficient
Pierre-Marie Pédrot (Jul 29 2021 at 13:58):currently there is still a bit of nonsense in the kernel that we use to print "monomorphic constraints introduced by a constant"
Pierre-Marie Pédrot (Jul 29 2021 at 13:58):but this is not sound, constraints really are global
Pierre-Marie Pédrot (Jul 29 2021 at 13:58):thankfully it's only used by printing
Pierre-Marie Pédrot (Jul 29 2021 at 13:59):(I think you mentioned that you wanted to remove this, which I support 100%)
Hugo Herbelin (Jul 29 2021 at 13:59):OK, I see, I thought the problem was about unifying Polymorphic and Monomorphic. But the attachment of global universes to constants is indeed a bit strange.
Hugo Herbelin (Jul 29 2021 at 14:01):Even in printing. You see (* {foo.u foo.v |= *) for constants with monomorphic universes while the only link they have with the constant is that they have been introduced by this constant, i.e. it's only about the name.
Pierre-Marie Pédrot (Jul 29 2021 at 14:01):yes, but even this is handled outside of the kernel
Pierre-Marie Pédrot (Jul 29 2021 at 14:01):(i.e. this is essentially debugging stuff)
Hugo Herbelin (Jul 29 2021 at 14:05):So, if I understand correctly, you don't want to merge Monomorphic and Polymorphic. What you want is to move the universe levels out of the "monomorphic" constant and to keep in Monomorphic only the constraints.
Hugo Herbelin (Jul 29 2021 at 14:05):In which case Monomorphic becomes mechanically a subcase of Polymorphic.
Pierre-Marie Pédrot (Jul 29 2021 at 14:06):No no, even the constraints should get out.
Pierre-Marie Pédrot (Jul 29 2021 at 14:06):the two things don't behave the same
Pierre-Marie Pédrot (Jul 29 2021 at 14:06):a monomorphic definition with only constraints is not the same as a polymorphic one with only constraints
Hugo Herbelin (Jul 29 2021 at 14:06):OK, and the constraints between non-polymorphic universes in Polymorphic would also go out of Polymorphic?
Pierre-Marie Pédrot (Jul 29 2021 at 14:07):I don't care, but I think that there is no reason either
Pierre-Marie Pédrot (Jul 29 2021 at 14:07):you might want to actually use the "weird" behaviour mentioned in an issue before
Pierre-Marie Pédrot (Jul 29 2021 at 14:07):it's useful to quantify over ghost constraints
Hugo Herbelin (Jul 29 2021 at 14:08):You mean because of lazyness of inclusion of constraints between non-variable universes in Polymorphic?
Pierre-Marie Pédrot (Jul 29 2021 at 14:08):it's not laziness, it's quantification
Pierre-Marie Pédrot (Jul 29 2021 at 14:08):a monomorphic constraints is just a polymorphic one with a set of constraints generated by default
Pierre-Marie Pédrot (Jul 29 2021 at 14:09):(more generally, I would really like to separate universe constraint extension from constant definition per se)
Hugo Herbelin (Jul 29 2021 at 14:10):Separate universe constraint extension from constant definition: sounds good a priori.
Hugo Herbelin (Jul 29 2021 at 14:11):So, what do you intend to do with constraints between non-variables in poly constants?
Pierre-Marie Pédrot (Jul 29 2021 at 14:12):Leave them around? You have to consider them anyways by transitivity.
Pierre-Marie Pédrot (Jul 29 2021 at 14:12):As soon as you allow constraints between globals and variables, you must allow constraints between globals
Pierre-Marie Pédrot (Jul 29 2021 at 14:13):and the former appear as soon as you mix mono with poly
Hugo Herbelin (Jul 29 2021 at 14:13):Re-asking just to be sure: Do you intend to have the generators of constraints which are between non-variables once for all in the global env, or to re-add them at each use in another contant (and have them only increasing the local "global graph" of a constant)?
Pierre-Marie Pédrot (Jul 29 2021 at 14:14):the second case.
Pierre-Marie Pédrot (Jul 29 2021 at 14:14):i.e. don't change anything to what we have now
Pierre-Marie Pédrot (Jul 29 2021 at 14:14):the first situation is not closed under transitivity
Pierre-Marie Pédrot (Jul 29 2021 at 14:15):if you allow two constants with var < global then by uniformity you must allow constraints between globals
Hugo Herbelin (Jul 29 2021 at 14:16):But then (wrt "the second case"), what to do with what is called monomorphic now? Will it also become "global graph" local to a constant?
Pierre-Marie Pédrot (Jul 29 2021 at 14:16):no
Hugo Herbelin (Jul 29 2021 at 14:16):why not?
Pierre-Marie Pédrot (Jul 29 2021 at 14:16):because you don't want to make everybody polymorphic
Pierre-Marie Pédrot (Jul 29 2021 at 14:17):sometimes you might have constraints local to a definition
Pierre-Marie Pédrot (Jul 29 2021 at 14:17):but this is hard to compute
Pierre-Marie Pédrot (Jul 29 2021 at 14:17):but in general you must have the global graph somewhere
Hugo Herbelin (Jul 29 2021 at 14:18):But then the argument may apply in the other direction. You might want to have polymorphic definitions with global constraints not local to a definition?
Pierre-Marie Pédrot (Jul 29 2021 at 14:18):yes, but this you can do
Pierre-Marie Pédrot (Jul 29 2021 at 14:18):it's already possible today
Hugo Herbelin (Jul 29 2021 at 14:19):But then, you still don't need to keep a notion of monomorphic constant.
Pierre-Marie Pédrot (Jul 29 2021 at 14:19):I agree that in theory you could make everything polymorphic
Pierre-Marie Pédrot (Jul 29 2021 at 14:19):but there is a reason you don't want to do that: efficiency
Hugo Herbelin (Jul 29 2021 at 14:20):This I want to understand.
Pierre-Marie Pédrot (Jul 29 2021 at 14:20):universe polymorphism is extremely costly, and for various reasons
Pierre-Marie Pédrot (Jul 29 2021 at 14:20):if you have to recompute constraints every time you use a constant, even if they are the same, this has a cost
Hugo Herbelin (Jul 29 2021 at 14:21):You mean that even the degenerate form of universe polymorphism is costly?
Pierre-Marie Pédrot (Jul 29 2021 at 14:21):I am not even talking about substitutions
Pierre-Marie Pédrot (Jul 29 2021 at 14:21):not sure what you're talking about
Hugo Herbelin (Jul 29 2021 at 14:22):I mean: is it to re-add the delayed constraints every time which is costly?
Pierre-Marie Pédrot (Jul 29 2021 at 14:22):anyways, I think we should have some live discussion about the topic with other devs working on the same kind of stuff
Pierre-Marie Pédrot (Jul 29 2021 at 14:22):yes
Pierre-Marie Pédrot (Jul 29 2021 at 14:22):but not only, substitution is costly
Pierre-Marie Pédrot (Jul 29 2021 at 14:22):plus you have to store all these instances everywhere
Pierre-Marie Pédrot (Jul 29 2021 at 14:23):"the best proof is the proof you don't write"
Pierre-Marie Pédrot (Jul 29 2021 at 14:23):there is a reason why proof by reflection is efficient
Hugo Herbelin (Jul 29 2021 at 14:23):So, a polymorphic constant which has no delayed constraints (i.e. which is the same as a monomorphic of which the associated graph actually lives on its own declaration) is not costly?
Pierre-Marie Pédrot (Jul 29 2021 at 14:24):this is the same as a monomorphic constraint, barring potential weird code paths
Pierre-Marie Pédrot (Jul 29 2021 at 14:24):but these things don't exist in practice
Hugo Herbelin (Jul 29 2021 at 14:25):The weird code paths are my points. They are consuming useless our energy and makes things more complex to users too.
Pierre-Marie Pédrot (Jul 29 2021 at 14:25):but these things are not in the kernel
Pierre-Marie Pédrot (Jul 29 2021 at 14:25):the problem lies up ahead
Pierre-Marie Pédrot (Jul 29 2021 at 14:26):the kernel is mostly ok, if you forget about the horrible side-effect system
Hugo Herbelin (Jul 29 2021 at 14:26):Yes, the management of "side effect" in the kernel is not easy to follow.
Pierre-Marie Pédrot (Jul 29 2021 at 14:26):it's also wrong
Hugo Herbelin (Jul 29 2021 at 14:27):About the kernel, it would still be better it it had more uniformity. It looks a bit like a draft paper, missing the last week of polishing before submission to reviewers.
Hugo Herbelin (Jul 29 2021 at 14:29):Afaicu, there are still universe problems at the interaction between declare.ml and safe_typing.ml. Cleaning the code would help to find them.
Pierre-Marie Pédrot (Jul 29 2021 at 14:29):Agreed.
Pierre-Marie Pédrot (Jul 29 2021 at 14:29):but it's also due to intricate design issues
Pierre-Marie Pédrot (Jul 29 2021 at 14:30):I have a PR that removes futures from the kernel, but it's a mess in the upper layers
Hugo Herbelin (Jul 29 2021 at 14:30):It seems so.
Pierre-Marie Pédrot (Jul 29 2021 at 14:30):It's not even clear what the invariants are
Pierre-Marie Pédrot (Jul 29 2021 at 14:30):even in the current situation
Pierre-Marie Pédrot (Jul 29 2021 at 14:30):making the code purely functional exposes these issues in plain light
Hugo Herbelin (Jul 29 2021 at 14:31):About making the code purely functional, I fell on some issues too. What are the plans?
Pierre-Marie Pédrot (Jul 29 2021 at 14:32):no idea
Pierre-Marie Pédrot (Jul 29 2021 at 14:33):but we should have some meeting after the summer anyways
Hugo Herbelin (Jul 29 2021 at 14:33):OK
Hugo Herbelin (Jul 29 2021 at 14:33):Back to the kernel, I'm considering also merging push_named_* and add_constant. No objection?
Pierre-Marie Pédrot (Jul 29 2021 at 14:34):dunno, it depends on the final design
Pierre-Marie Pédrot (Jul 29 2021 at 14:35):I'd like some presentation on the topic as well
Hugo Herbelin (Jul 29 2021 at 14:36):Incidentally, about the double status of section variables as local and global objects, I made some progresses, but this is where I blocked on the dependency of proof states on the global environment.
Hugo Herbelin (Jul 29 2021 at 14:38):My current conclusion is that we don't need to define x:=S.x in the goal context but rather S.x:=x outside the goal context!! (where S.x is the global copy of the section variable).
Hugo Herbelin (Jul 29 2021 at 14:39):But for that, we need to be able to modify the env_globals local to an evar...
Hugo Herbelin (Jul 29 2021 at 14:40):which is incompatible with the way it works now.
Gaëtan Gilbert (Jul 29 2021 at 14:56):why are you copying section variables?
Hugo Herbelin (Jul 29 2021 at 15:17):why are you copying section variables?
I used the word "copying" informally. The point is that it we want section variables in a goal to behave like any other goal variable, we need to be able to hide/clear them on demand. But even if we clear them, they continue to be there in the global context, potentially depending in global constants of the section. So, we may need two "copies" (one in the global env for reference from global constants, with say a qualified name, and one in the goal context, with an atomic name). Which one should be called a copy of the other is not clear. (I'm not sure I answer your question though.)
Gaëtan Gilbert (Jul 29 2021 at 15:19):we want section variables in a goal to behave like any other goal variable
do we?
Hugo Herbelin (Jul 29 2021 at 16:02):do we?
A typical situation where "we" (or at least some persons, I don't know how to estimate how many) want to clear a section variable is destruct n where n has been "consumed" and there is no reason to have its name continuing to clutter the name space.
Paolo Giarrusso (Jul 29 2021 at 16:25):Or when a tactic loops and works over all assumptions, so if you exclude a section variable from using, the Qed fails.
Paolo Giarrusso (Jul 29 2021 at 16:33):(I'm sure that point has been brought up before, together with the idea to hide those variables in the upper layers only?)
Gaëtan Gilbert (Jul 29 2021 at 16:41):isn't it just that we want to stop treating section variables as assumptions?
Last updated: Apr 19 2024 at 14:02 UTC