The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Stefan

On 28 Aug 2008, at 02:41, Stefan Monnier wrote:

> > PS One day, not far away, it will be possible to ensure that
> > eq_rect commutes with constructors even in the *definitional*
> > equality. We know how to implement it, but we have yet to
> > persuade people to believe it.
>
> It sounds very interesting.  Could you (in private or on the
> mailing-list) give some details or point to some article?

When I say "we have yet to persuade", "we" are the usual
Nottingham (or in my case, Strathclyde) suspects and the onus is
on us to get our acts together, rather than on others to be more
than usually credulous.

The current best source for this stuff is our PLPV paper

  Observational Equality, Now!
  Thorsten Altenkirch, Conor McBride, Wouter Swierstra
  http://www.strictlypositive.org/obseqnow.pdf

in which we showed, for the weakest nontrivial dependent type
theory we could think of --- large elimination for Bool alone
--- how to carve out a propositional subtheory which allows us
to deliver a propositional equality with some quite good properties

  1 coercion (our analogue of eq_rect) commutes with constructors
  2 closed expressions have canonical values (a property preserved
      by consistent extension with propositional axioms)
  3 extensionality for functions holds
  4 proof irrelevance holds definitionally
  5 coercion by reflexivity is the identity

1, 2, 3 is a chain of consequences: make coercion (transportation
between provably equal types) compute under constructors instead
of inspecting the proof and it's easy to ensure that you get
canonical values regardless of the proofs, hence adding consistent
axioms is ok, hence extensionality is ok. In CIC as we know it,
adding ext is consistent, but it messes up evaluation exactly
because eq_rect and friends do not commute with constructors.

We presented an inductive-recursive model of this theory in Agda 2,

  http://sneezy.cs.nott.ac.uk/darcs/JOTT/agda/ObsEq.agda

in which 1, 2, 3 hold, and we showed how to get 4 and 5 in
principle, by using type information to liberalize the equivalence
of normal forms.

(Please note that you can't get proof irrelevance definitionally
by decree: you have to change the computational behaviour of every
operator which currently matches for reflexivity to do something
more subtle. A lession I learned the hard way was that proof
irrelevance for intensional equality is rather tricky, but when
you do what you need to get extensionality, proof irrelevance
kind of happens by accident.)

I have since translated the Agda construction to Coq

  http://sneezy.cs.nott.ac.uk/darcs/JOTT/coq/ott.v

which gives us stronger evidence that evaluation terminates.

Meanwhile, there's a prototype implementation buried in the
source repo of Epigram 2. Perhaps, in the future, someone will
have time to do some more work on it and help it to see the
light of day.

But we are working on a new paper, where we hope to flesh out
in detail why

  * every derivable typing in Extensional Type Theory can be made
      a typable term in OTT by coding equality reflection as
      appeals to the propositional equality (this is basically
      the result in Nicolas Oury's thesis)
  * OTT preserves the typing and equality judgments of
      Intensional Type Theory (once we get all the way to 5;
      actually, we get the potential for a much richer
      definitional equality)
  * OTT is decidable

There's a longer term agenda which needs more work, including
at least

  * adding quotients as a neater alternative to those uses of
      setoids which are still needed once equality is extensional
  * equipping coinductive structures with the language of evidence
      required to justify strong finality (the source of recent
      consternation in both Coq and Agda 2)

We think it's really exciting, and we'd like to hope that in
time, it'll get taken up by our comrades. Of course, we have to
make this story more intelligible and credible before that
can happen, but we're working on it as fast as busy people can.

All the best

Conor