Stream: Coq devs & plugin devs

Topic: Canonical Structures


view this post on Zulip Janno (May 13 2020 at 15:14):

To reiterate what I said in the call just now: there are two improvements that I think would make canonical structures with function fields more useful:

  1. requiring fewer casts in situations where the solution should be unique and obvious. https://github.com/coq/coq/issues/11189 is one example.
  2. allowing dependent functions. I've started working on this but my understanding of the code is.. minimal at best. Here's the diff so far: https://github.com/Janno/coq/commit/4f6a31c87fcd28a0ad3d2a200b8fd420e39d4415. That commit also has a test case that I think should eventually pass.

view this post on Zulip Janno (May 13 2020 at 15:15):

(That branch contains a renaming of Prod_cs to Impl_cs so that I can use Prod_cs for dependent functions. It's a bit confusing, I must admit!)

view this post on Zulip Janno (May 13 2020 at 15:23):

Okay, maybe it wasn't so difficult after all: https://github.com/coq/coq/compare/master...Janno:janno/cs_dep_fun seems to make the test pass. I wonder if it makes any sense :D

view this post on Zulip Enrico Tassi (May 13 2020 at 15:26):

Is the comment of Georges correct? Because this has an impact on point 2.

His observation is that stuff like noccurn is not exactly what you may want. Take this product forall x : nat, vector nat _. The _ is an evar that potentially sees x, eg ?e[x := x]. If you want the code to make a choice there between Prod_cs and Impl_cs (as you want in 2) then it is not clear what to choose. You could say it is the dependent space (since x occurs, this is what noccurn returns), or prune ?e saying that is cannot use x. Both are possible. Also, it may be the case a little change in the input term fixes ?e to a concrete term that does not use x. Making the choice quite fragile.

This is why I've asked if 1 would be enough: having a single AnyFunctionspace_cs for both the dependent and non-dependent space seems a way more robust behavior, but maybe it is not enough for your use cases.

view this post on Zulip Janno (May 13 2020 at 15:33):

I.. actually don't quite know. But I am beginning to understand what Georges wrote (as usual, it takes me a few months)

view this post on Zulip Janno (May 13 2020 at 15:34):

In my branch above I kept two variants just because I thought it might have a performance impact otherwise but I would prefer just having one. I can't really speak to the consequences, though.

view this post on Zulip Matthieu Sozeau (May 13 2020 at 15:39):

I'm a bit surprised it "just works" as we must be comparing terms in the wrong environment at some point

view this post on Zulip Matthieu Sozeau (May 13 2020 at 15:39):

I would prefer if the decomposition of Prod was [a; (fun x : a => b)] instead.

view this post on Zulip Matthieu Sozeau (May 13 2020 at 15:40):

And then keeping a single Prod_cs should be enough, we don't need to know about the dependency apparently.

view this post on Zulip Matthieu Sozeau (May 13 2020 at 15:41):

The noccurn test would just be an "early" optimization in this case

view this post on Zulip Janno (May 13 2020 at 15:46):

I don't suppose I can just change [a; b] to [a; mkLambda (x,a,b)], can I? (It doesn't seem to work.)

view this post on Zulip Enrico Tassi (May 13 2020 at 15:47):

My understanding is that today Coq does an noccurn and if it says "it occurs" it does not even try to look up a canonical solution. During the call Janno said that he tried to simply disable the check, but later things broke. I think we could start from that, see why they broke.

IIRC when a problem like c args = proj _ is solved by CS, then c is left as it is. In our case it would be a -> b = proj _, we may need to unify a->b with the canonical value (unlike we do the c args case, where c is left alone). This unification would prune (if needed) the evars in b

view this post on Zulip Janno (May 13 2020 at 15:47):

Never mind, I had to change it in two places. It does seem to work.

view this post on Zulip Matthieu Sozeau (May 13 2020 at 15:56):

