Stream: Coq devs & plugin devs

Topic: Fixpoint values in the VM

Pierre-Marie Pédrot (Oct 13 2022 at 15:03):

I am trying to wrap my head around the implementation of (co)fixpoints in the VM and native, because the machines do not compute the same normal forms.

Pierre-Marie Pédrot (Oct 13 2022 at 15:03):

(Background: trying to share the reification of both machines)

Pierre-Marie Pédrot (Oct 13 2022 at 15:04):

It turns out that the VM has a dedicate node Vfix for non-neutral fixpoints, while the native has not.

Pierre-Marie Pédrot (Oct 13 2022 at 15:04):

As a result, native compilation always eta-expands a fixpoint, but the VM doesn't.

Pierre-Marie Pédrot (Oct 13 2022 at 15:05):

Fixpoint dummy (n : nat) := match n with 0 => tt | S n => dummy n end.

Eval native_compute in dummy.
(*
     = fun n : nat =>
       (fix Ffix (n0 : nat) : unit := match n0 with
                                      | 0 => tt
                                      | S x => Ffix x
                                      end) n
     : nat -> unit
*)
Eval vm_compute in dummy.
(*
     = fix Ffix (x : nat) : unit := match x with
                                    | 0 => tt
                                    | S x0 => Ffix x0
                                    end
     : nat -> unit
*)

Pierre-Marie Pédrot (Oct 13 2022 at 15:05):

I understand that the VM was implemented at a point in time where eta-expansion was not allowed by the kernel.

Pierre-Marie Pédrot (Oct 13 2022 at 15:06):

Since we are past this point, shouldn't we make the VM and native behave the same and always eta-expand?

Pierre-Marie Pédrot (Oct 13 2022 at 15:07):

The way we handle Vfix in the VM is not pretty, and I wouldn't be surprised if we could exploit it with weird fixpoints.

Guillaume Melquiond (Oct 13 2022 at 15:07):

Shouldn't it be to always eta-reduce instead? Currently, vm_compute and compute agree. It would be best that native_compute would agree with compute too rather than the opposite.

Pierre-Marie Pédrot (Oct 13 2022 at 15:08):

Eta-reduction is not always valid, though.

Pierre-Marie Pédrot (Oct 13 2022 at 15:08):

(mumble mumble cumulativity on domains of arrow is invariant)

Pierre-Marie Pédrot (Oct 13 2022 at 15:08):

Your off-the-shelf NbE always eta-expand functions, BTW.

Guillaume Melquiond (Oct 13 2022 at 15:08):

Sure. But, at the very least, not to do spurious eta-expansions.

Pierre-Marie Pédrot (Oct 13 2022 at 15:09):

How do you know that without retyping?

Guillaume Melquiond (Oct 13 2022 at 15:18):

But for fixpoints, you should not have to do any retyping. If you are strongly reducing a non-reducing fixpoint (i.e., just substituting the up-variables), then you know that the n first eta-expansions (with n the position of the main argument) are spurious.

Pierre-Marie Pédrot (Oct 13 2022 at 15:19):

I'm pretty sure this is not true, let me find a counter example.

Pierre-Marie Pédrot (Oct 13 2022 at 15:30):

(I just discovered that Coq has the brilliant idea to eta-expand in pretyping when it detects a cumulativity issue. This is troubling to say the least.)

Maxime Dénès (Oct 13 2022 at 15:31):

Yeah I remember discovering this too.

Pierre-Marie Pédrot (Oct 13 2022 at 15:32):

It took me at least one minute to find out why and refrain from looking for an inconsistency

Maxime Dénès (Oct 13 2022 at 15:32):

I found a fake proof of false like this once.

Pierre-Marie Pédrot (Oct 13 2022 at 15:32):

so, the example breaking @Guillaume Melquiond claim:

Universes i j.
Constraint i < j.

Axiom K : Type@{j} -> unit.

Fixpoint F (n : nat) (A : Type@{j}) := match n with
| 0 => K A
| S n => F n A
end.

Check (F : nat -> Type@{i} -> unit). (* Actually gets eta-expanded *)
Check (F : nat -> Type@{j} -> unit).
Check (fun (n : nat) (A : Type@{i}) => F n A).

