The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT irif.fr>]

On 16/09/2017 16:39, Jasper Hugunin wrote:
> I became curious as to why the unit type can't be defined as a primitive
> record:
> ```
> Set Primitive Projections.
> 
> Record one := oo { }.
> (*
> one is defined as a non-primitive record
> The record one could not be defined as a primitive record
> [non-primitive-record,record]
> *)
> Fail Definition test_eta : (fun _ => Set) = (fun 'oo => Set) := eq_refl.
> ```
> 
> As above, it might be nice to have a judgemental eta rule for the unit type.

The problem lies in the conversion algorithm used by Coq. For efficiency
reasons, it is untyped, i.e. it compares terms without having their
types at hand. Obviously, it expects that when you ask t ≡ u, there
exists some type A such that t : A and u : A, otherwise it doesn't even
make sense.

Now, η-rules in an untyped world become tricky, because they are in
general presented in a type-directed way, e.g. for function types

Γ ⊢ t ≡ u : Πx:A.B if Γ, x : A ⊢ t x ≡ u x

The same holds for negative record types.

Luckily, reduction of the λ-calculus enjoys a few nice properties, in
particular that normal forms of terms at a given type have a specific
shape, and you can describe them using the nice decomposition into
neutral and normal terms. This is where the conversion algorithm used by
Coq becomes clever.

For instance, when asked if

λx:A.t ≡ u

then Coq knows that necessarily u has a function type Πx:A.B for some B,
so that it is legal to perform η-expansion on the fly. In practice, when
it encounters this situation where u is not an abstraction, Coq then checks

t ≡ u x

(Technically it uses de Bruijn indices, but that's a detail.)

The very same thing happens for primitive records. When asked for

t.(pᵢ) ≡ u

then the problem is transformed into

t ≡ Rec (u.(p₀), ..., u.(pₙ))

where pᵢ is the i-th projection of the Record type Rec, because Coq is
now able to infer the type of the expression t. If you apply this
algorithm, you'll observe that it actually validates the surjective
pairing definition rule for primitive records.

Unluckily, this does *not* work for zero-ary records, for a very good
reason: they don't have projections! Therefore there is no way to use
this trick.

One could think to overcome this limitation using a type-directed
algorithm, but this has been completely ruled out for efficiency reasons
based on experimental observations.

PMP