What happens is that this [a; b] stack is compared to one coming from the left (extraargs1), at line https://github.com/coq/coq/compare/master...Janno:janno/cs_dep_fun#diff-c693614a22b8a1de52bd824f20139dbfL1128

view this post on Zulip Matthieu Sozeau (May 13 2020 at 15:57):

Well, some part of the stack, depending on o_TCOMPS. I'm wondering what value this o_TCOMPS has for product projections.

view this post on Zulip Janno (May 13 2020 at 16:01):

Sorry, I have no idea how to reply to the comments on GitHub. I see them but there is no way to do anything with them. That is one hell of a confusing interface.
@Matthieu Sozeau I re-added the line that I removed in the next commit (which, rather unhelpfully, has the same commit message).
@Enrico Tassi I have no idea how the unification algorithm works so I don't know where a and b end up..

view this post on Zulip Janno (May 13 2020 at 16:02):

Oh, sorry, got the authors mixed up. (fixed)

view this post on Zulip Matthieu Sozeau (May 13 2020 at 16:05):

Ok, I see now: we should also use [a; tLambda (na, a, b)] in pattern_of_constr in case the variable occurs in b. This is what gets compared to sk2/effective_sk2 during unification

view this post on Zulip Matthieu Sozeau (May 13 2020 at 16:07):

We could keep the special case for non-dependent products to avoid unifying things twice. Or actually always return just [tLambda (na, a, b)] uniformly

view this post on Zulip Enrico Tassi (May 13 2020 at 16:07):

I think that now I understand the code and why it needs the product to be non dependent. It sees a -> b as (pardon my OCaml), (->) a b.
But this makes sense only if b does not see a, hence the "delift" performed on b.

I guess Matthieu was already on the right track, I just could not understand it ;-) I agree with what he proposes.

view this post on Zulip Janno (May 13 2020 at 16:07):

I haven't removed the non-dependent case yet but here's the what I did with the mkLambda: https://github.com/coq/coq/commit/40f10e41df7af734bb2798a2a989f29d3c25b92d

view this post on Zulip Matthieu Sozeau (May 13 2020 at 16:08):

Cool, we all agree :)

view this post on Zulip Janno (May 13 2020 at 16:09):

I suppose two of us know what they are talking about and one (that would be me) will agree with whatever you two decide :)

view this post on Zulip Matthieu Sozeau (May 13 2020 at 16:13):

I'd be curious to try the variant where it is uniform and we just translate tProd (na, a, b) -> Prod_cs, None, [tProd (na, a, b)] actually, and do away with the special case for ->. If it benchmarks well, it would be simpler. Otherwise said I don't think it needs to deconstruct the arrow as (->) a b at all.

view this post on Zulip Janno (May 13 2020 at 16:26):

As in https://github.com/coq/coq/commit/57e8dc718cbd54ee584994f0b2be2005cd296102?

view this post on Zulip Matthieu Sozeau (May 13 2020 at 17:01):

