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. (In a previous section I looked at extensional type theory, so the comments on that are found in that section, which is why you don't see them below.) ------- 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. 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). 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. We cannot "strongly canonicalise" functions, in the sense of taking all extensionally equal functions to intensionally equal ones, because extensional equality of functions is undecidable. Fortunately, that doesn't matter! Extensional functional equality is observational by definition in OTT, so we don't need to use canonicalisation, or even quotient types at all, to model extensional functional equality. 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. However, establishing that OTT has certain important metatheoretical properties such as normalisation is future work. ------- -- Robin On Mon, 29 Jan 2007 20:26:56 +0000 Thorsten Altenkirch <[EMAIL PROTECTED]> wrote: > In Intensional Type Theory one uses setoids to simulate extensional > reasoning, a setoid is a type together with an equivalence relation > (i.e. you can form the large type SETOID): > > A : * > ~_AA : A -> A -> * > eqR_A : EquivRel ~ > --------------------------------- > (A,~_A,eqR_A) : SETOID > > where EquivRel is formalizes that ~ is an equivalence relation. > Given setoids AA=(A,~A,eqR_A) and BB = (B,~B,eqR_B) we can form a > new setoid AA => BB where the underlying set is given as > > A=>B = Sigma f : A->B . Pi a,b:A.(a ~A b) -> f a ~ f b > > and the equivalence relation > > (f,_) ~A=>B (g,_) = Pi a:A.f a ~B g a > > and I leave it as an exercise to show that this is an equivalence > relation. Clearly, we can use A => B as if it were the function > space and ~ as if it were the propositional equality on the function > type. However, each time we want to substitute an extensionally > equal function by another one, we still have to prove that our > predicate preserves the setoid equality. This seems unnessessary > because we know that all predicates we can define preserve > extensional equality. > > In a different way this also applies to quotient types. While in > general not all function preserve the equality we quotient by, we > can introduce an elimination operator for quotients which requires us > to show that the operation preserves the equality. If this is the > only way we ever use quotient types we also know that any predicate > will preserve the equality. > > E.g. if we want to formalize category theory we would like to define > a category simply as a structure: > > Obj : * > Hom : Obj -> Obj -> * > id : Pi A:Obj.Hom A A > comp : Pi A,B,C:Hom B C -> Hom A B -> Hom A c > eqL : Pi A,B:*;f:Hom A B.comp f (id A) = f > ... > > However, we want be able to construct many categories this way, > because the equality we want to use may not be the propositional > equality of Intensional Type Theory. E.g. if we formalize the > category of groups a morphism is a function on the underlying sets > which commutes with the group structure. Hence for two morphisms to > be equal requires to show that they use the same proof that the > function commutes with the group structure!? > > Hence we certainly should introduce a setoid of Homsets. Some people > have suggested that this is sufficent, however, in this setting it > is not clear how to perform certain constructions which turn homsets > into objects, such as the construction of the arrow category > (objects are morphisms, morphisms are commuting squares). It would > be consequent to use a setoid to model objects as well. Fine, > however, we now have to make precise that homsets are a family of > setoids indexed by a setoid. In particular we have to provide a > family of isomorphisms which assigns to equal objects an isomorphism > of homesets... > > All this can be done, but it seems that we are reinventing Type > Theory on the level of setoids. An indeed this basically the idea of > OTT: to use a model construction to interpret all constructions of > Type Theory as taking place in the setoid interpretation. The > advantage is that you can use the setoid equality in the model in > the same way as you use propositional equality in ordinary Type > Theory. I.e. we use the relation ~A=>B as defined above but we never > have to show that our predicates respect this relation because this > is part of our model construction (or more exactly part of our > defintion what it means to be a predicate over A=>B). In the category > theory example we can just use the naive formalisation, but since we > can use arbitrary quotients we get all the categories we are > interested in. > > So to summarize: OTT can be viewed as a convenient interface to use > setoids without having to realize all the underlying machinery. It's > goal is to have an extensional propositional equality but to retain > decidability and canonicity.
