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.

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 n`

really means "*construct the record uniquely characterized by its x 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 "`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.

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: Oct 04 2023 at 21:01 UTC