Hugo Herbelin (Dec 31 2021 at 15:22): Hugo Herbelin (Dec 31 2021 at 15:22):(About the current coq-club discussion)
It is known for probably more than 15 years that Coq tolerates fixpoints with non guarded recursive calls in erasable subterms. My perception is that this has been kept as it (including by me) because considered rather anecdotical (mostly for the reasons given by @Pierre-Marie Pédrot that non-standard reduction is in theory not needed).
It is a bit inelegant in practice though. Shouldn't we do something? Beside not being able to assume strong normalization of Coq, it also defeats the claim that we want a decidable type-checking algorithm as shown is this example:
Definition K (x y : Prop) := x.
Fixpoint Kloop (n : nat) := K True (Kloop n).
Opaque K.
Check fun x : K True (Kloop 0) => x : Kloop 0. (* stack overflow *)
Fortunately, the code checking guard is already combining checking well-foundedness with incremental reduction. So, it seems to me that there would be an easy fix:
NotEnoughArgumentsForFixCall) but not in the other cases of failures and in particular not if it is a non-guarded recursive call.What do you think?
Enrico Tassi (Dec 31 2021 at 15:41):Invest in size types?
Hugo Herbelin (Dec 31 2021 at 15:43):Sure, but this looks long term (are there some news from William?).
Karl Palmskog (Dec 31 2021 at 16:09):here I was hoping that sized types would be incorporated as an alternative way of getting explicit well-foundedness proofs "for free", not necessarily built into Coq's type checker...
Karl Palmskog (Dec 31 2021 at 16:11):with Equations and so on, should one [i.e., should general Coq users] even be using Fixpoint/fix at all?
Gaëtan Gilbert (Dec 31 2021 at 16:59):So, it seems to me that there would be an easy fix:
worth a try if easy to implement, worst case we get to see the impact on CI
Hugo Herbelin (Jan 02 2022 at 10:26):Karl Palmskog said:
here I was hoping that sized types would be incorporated as an alternative way of getting explicit well-foundedness proofs "for free", not necessarily built into Coq's type checker...
I don't know the plans so well. One advantage of sized types (in the kernel) is also modularity: one can build fixpoints depending on size properties of some parameters w/o having to be constrained to give explicit instances of the parameters.
Afaiu, sophisticated proofs of well-foundedness, even if it could clearly be extended (e.g. with recursion on many arguments) are somehow already supported by the {wf ...}/{measure ...} architecture.
Karl Palmskog (Jan 03 2022 at 08:50):well, I meant that sized types could be a more automated alternative to a specific measure specification, e.g., {sized ...}
Paolo Giarrusso (Jan 04 2022 at 19:15):They seem less automated and less flexible, and their motivating examples in Agda are all things that Coq already supports; the only advantage is properly modular typechecking, at the cost of adding sizes to your spec
Paolo Giarrusso (Jan 04 2022 at 19:21):Hm, I see https://github.com/coq/coq/wiki/CoqTerminationDiscussion#sized discusses some differences (including inference) in Sacchini's proposal...
Karl Palmskog (Jan 04 2022 at 19:22):Pros: logically simple (compositional), minimal work from users when it works
That's the kind of mechanism I'm interested in, but not necessarily built into the [default] type checker.
Paolo Giarrusso (Jan 04 2022 at 19:30):So you still need a kernel mechanism, plus an elaboration for sized types. Does the latter exists?
Karl Palmskog (Jan 04 2022 at 19:31):no idea, but why does it have to be in the kernel?
Paolo Giarrusso (Jan 04 2022 at 19:32):I'm just saying, sized types (or anthing really) must either be in the kernel or elaborate to something in-kernel
Karl Palmskog (Jan 04 2022 at 19:34):OK sure, it has to pass the kernel at some point
Paolo Giarrusso (Jan 04 2022 at 19:35):And you should hide the elaboration output from users, like when elaborating to eliminators.
Paolo Giarrusso (Jan 04 2022 at 19:37):Equations and Lean do it somewhat, but I'm not sure all source-level definitional equality remain definitional after elaboration.
Ali Caglayan (Jan 04 2022 at 20:24):There was a recent attempt to add sized typing to coq https://github.com/coq/coq/pull/12426
Ali Caglayan (Jan 04 2022 at 20:25):But the authors concluded that there were performance issues in their implementation https://arxiv.org/abs/1912.05601
Karl Palmskog (Jan 04 2022 at 20:28):sure, but this attempt was all about hacking the kernel
Paolo Giarrusso (Jan 04 2022 at 20:44):given how elegant are ordinals to formalize in type theory, I wonder if elaboration is possible at all. https://arxiv.org/pdf/1903.08233.pdf says sized types “require” extensions of the underlying type theory (tho that might be a limit of what we know already).
Karl Palmskog (Jan 04 2022 at 20:47):how do you prove that you have to extend the type theory? Seems like difficult to do. And if it turns out that all one needs is to add an axiom, that's fine by me if I get nice automation
Paolo Giarrusso (Jan 05 2022 at 00:18):as I already tried to say, I don’t mean “provably impossible”, just that we haven’t figured out a way to do it yet.
Karl Palmskog (Jan 05 2022 at 11:16):or, we haven't figured out the impossibility proof yet
Matthieu Sozeau (Jan 05 2022 at 13:46):@Hugo Herbelin I thought allowing only linear reductions would solve the issue elegantly, is it not sufficient?
Hugo Herbelin (Jan 05 2022 at 14:57):You mean forbidding any form of K-redexes in the body of a fix?
Matthieu Sozeau (Jan 06 2022 at 13:12):I mean not allowing to unfold a K-redex indeed, forcing the body to be guard-checked
Hugo Herbelin (Jan 09 2022 at 13:08):Matthieu Sozeau said:
I mean not allowing to unfold a K-redex indeed, forcing the body to be guard-checked
We can try that... though I'm unsure Equations or Program don't have patterns of the form fix aux ... := let H _ := ... in H aux ... end (which could certainly be adapted though if needed).
Hugo Herbelin (Jan 09 2022 at 13:27):In any case, whatever decision is taken, I made an experiment of strongly checking guard at #15434.
Hugo Herbelin (Jan 09 2022 at 13:28):It revealed one case of non strongly guarded fixpoint in CI (in fiat-crypto).
Matthieu Sozeau (Jan 10 2022 at 09:26):Right, the partial applications might be a problem with the strategy I proposed.
It's great to know that #15434 has only one legitimate failure in the wild !
Last updated: Jun 08 2023 at 04:01 UTC