Pierre-Marie Pédrot (Oct 13 2022 at 15:32):

just a variant of the usual expansion trick

Maxime Dénès (Oct 13 2022 at 15:32):

In the end, it was not a paradox, just the definition wasn't what I had expected once gone through pretyping.

Pierre-Marie Pédrot (Oct 13 2022 at 15:33):

Pollack inconsistency at its finest

Pierre-Marie Pédrot (Oct 13 2022 at 15:34):

so anyways: assuming we merge Vfix into Vfun, now we get an expanded fixpoint value in the VM

Pierre-Marie Pédrot (Oct 13 2022 at 15:34):

we cannot decide to reduce because it would make the term ill-typed

Pierre-Marie Pédrot (Oct 13 2022 at 15:35):

so at the very least we need a conversion check with the argument types of the fixpoint

Pierre-Marie Pédrot (Oct 13 2022 at 15:35):

this looks expensive to me

Gaëtan Gilbert (Oct 13 2022 at 15:36):

so don't merge vfix

Pierre-Marie Pédrot (Oct 13 2022 at 15:36):

(Relatedly, now that I have some eyes, anybody looking at https://github.com/coq/coq/pull/16651 ? That's a soundness issue)

Pierre-Marie Pédrot (Oct 13 2022 at 15:37):

@Gaëtan Gilbert this is a hack to support a broken eta, and it makes native different from VM

Pierre-Marie Pédrot (Oct 13 2022 at 15:37):

I think that what NbE taught me is that functions are functions, and that's it.

Pierre-Marie Pédrot (Oct 13 2022 at 15:37):

We shouldn't have a different class of values for some function types

Pierre-Marie Pédrot (Oct 13 2022 at 15:40):

also the code is making some hypotheses about the shape of closures

Pierre-Marie Pédrot (Oct 13 2022 at 15:40):

value coq_kind_of_closure(value v) {
  opcode_t * c;
  int is_app = 0;
  c = Code_val(v);
  if (Is_instruction(c, GRAB)) return Val_int(0);
  if (Is_instruction(c, RESTART)) {is_app = 1; c++;}
  if (Is_instruction(c, GRABREC)) return Val_int(1+is_app);
  if (Is_instruction(c, MAKEACCU)) return Val_int(3);
  return Val_int(0);
}

Pierre-Marie Pédrot (Oct 13 2022 at 15:41):

can't we break that with, say, primitive functions?

Guillaume Melquiond (Oct 13 2022 at 15:48):

I must be missing something, because I do not understand why it breaks my claim.My claim is that the machines do not have to eta-expand F to normalize it. The fact that the pretyper eta-expanded it first does not seem relevant.

Guillaume Melquiond (Oct 13 2022 at 15:51):

Pierre-Marie Pédrot said:

We shouldn't have a different class of values for some function types

We certainly should, because the reduction rule for fixpoints is completely different from the one for functions. In particular, no substitution happens until some very specific constraints have been fulfilled.

Pierre-Marie Pédrot (Oct 13 2022 at 15:51):

Fair enough, but then (barring potential soundness issues) we shouldn't have native behave differently

Gaëtan Gilbert (Oct 13 2022 at 15:53):

so change native

Pierre-Marie Pédrot (Oct 13 2022 at 15:55):

I am still unconvinced by @Guillaume Melquiond 's argument. Special-casing fixpoints is evil, and we already had issues with parametricity because of that.

Guillaume Melquiond (Oct 13 2022 at 15:56):

Pierre-Marie Pédrot said:

can't we break that with, say, primitive functions?

I don't think so. It has the unfortunate effect that primitive functions will be naturally eta-expanded, but that is about it.

Guillaume Melquiond (Oct 13 2022 at 16:10):

Okay, I now understand better why you complain. The fixpoint has already been eta-expanded before being sent to the OCaml compiler the first time. So, when we recover it after NbE (and before strong normalization), we have no way to know whether this eta-expansion was spuriously introduced by the native compiler or it was already there in the first place for typing reasons.

Last updated: Oct 08 2024 at 15:02 UTC