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:
(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!)
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
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.
I.. actually don't quite know. But I am beginning to understand what Georges wrote (as usual, it takes me a few months)
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.
I'm a bit surprised it "just works" as we must be comparing terms in the wrong environment at some point
I would prefer if the decomposition of Prod was [a; (fun x : a => b)]
instead.
And then keeping a single Prod_cs
should be enough, we don't need to know about the dependency apparently.
The noccurn
test would just be an "early" optimization in this case
I don't suppose I can just change [a; b]
to [a; mkLambda (x,a,b)]
, can I? (It doesn't seem to work.)
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
Never mind, I had to change it in two places. It does seem to work.
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
Well, some part of the stack, depending on o_TCOMPS. I'm wondering what value this o_TCOMPS has for product projections.
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..
Oh, sorry, got the authors mixed up. (fixed)
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
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
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.
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
Cool, we all agree :)
I suppose two of us know what they are talking about and one (that would be me) will agree with whatever you two decide :)
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.
As in https://github.com/coq/coq/commit/57e8dc718cbd54ee584994f0b2be2005cd296102?
Almost, no need to have [a
at the head of the lists as the lambda domains will be compared anyway
And I think we can just put the products instead of rebuilding lambdas
This avoids also a decomposition.
Ah, now I get it. I just assumed you meant Lambda, not Prod!
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.
Now, how would I go about tackling https://github.com/coq/coq/issues/11189?
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?
How do I even get the fields of a non-primitive record? Also, how do I find out if an inductive is a record?
I feel like there is a module that I am missing that contains all the record-related functions that I can't find
No, there is no such a functionality (recognize unfolded canonical projs). Actually evarconv tries hard not to unfold canonical projections, exactly for that reason.
Recordops.lookup_projections
lets you get the projections of a record
Ah, just what I was looking for! Thanks!
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
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).
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....
Now, while we are at it, could we add a Lambda
key in canonical inference to have lambda abstraction behave as a key?
I think I thought about adding Lambda
many times but I never come up with a good use case. Do you have one?
Oh I have a few...
e.g. functions that are canonically positive.
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!
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...
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).
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) *)
(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.
Well, as xi and ci are convertible, one could use both, no?
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?
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)
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?
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.
Maybe we should add, ", when ci unifies with xi _" to be clearer
Where exactly do you want to add this? I don't see a good place but I might be missing something.
I would suggest rephrasing "to extend the field xi into a complete structure build on ci, when ci unifies with xi _" ?
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.)
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.
Or can I start benchmarks myself? Where can I find documentation about that?
go https://ci.inria.fr/coq/ and get an account
(someone will have to approve your request)
then pendulum > benchmark-par-of-the-branch > build-with-parameters
fill in the form and click build
Is there a signup option? I guessed a probable url and got this:
Sign up
This is not supported in the current configuration.
I can't find a register/sign up link or button
try from https://ci.inria.fr/
(not sure, but there is a sign-up button there)
then you should probably join the Coq project, which will require validation
Done!
you should be in now
Cool, thanks!
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
I don't see "build-with-parameters" anywhere when clicking on "benchmark-part-of-the-branch"
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.)
did you log in again (in ci.inria.fr/coq) ? (top right corner)
I logged out and logged back in again but nothing changes.
I made you admin (we all are), please try again
Yup, that fixed it!
well, happy benchmarking
Thanks :)
Oh, and 1% difference in time is typically noise
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.
anyway, it is running fine... lets see
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.
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!
@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?
Your PR seems about equivalent to unifying with forall x:_, _
(but maybe a bit more efficient) so I would put it first
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.
I'd make split_tycon internal to pretyping
Okay, I'll do that!
nice response time ;)
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?
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
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?
sorry I get confused between canonical structures and coercions (_cs sounds like coercion to me somehow)
Ah, I see!
Last updated: Oct 13 2024 at 01:02 UTC