Almost, no need to have [a at the head of the lists as the lambda domains will be compared anyway

view this post on Zulip Matthieu Sozeau (May 13 2020 at 17:02):

And I think we can just put the products instead of rebuilding lambdas

view this post on Zulip Matthieu Sozeau (May 13 2020 at 17:03):

This avoids also a decomposition.

view this post on Zulip Janno (May 13 2020 at 17:13):

Ah, now I get it. I just assumed you meant Lambda, not Prod!

view this post on Zulip Janno (May 14 2020 at 06:23):

This is the current diff: https://github.com/coq/coq/compare/master...Janno:janno/cs_dep_fun. It does seem to do the right thing, too.

view this post on Zulip Janno (May 14 2020 at 06:26):

Now, how would I go about tackling https://github.com/coq/coq/issues/11189?

view this post on Zulip Janno (May 14 2020 at 09:28):

Trying to implement this myself but I am stuck trying to determine if a term is in fact an unfolded (non-primitive) projection. Is there a function for this?

view this post on Zulip Janno (May 14 2020 at 09:44):

How do I even get the fields of a non-primitive record? Also, how do I find out if an inductive is a record?

view this post on Zulip Janno (May 14 2020 at 09:44):

I feel like there is a module that I am missing that contains all the record-related functions that I can't find

view this post on Zulip Enrico Tassi (May 14 2020 at 09:49):

No, there is no such a functionality (recognize unfolded canonical projs). Actually evarconv tries hard not to unfold canonical projections, exactly for that reason.

view this post on Zulip Enrico Tassi (May 14 2020 at 09:51):

Recordops.lookup_projections lets you get the projections of a record

view this post on Zulip Janno (May 14 2020 at 09:54):

Ah, just what I was looking for! Thanks!

view this post on Zulip Janno (May 14 2020 at 09:54):

The reason I am dealing with unfolded projections is that I am extending this match here: https://github.com/coq/coq/blob/master/pretyping/pretyping.ml#L849
It seemed like a reasonable place to add this new feature

view this post on Zulip Janno (May 14 2020 at 11:29):

As far as I can tell, check_evar_record (my only example for code relying on lookup_canonical_conversion) never introduces new evars for the arguments of the canonical structure. How does that work? My naive intuition says that to continue with unification, the arguments need to be filled by evars (or by the appropriate parameters of the record, if that's generally possible).

view this post on Zulip Cyril Cohen (May 14 2020 at 14:14):

Janno said:

This is the current diff: https://github.com/coq/coq/compare/master...Janno:janno/cs_dep_fun. It does seem to do the right thing, too.

As far as I understand, the current approach/diff does not distinguish dependent product from implications. I think this is good, since a a dependent product can become an implication by reduction, and having two distinct case in canonical instance resolution might introduce some impredictability....

view this post on Zulip Cyril Cohen (May 14 2020 at 14:17):

Now, while we are at it, could we add a Lambda key in canonical inference to have lambda abstraction behave as a key?

view this post on Zulip Janno (May 14 2020 at 14:18):

I think I thought about adding Lambda many times but I never come up with a good use case. Do you have one?

view this post on Zulip Cyril Cohen (May 14 2020 at 14:19):

Oh I have a few...

view this post on Zulip Cyril Cohen (May 14 2020 at 14:20):

e.g. functions that are canonically positive.

view this post on Zulip Janno (May 14 2020 at 14:22):

I can try to implement that, I guess. I'm stuck with the other feature anyway and I am not as intimidated by the Lambda thing. (Not yet, anyway.)
It would be great if you could give me a small test case so that I know I am working toward something that makes sense!

view this post on Zulip Cyril Cohen (May 14 2020 at 14:27):

Janno said:

It would be great if you could give me a small test case so that I know I am working toward something that makes sense!

I'll try maybe on Monday...

view this post on Zulip Janno (May 14 2020 at 14:33):

This is what I have now:

Structure cs_lambda := { cs_lambda_key : nat -> nat }.
Canonical Structure cs_lambda_func := {| cs_lambda_key := fun x => x+1 |}.
Example cs_lambda_ex0 := eq_refl : (cs_lambda_key _) = (fun x => x + 1).

view this post on Zulip Janno (May 14 2020 at 14:34):

Or, somewhat less specific:

Example cs_lambda_ex0 := eq_refl : (cs_lambda_key _) = (fun _ => _).
Print cs_lambda_ex0. (* eq_refl : cs_lambda_key cs_lambda_func = (fun H : nat => H + 1) *)

view this post on Zulip Janno (May 15 2020 at 09:19):

(Working on the documentation of CS.) This following sentence from the canonical structure docs really confuses me

Otherwise said, qualid is canonically used to extend the field cᵢ into a complete structure built on cᵢ.

Is this a typo? The equation above it really makes me think this is supposed to read "extend the field xᵢ" instead of cᵢ. But I don't really know the terminology here.

view this post on Zulip Matthieu Sozeau (May 15 2020 at 10:02):

Well, as xi and ci are convertible, one could use both, no?

view this post on Zulip Janno (May 15 2020 at 10:07):

Well, yes, because the documentation pretends that the canonical extension will only happen when we are looking for a term xᵢ _ that matches cᵢ literally. But that's not always the case, is it?

view this post on Zulip Janno (May 15 2020 at 10:08):

Okay, sure, it will only succeed if they are unifiable. But an instance might also be considered if the terms don't match perfectly (with _ -> _ projections, for example)

view this post on Zulip Janno (May 15 2020 at 10:09):

In that case we might be looking at xᵢ _ ~ nat -> nat but our instance has cᵢ := bool -> bool. How does that fit into the picture?

view this post on Zulip Janno (May 15 2020 at 10:13):

I guess the paragraph is technically correct but just very confusing for me. Maybe I simultaneously know too much about the implementation and too little about how people think about canonical structures.

view this post on Zulip Matthieu Sozeau (May 15 2020 at 10:16):

Maybe we should add, ", when ci unifies with xi _" to be clearer

view this post on Zulip Janno (May 15 2020 at 10:30):

Where exactly do you want to add this? I don't see a good place but I might be missing something.

view this post on Zulip Matthieu Sozeau (May 15 2020 at 19:23):

I would suggest rephrasing "to extend the field xi into a complete structure build on ci, when ci unifies with xi _" ?

view this post on Zulip Janno (May 19 2020 at 08:08):

Matthieu Sozeau said:

I would suggest rephrasing "to extend the field xi into a complete structure build on ci, when ci unifies with xi _" ?

Done. (Not yet pushed because I want to have other comments resolved before I push my rebased commits.)

view this post on Zulip Janno (May 19 2020 at 08:09):

Could somebody start a benchmark for https://github.com/coq/coq/pull/12349? Removing the restriction to non-dependent functions could potentially have a negative performance impact, I think.

view this post on Zulip Janno (May 19 2020 at 12:09):

Or can I start benchmarks myself? Where can I find documentation about that?

view this post on Zulip Enrico Tassi (May 19 2020 at 13:13):

go https://ci.inria.fr/coq/ and get an account

view this post on Zulip Enrico Tassi (May 19 2020 at 13:13):

(someone will have to approve your request)

view this post on Zulip Enrico Tassi (May 19 2020 at 13:14):

then pendulum > benchmark-par-of-the-branch > build-with-parameters

view this post on Zulip Enrico Tassi (May 19 2020 at 13:15):

fill in the form and click build

view this post on Zulip Janno (May 19 2020 at 13:16):

Is there a signup option? I guessed a probable url and got this:

Sign up
This is not supported in the current configuration.

view this post on Zulip Janno (May 19 2020 at 13:16):

I can't find a register/sign up link or button

view this post on Zulip Enrico Tassi (May 19 2020 at 13:17):

try from https://ci.inria.fr/

view this post on Zulip Enrico Tassi (May 19 2020 at 13:18):

(not sure, but there is a sign-up button there)

view this post on Zulip Enrico Tassi (May 19 2020 at 13:19):

then you should probably join the Coq project, which will require validation

view this post on Zulip Janno (May 19 2020 at 13:20):

Done!

view this post on Zulip Enrico Tassi (May 19 2020 at 13:25):

you should be in now

view this post on Zulip Janno (May 19 2020 at 13:26):

Cool, thanks!

view this post on Zulip Enrico Tassi (May 19 2020 at 13:27):

try to follow my instructions. Btw, you can select a smaller set of packages for the bench, eg start with the ones you are most likely to hit (math-comp, iris & co) since if you run all packages it will take a lot of time, but you can do as you prefer

view this post on Zulip Janno (May 19 2020 at 13:28):

I don't see "build-with-parameters" anywhere when clicking on "benchmark-part-of-the-branch"

view this post on Zulip Janno (May 19 2020 at 13:35):

I think I have neither "admin" nor "slave admin" permissions. Could that be a problem? (All other members have at least one of these, as far as I can tell.)

view this post on Zulip Enrico Tassi (May 19 2020 at 13:53):

did you log in again (in ci.inria.fr/coq) ? (top right corner)

view this post on Zulip Janno (May 19 2020 at 13:54):

I logged out and logged back in again but nothing changes.

view this post on Zulip Enrico Tassi (May 19 2020 at 13:55):

I made you admin (we all are), please try again

view this post on Zulip Janno (May 19 2020 at 13:56):

Yup, that fixed it!

view this post on Zulip Enrico Tassi (May 19 2020 at 13:57):

well, happy benchmarking

view this post on Zulip Janno (May 19 2020 at 13:57):

Thanks :)

view this post on Zulip Enrico Tassi (May 19 2020 at 14:19):

Oh, and 1% difference in time is typically noise

view this post on Zulip Janno (May 19 2020 at 14:20):

Hehe, I mostly ignore time measurements and cycles. I've done too much benchmarking to put any faith in N=1 time or cycle benchmarks.

view this post on Zulip Enrico Tassi (May 19 2020 at 14:22):

anyway, it is running fine... lets see

view this post on Zulip Janno (May 19 2020 at 18:00):

The benchmark results seem reasonably indistinguishable from noise. I don't have enough coffee grounds to properly interpret the results but my gut says there's a tiny tiny slowdown in coq-lambdarust. Probably not too bad, though. I'll post the results in the PR.

view this post on Zulip Janno (May 21 2020 at 13:35):

I made some progress on my next goal for improving canonical structures: https://github.com/coq/coq/pull/12383
I could use feedback on whether this is a good idea, how to best do this (my attempt is rather naive) and anything else really!

view this post on Zulip Janno (May 27 2020 at 14:20):

@Gaëtan Gilbert regarding https://github.com/coq/coq/pull/12383 and moving the app case into inh_app_fun: I see that inh_app_fun and inh_app_fun_core interact with coercions, program mode, and type classes. Should CS search be triggered before all these things? (The current state of the patch triggers it after.) I don't understand exactly how, for example, program mode interaction works here. Will the choice of what to do first impact what kind of obligations arise?

view this post on Zulip Gaëtan Gilbert (May 27 2020 at 14:31):

Your PR seems about equivalent to unifying with forall x:_, _ (but maybe a bit more efficient) so I would put it first

view this post on Zulip Janno (May 29 2020 at 11:30):

I finished moving the code for the app case to coercions.ml and that seems to work fine. I am also moving the fun code into split_tycon but now I wonder where I should move split_tycon to? I can't call Evarconv.unify from Evardefine because that yields a module dependency cycle.

view this post on Zulip Gaëtan Gilbert (May 29 2020 at 11:45):

I'd make split_tycon internal to pretyping

view this post on Zulip Janno (May 29 2020 at 11:45):

Okay, I'll do that!

view this post on Zulip Gaëtan Gilbert (May 29 2020 at 11:45):

nice response time ;)

view this post on Zulip Janno (May 29 2020 at 11:47):

Next question: I am currently checking for a Prod_cs instance to avoid unnecessary unification but I completely forgot about Default_cs. I suppose either would be reason enough to try unification?

view this post on Zulip Gaëtan Gilbert (May 29 2020 at 11:51):

I don't know how the _cs stuff works, maybe someone else does.
It may work to unify without looking up coercions (keeping the optimised version for when it"s already a product and when it's an evar)? failing paths may be slower but not necessarily by a lot

view this post on Zulip Janno (May 29 2020 at 11:54):

Hm, I don't understand what you are proposing. How do coercions figure into it? Is there an option for unification that I can/should set?

view this post on Zulip Gaëtan Gilbert (May 29 2020 at 11:57):

sorry I get confused between canonical structures and coercions (_cs sounds like coercion to me somehow)

view this post on Zulip Janno (May 29 2020 at 11:58):

Ah, I see!


Last updated: Oct 21 2021 at 22:02 UTC