The Coq mailing list

[Jason Hickey <jyh AT cs.caltech.edu>]

Thanks Conor for a most comprehensive answer!

Conor McBride wrote:
> I grew up in a religious warzone where the first thing we learned was:
> whatever you say, say nothing.

And I should be more polite in my challenges:)  Coq is really very 
carefully designed.

> We should be careful to distinguish extensionality as an axiom, from the
> thing which makes 'extensional type theory' extensional: the equality
> reflection rule. Equality reflection says that two provably equal things
> become definitionally equal.
>
>    Gamma |- q : x =_T y          (q proves proposition 'x equals y in T')
>  ------------------------
>    Gamma |- x === y : T          (x judgmentally equal to y in T)

It is such a wonderfully strong principle, but the price is so high!  In 
one broad stroke, equality reflection requires the non-observability of
extensionally equal values in all contexts.  One compromise we use is to
assume that equality reflection only holds on types where the elements
have canonical representatives.  This includes only unit, bool, int, and
sums and products of those types.

As your examples show, one real cost of extensionality regards the
interpretation of judgments.  What do we mean by the following judgment?

   f : A -> B, q : P1 |- P2

For the judgment to be well-formed, P1 must be functional with respect
to f, and P2 must be functional with respect to f and q.  Clearly, the
finer the equality on (A -> B), the easier this is to show.  The
semantics of PRL judgments is complicated for this reason.

> (1) there are such liars in the world, such cheats
>
>     Q : nat = (nat -> nat) |- (lambda x : nat. x x) (lambda x : nat. x x)
>                               : nat

I see, and with an empty context and intensional function equality, this
can't arise.  To spell it out, in extensional type theory, if we assume
void is an empty type, then the following holds for fairly arbitrary
formulas e1 and e2.  In fact, termination wouldn't really matter, since
these functions can never be applied.

   |- (lambda x : void. e1) = (lambda x : void. e2)

>     If you look at the equality reflection rule, you'll see that it makes
>     checking the equality judgment impossible: it requires dreaming up
>     the proof q which makes the premise hold.

Another good point!

> Jason, have you guys cracked it? Have
> you got a system where
>   (a) extensionality holds propositionally
>   (b) values in the empty context are canonical
>   (c) the judgmental equality is decidable, hence so is typechecking
>   (d) symbolic evaluation under false hypotheses terminates

This may seem surprising, but in the PRL theories, only (a) holds.  In
PRL, computation is defined on untyped terms and is treated
definitionally.  The following fact is true:

   Gamma |- 0 : nat

The following fact is identical.

   Gamma |- ((lambda x. 0) omega) : nat
where
   omega = (lambda x. x x) (lambda x. x x)

So:
   (b) values can never be assumed to be canonical
   (c) proof terms are usually only weakly normalizing,
       equality and typechecking are undecidable in general
   (d) symbolic evaluation does not terminate in general

       The extreme example uses the intersection type
       Top === (isect x : void. void), which contains all terms,
       including non-terminating ones, and all elements of
       Top are equal.

You might be aghast by this, but the practical consequences are not so bad.

   1. Type checking becomes a proof obligation.
      Usually (but not always), these proof obligations
      are easily proved automatically.
   2. Proof checking requires checking the entire derivation.
      Its still decidable, but more complicated than a type
      checking problem.

In return, the PRL type theory is expressive, with things like 
extensional function equality, quotient types, very-dependent function 
types, intersections, etc.

The rule for substitution might help illustrate the functionality issue. 
 In the following rule, one must show that C[x] is functional with 
respect to type T.

   Gamma |- e1 = e2 : T
   Gamma, x : T |- C[x] : Type  (* functionality *)
   Gamma |- C[e2]
   ------------------------------------------------
   Gamma |- C[e1]

The Coq theory gains a lot from nice properties like SN, decidable type 
checking, canonical values, and more.  It would be unfortunate if these 
properties were compromised by extensional function equality--and 
probably not worth adding if so.

Jason

--
Jason Hickey                  http://www.cs.caltech.edu/~jyh
Caltech Computer Science      Tel: 626-395-6568 FAX: 626-792-4257