Hi Robin
Robin Green wrote:
Hi Thorsten,
Thanks very much for your explanation - that was very helpful.
Here is what I have written so far about OTT for my MRes literature
review; please let me know if you see anything wrong. As I'm new to
this, there probably is.
A couple of small points seem relevant.
[..]
-------
Observational Type Theory[McBrideOTT] is a theory under development -
which the authors aim to implement in Epigram 2 - which tries to make
reasoning with propositional extensional equality more convenient. Like
NuPRL, it has a general theory of equality in types, involving not just
function types but sums, products, etc. Also, as in NuPRL, equality is
recursive in the sense that equality on compound types, such as
function types and \Sigma -types, is defined in terms of the equality
on (and pairwise equality _of_) their constituent types.
It might be worth mentioning the ways in which it's unlike NuPRL. In the
spirit of intensional type theories, all the evidence is present in
terms. A key objective (we have a prototype, but we haven't done all the
math) is that typechecking terms (as opposed to checking derivation
trees built arbitrarily from the rules) should be decidable.
The basic idea of OTT is that equality should be _observational_: we
should not be able to make observations (apart from time/space usage
observations) which tell two equal terms apart. That is to say, all
eliminators must respect the equality on the types they eliminate -
that is sufficient, because we cannot observe values other than via
eliminators (function application is an eliminator).
I'd rather spin it the other way. It's basically Leibniz's intuition:
two things should be equal if every property (expressible within the
theory) which holds for one also holds for the other. Somehow, the
"observations" come first. When we're defining what "observational
equality" means for a given type-former, we're obliged to consider all
the eliminators for that type-former and collect all the guarantees
about the elements that we need if those eliminators are to preserve
equality. That's a general approach which we can (and will) take with us
to systems other than Pi, Sigma, W, 0, 1, 2.
For quotient
types, this means that if we create a quotient type T/R and name it Q,
we need to somehow canonicalise values of T that are equivalent under R
to equal values - for example, values in Integer/(\lambda
x,y\rightarrow(x=y)\bmod2) could be canonicalised to 0 or 1. This could
be done either upon construction - so that the carrier of Q is the set
of canonical values - or upon elimination, so that the carrier of Q is
T. In a referentially-transparent language, the latter is not
necessarily inefficient, because we can memoise the results of the
elimination.
Quotient types don't (won't? shouldn't? can't?) rely on a notion
(effective or otherwise) of canonical form, although it's always nice if
you can get one. I'm planning to implement quotients as a class of
abstract datatypes, with
A:*; ~:A->A->*; Q:EqRel A ~
-------------------------------
Quot A (~) Q : *
a : A
----------------------
[a] : Quot A (~) Q
x : Quot A (~) Q
P : Quot A (~) Q -> *
p : Pi a:A. P [a]
q : Pi a,a':A. a ~ a' -> (p a : P [a]) = (p a' : P [a'])
------------------------------------------------------------
expose x P p q : P x
That's to say, access to the element of the carrier is a privilege which
comes with the explicit responsibility to respect the equivalence. We're
correspondingly entitled to consider [a],[a'] : Quot A (~) Q to be
observationally equal if a ~ a'. Jacking that up to a heterogeneous
definition is a bit annoying but not problematic. (When is one class in
one quotient equal to another class in another quotient? When the
quotients are equal and the representatives are equivalent!)
An interesting question is what the definitional equality should do with
quotients, although an acceptable minimum is to reduce to the
definitional equalty on the carrier.
What has happened here? We've relocated the proof obligation that you
have when defining setoid functions, however trivial, to the place where
the work is really needed.
[..]
It seems that OTT with quotient types will be enough to model anything
- we can define any data type or computation, with any equivalence
relations we like; we don't need anything else. In particular, we don't
need the fiddly setoid model commonly used in ITT. Having personally
tried to formalise category theory using setoids in Haskell, I can
testify that it is a pain, so I look forward to trying OTT.
Depending on your capacity for enduring primitive conditions, this may
be possible quite soon...
However, establishing that OTT has certain important metatheoretical
properties such as normalisation is future work.
There's been quite a lot of progress since that paper. Wouter's Agda
development shows that the structural coercion mechanism is normalising
(if induction-recursion is normalising). Moreover, the weird "s [Q:S =
T> == s if S == T" rule doesn't seem to mess things up as badly as I had
feared. In particular, it now looks like we don't need to use it in
evaluation, just in deciding the conversion of neutral terms.
Intuitively, an identity coercion can only inhibit evaluation if it is
hiding a canonical constructor of a canonical type from something which
would otherwise consume it, but under those circumstances, the
structural rules push the coercion under the constructor anyway. Both
the implementation and the metatheory are looking a lot simpler than
they did a year ago.
All the best
Conor
