Stream: Coq users

Topic: Primitive projection


view this post on Zulip Julin Shaji (Mar 13 2023 at 06:36):

What does primitive projections mentioned at https://coq.inria.fr/refman/language/core/records.html#primitive-projections mean?

Is it that the original constructors of the type are sort of hidden?

Could figure out an example.

view this post on Zulip Meven Lennon-Bertrand (Mar 13 2023 at 10:05):

The idea is that records with primitive projections are really defined by their projections, rather than by their constructor. If you have a primitive record Record foo := Build_foo {x : nat ; y : nat}. what "comes first" are the projections f.(x) and f.(y), and the constructor Build_foo m nreally means "construct the record uniquely characterized by itsx projection being m and y projection being n". This is dual to a non-primitive record, where the constructor "comes first" and the x projection is defined as "take the first argument of the only possible constructor for this inductive type". In categorical parlance (if that makes sense to you), a primitive record is a coalgebra (defined by its destructors), and Build_foo witnesses the fact that it is a final coalgebra, and thus also has an algebra structure. While an inductive type/non-primitive record is an algebra (defined by its constructors), and pattern-matching witnesses the fact that it is an initial algebra, and thus also has a coalgebra structure.

Thus, pattern-matching really only makes sense for inductive types which are defined by their constructors, but not for a primitive record where the constructor is an "afterthought". Although, happily, you can still encode something that looks like match in terms of the projections.

view this post on Zulip James Wood (Mar 13 2023 at 10:47):

IIRC, the most visible practical distinction is that records with primitive projections satisfy η-laws definitionally. Therefore, two records with primitive projections are definitionally equal exactly when all of their corresponding projections are definitionally equal. For example, the following is only provable (without funext) thanks to primitive projections:

Set Primitive Projections.

Record prod {A B : Type} : Type := pair { fst : A; snd : B }.
Arguments prod A B : clear implicits.
Arguments pair {A B}.

Definition swap {A B} (z : prod A B) : prod B A := pair z.(snd) z.(fst).

Definition swap_swap {A B} : (fun (z : prod A B) => swap (swap z)) = id _ := eq_refl.

Last updated: Mar 29 2024 at 08:39 UTC