The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT loria.fr>]

On Mon, 14 Feb 2005, Jason Hickey wrote:

> Conor McBride wrote:
>
> > 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.
> [...]
> 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.

in a recent work (see http://www.loria.fr/~blanqui/papers/shostak.pdf), we 
study a restricted form of equality reflection that preserves all these good 
properties in the calculus of constructions. we restrict equality reflection 
to the judgements (x =_T y) that are provable, in the first-order theory of 
equality, from the algebraic equalities assumed in Gamma. this is decidable. 
we expect to extend this to richer theories.