Primitive projection wrapping · Coq users

According to the Coq manual, primitive projections are always applied, even if there was no explicit record defined to apply them to. Seemingly for this reason, the Interaction Trees library always wraps its primitive projection(s) in a function, which is then what is passed around. Are there any examples of what might happen when using unwrapped projections everywhere? The Interaction Trees code comments talk about that this can be confusing, but doesn't state any specifics.

CoInductive itree : Type := go { _observe : itreeF itree }.
(* .... *)
Definition observe {E R} (t : itree E R) : itree' E R := @_observe E R t.
(* observe and _observe have the same type *)

Yannick Zakowski (Feb 06 2023 at 22:19):

@Li-yao is the one that crafted that at the time, so he might have more insights! But he told me essentially of two motivations:

Paolo Giarrusso (Feb 06 2023 at 23:58):

That sounds super-surprising! Among other reasons, Karl's summary isn't quite complete, because Coq _already_ wraps primitive projections into constants.

Paolo Giarrusso (Feb 07 2023 at 00:02):

Section foo.
Context (E R : Type).
Definition itreeF (X : Type) : Type := E * R * X.
CoInductive itree : Type := go { _observe : itreeF itree }.
End foo.
(* .... *)
Definition observe := @_observe.

Paolo Giarrusso (Feb 07 2023 at 00:03):

That is, it _is_ true that the _primitive projection_ _observe cannot be partially applied. But _observe also refers to a wrapper — a _compatibility constant_.

Paolo Giarrusso (Feb 07 2023 at 00:05):

However, this wrapping was intended to be transparent, but it isn't in some corner cases, so there are plans to _drop_ these compatibility constant. When that happens, hopefully itree will mostly keep working as-is — except when those corner cases are relevant.

Karl Palmskog (Feb 07 2023 at 07:20):

but if all uses of _observe are already wrapped manually, how can Itree be affected by those corner cases when the compatibility constant disappears?

Karl Palmskog (Feb 07 2023 at 07:33):

it seems like the wrapping could then be motivated as a defense against future changes in Coq.

Yannick Zakowski (Feb 07 2023 at 09:38):

Mmmh the remark on Proper indeed seems incorrect, I must have misunderstood/be misremembering.
On the reduction side though here is a minimal illustration on the delay monad of the concern:

Set Primitive Projections.
Variant delayF (X : Type) (rec : Type) : Type :=
| NowF (x : X)
| LaterF (d : rec).
CoInductive delay X : Type := go { _observe : delayF X (delay X) }.
Arguments NowF {_ _}.
Arguments LaterF {_ _}.
Arguments _observe {_}.
Arguments go {_}.
Notation Now x := (go (NowF x)).
Notation Later t := (go (LaterF t)).

Definition subst {X Y} (k : X -> delay Y) : delay X -> delay Y :=
  cofix F (c : delay X) : delay Y :=
    match _observe c with
    | NowF x => k x
    | LaterF d => Later (F d)
    end.

Definition bind {X Y} (c : delay X) (k : X -> delay Y) := subst k c.

Definition iter {Acc Res : Type} (body : Acc -> delay (Acc + Res)) : Acc -> delay Res :=
  cofix F acc :=
    bind
      (body acc)
      (fun x =>
         match x with
         | inl acc' => Later (F acc')
         | inr res  => Now res
         end
      ).

Variable (body : nat -> delay (nat + nat)).
Variable (k : nat -> delay bool).
(* Undesired reduction behavior, the wrapping blocks it *)
Eval cbn in _observe (bind (iter body 0) k).

MackieLoeffel (Feb 07 2023 at 11:29):

Did you experiment with controlling the reduction behavior of _observe directly? E.g. via one of the following? These seem to fix at least this example.

Arguments _observe {_} !_.
Arguments _observe {_} : simpl never.

Paolo Giarrusso (Feb 07 2023 at 21:23):

Does Arguments _observe {_} !_ /. work? I avoid Arguments _observe {_} !_. like the pest because cbn and simpl interpret it differently sometimes. This time I haven't memorized the exact bug reports so I don't know if they would apply here...

Brandon Moore (Feb 07 2023 at 23:24):

In @Yannick Zakowski's example code Eval simpl in _observe (bind (iter body 0) k). doesn't over-reduce, even with any Arguments. Any of @Paolo Giarrusso's suggestions also work to make cbn leave _observe (bind (iter body 0) k) alone.

