The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

Hi folks

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

Jason Hickey:
> > Seriously though, I'm curious why Coq does not admit function
> > extensionality.  The PRL (Martin-Lof-style) type theories are carefully
> > intensional with two exceptions--the function type is fully extensional,
> > and the quotient type is partially extensional.
> >
> > [...]
> >
> > But, let me throw down the guantlet.  Why are the Coq folks so backward
> > as to refuse function extensionality?  If there are technical reasons,
> > why not be clear about it, and define a standard theory extension for
> > people who care about reasoning, not complexity?

> Presumably extensionality would break strong normalization?  And without
> strong normalization doesn't (dependant) type-checking break?  I think
> this is a case, but I am not an expert on these things.

I wouldn't presume to speak for 'Coq folks', but I am reasonably
well-informed about the technical issues, so let me try to be helpful, whilst
concealing as best I can (ie probably not so well) my personal prejudices.

We've already had the observation that just adding the extensionality axiom
to Coq is consistent. Some people may dislike extensionality because it
identifies different implementations with the same specification. But as
things stand, these differences are not observable within the type theory,
hence perhaps there is no obligation to believe in them.

I'd therefore suggest that the argument against extensionality in the Coq FAQ
requires more cautious elaboration. It is perhaps worth being careful to
distinguish observations which the theory can make (functions-to-bool, if you
like) and observations which its implementation can make. Which of these
should 'propositional equality' capture?

Of course, one can also imagine even more intensional type theories which
permit sufficient observations on functions as to be incompatible with the
extensionality axiom.

Russell O'Connor:
> Presumably extensionality would break strong normalization?  And without
> strong normalization doesn't (dependant) type-checking break?  I think
> this is a case, but I am not an expert on these things.

Extensionality, added as an axiom, doesn't break SN. As I've said, it
breaks the property that values in the empty context are canonical, basically
gumming up the computational behaviour of terms with substs which won't go
away. Lovely reflective things won't behave so nicely; you might find it
hard work to prove that true isn't (subst (ext ...) .... false). On the other
hand, if you don't want to run these terms inside the system, then it's no
big deal. Moreover, I don't see why the extracted programs shouldn't just
treat all substs as the identity: does anyone know if that's a problem?

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)

In this situtation, if you want to prove

  (forall x. f x = g x) -> (lambda x. f x) = (lambda x. g x)

then the proof is just

  lambda q. refl

because we have, judgmentally

  q : forall x. f x = g x; x |- f x === g x

by equality reflection on the proof (q x).

Equality reflection is a marvellous, generous friend! But what's the price?

(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

    Check it for yourself! Under a false hypothesis, intensional type theory
    can prove anything, but you can still execute the proofs safely, because
    they're neutral. With equality reflection, this kind of computation
    becomes dangerous. Correspondingly, be very careful when normalizing a
    type to see if it's functional, and other everyday stuff like that.

(2) a term is a suspicion, not a proof

    In intensional type theory, humans must provide the thing left of : as
    evidence of type inhabitation, but the machine can check judgmental
    equality for itself. This clean separation of what machines do and
    what people do is one of the main selling points. You can see the
    'two-level approach' of reflective theorem proving as shifting work from
    inhabitation to equality, hence from human to machine. (I'm so
    impartial...)

    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. Indeed, as a form of
    extensionality holds, this requires the machine to check whether
    functions are extensionally equal. Fortunately for the lot of us,
    machines just aren't that clever. Correspondingly, machines can't
    just typecheck terms. Terms are no longer the evidence of type
    inhabitation, hence cannot reasonably be called 'proof objects'. The
    real proof objects are the whole derivations, including both
    inhabitation and equality steps.

I'm fairly ignorant of the PRL type theories having grown up on the other
side of the wall/ocean/whatever. 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
?

My understanding is that extensional type theory has properties (a) and (b)
but not (c) and (d). Are the PRL type theories intensional enough to have
the latter as well? Do they have equality reflection, or something more
subtle?

Coq has (b), (c) and (d) if you don't add axiomatic extensionality and (a),
(c) and (d) if you do.

I hope I've been suitably informative, and I'm sure that if I've been unfair
or otherwise ignorant, then I'll be rapidly set straight.

Cheers

Conor

--
http://www.cs.nott.ac.uk/~ctm

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.