Comment on the use of `Definition d := Eval hnf in [expression]`

[gallais]

My understanding is that this provides definition-time partial evaluation and that using the specialised programs is more efficient but it would be nice to see this pattern not just used but also commented upon.

[gares]

@ggonthier could you help here? I don't recall exactly why hnf is there, IIRC CS declaration does call whd to get the canonical value.

[gares]

@CohenCyril do you happe to know this?

[gares]

We could also try to remove that...

[WojciechKarpiel]

Hi! I was wondering the same thing. Do you know the answer now? The only explanation of Eval hnf in pattern I found is in the "Canonical Structures for the working Coq user" (awesome intro to Canonical Structures btw):

The “Eval hnf in” command reduces away the abstractions in the body of the packager

This is kind of what I expected it to do, but why eval to HNF specifically? In the following snipplet, the 2nd and 3rd definition seem to be equivalent:

Fixpoint fn (n: nat): nat := match n with
                               | O => 0
                               | S n => fn n 
                               end.

Definition val1 := fn 10000.
Print val1.
Eval compute in val1.
Eval compute in val1.
Eval hnf in val1.
Eval hnf in val1.

Definition val2 := Eval hnf in fn 10000.
Print val2.
Eval compute in val2.
Eval compute in val2.
Eval hnf in val2.
Eval hnf in val2.

Definition val3 := Eval compute in fn 10000.
Print val3.
Eval compute in val3.
Eval compute in val3.
Eval hnf in val3.
Eval hnf in val3.

[gares]

I don't know if this is the only reason, but in many cases we do Canonical xx := Eval hnf in [some tough inference] and the inference is supposed to generate a record, but it is probably (syntactically) more like constant _ idfun that can reduce to a hnf which is RecordConstructor fields....

So I think the idea is to avoid declaring as canonical a term which is not immediately a record but reduces to it. In some sense do the work now and not later.

[gares]

If you run compute you risk to unfold the fields which you typically don't want to unfold.