Li-yao (Feb 08 2023 at 00:32):

You can declare a Proper instance for the wrapper, but it does not let you rewrite under the unwrapped projection.

From Coq Require Import Setoid Morphisms.
Set Primitive Projections.

Record a : Type := { f : nat }.

Parameter aa : a -> a -> Prop.
Parameter nn : nat -> nat -> Prop.

#[global] Instance Proper_f : Proper (aa ==> nn) f.
Admitted.

Theorem w : forall x y : a, aa x y -> nn (f x) (f y).
Proof.
  intros x y H. rewrite H. (* fails *)

Paolo Giarrusso (Feb 08 2023 at 00:35):

I'm used to having Record a : Type := { f : nat -> nat }. #[global] Instance Proper_f a : Proper (nn ==> nn) (f a). work

Paolo Giarrusso (Feb 08 2023 at 00:37):

Paolo Giarrusso (Feb 08 2023 at 00:38):

Li-yao (Feb 08 2023 at 00:39):

Paolo Giarrusso (Feb 08 2023 at 00:39):

so you give up on the term-size advantages of prim. projections — is the only point to get eta?

Li-yao (Feb 08 2023 at 00:46):

you can write r = {| f := f r |} with the projection if you want but then the issue is that cbn will force all of your cofix.

Paolo Giarrusso (Feb 08 2023 at 00:49):

Paolo Giarrusso (Feb 08 2023 at 00:51):

Paolo Giarrusso (Feb 08 2023 at 00:52):

because always using your wrappers removes the main performance advantage of prim. projs — omitting indexes E R from the actual syntax of applications, making the real term smaller

Paolo Giarrusso (Feb 08 2023 at 00:53):

then having definitional eta-equality (not just propositional) is the only remaining upside

Li-yao (Feb 08 2023 at 00:53):

Paolo Giarrusso (Feb 08 2023 at 00:54):

Li-yao (Feb 08 2023 at 00:57):

The other part of it is to not find myself in a situation where _observe x does not match _observe x.

Li-yao (Feb 08 2023 at 00:58):

Li-yao (Feb 08 2023 at 01:02):

As another way to avoid that, we could also be forbidden from writing unapplied projections, whether by being forced to write (fun x => _observe x) or by distinguishing x.(_observe) (projection) from _observe x (wrapper).

Paolo Giarrusso (Feb 08 2023 at 01:19):

The last version is interesting... There have been plans to drop the compatibility layer, but that might be a way to preserve a reasonable amount of compatibility. But it's maybe annoying that in a sense that "defaults" to the expensive variant...

Li-yao (Feb 08 2023 at 01:28):

And another goal of itree is to hide those representation details, so I just made some maybe-more-ideological-than-practical decisions knowing that it doesn't matter at the level of abstraction I cared about.

Wojciech Kołowski (Feb 08 2023 at 13:28):

@Li-yao Rewriting with the wrapper doesn't work either (at least for your example) or I'm doing something wrong.

From Coq Require Import Setoid Morphisms.
Set Primitive Projections.

Record a : Type := { f : nat }.

Parameter aa : a -> a -> Prop.
Parameter nn : nat -> nat -> Prop.

#[global] Instance Proper_f : Proper (aa ==> nn) f.
Admitted.

Theorem w : forall x y : a, aa x y -> nn (f x) (f y).
Proof.
  intros x y H.
  Fail rewrite H.
  (* Tactic failure: Nothing to rewrite. *)
Abort.

Definition f' (x : a) : nat := f x.

#[global] Instance Proper_f' : Proper (aa ==> nn) f'.
Admitted.

Theorem w : forall x y : a, aa x y -> nn (f' x) (f' y).
Proof.
  intros x y H.
  Fail rewrite H.
  (* Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints: *)
Abort.

Can you give an example of a situation in which _observe x does not match _observe x (I guess you mean that they are not computationally equal)?

Also, is there any way other than convention to force primitive projections to be written as .(p)?

Paolo Giarrusso (Feb 08 2023 at 13:32):

probably better add Declare Instance : Equivalence aa. and Declare Instance : Equivalence nn to the test.

Stream: Coq users

Topic: Primitive projection wrapping

Karl Palmskog (Feb 06 2023 at 19:47):