The Coq mailing list

[Jasper Hugunin <jasperh AT cs.washington.edu>]

Thanks for the explanation Pierre.

My interpretation of what you told me is that the problem arises because, with eta for unit, any t u : unit should be convertible. (Let tt be the constructor of unit)

If you are checking t ≡ tt, you can still expand t into tt applied to zero parameters, and the conversion check works. But assuming you want your judgemental equality to be an equivalence relation, you then have t ≡ u by transitivity, and the constructor tt has disappeared. That happens because there is no projection recording where the tt came from (It's not tt t.(p0) or some such).

I don't think your primitive record example quite works; I would hope that when checking

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

u gets expanded so we have

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

That seems to more closely match the function version, where we have the constructor form on the left and u on the right, where u then gets expanded into constructor form (and then the internal terms are compared because the heads match).

The way you have it, it sounds like whenever we want one projection of t to agree with the record u, we need all of t to agree with the eta expansion of u, which doesn't make sense.

Thank you for explaining this to me; I think I have a better understanding of where the generalization fails now.

- Jasper Hugunin

On Sat, Sep 16, 2017 at 9:04 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT irif.fr> wrote:

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