Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch

Hi Bas,

thank you - indeed this is a very interesting observation. This was  
the proof I had in mind when I first claimed that the axiom of choice  
is provable in OTT. However, I was deluded in believing that OTT/ 
predicative topoi exactly characterize the theory of the setoid  
model. As you clearly point out this is not the case. To me this is  
an incompleteness of the formal system (OTT/predicative topoi) wrt  
the intended interpretation. This should be fixable, leading to OTT+X  
or predicative topoi + X which should be complete wrt the setoid  
model. More categorically we could say that X characterizes the  
predicative topoi obtained by an exact completion of an LCCC - I think.


Indeed, in the setoid model we can construct a function

f : A - [B]
--
lift f : [A - B]

if the setoid A is trivial, i.e. has the identity as its  
equivalence relation. The construction is exactly the one you point  
out  it actually corresponds to my previous informal explanation why  
this is not unreasonable:


Note that this is not completely unreasonable: we observe the  
hidden choice made by f, but we compensate by this by hiding our  
knowledge.


Which setoids have a trivial equality? Certainly all first order  
types. However, if we start with an extensional theory (which can be  
justified with the setoid model) than also higher types N - N have a  
trivial equality (indeed the extensional equality here is the  
finest equality). Hence we certainly get considerable more than  
countable choice.


Actually, instead of using only [..] we can formulate a more general  
operator for quotient types, given an equivalence relation ~ : B - B  
- Prop, we define ~' : (A - B) - (A-B)-Prop as f ~' g = forall  
a:A.f a ~ g a. We obtain the following generalisation:


f : A - B/~
-
lift f : (A - B)/~'

But hang on - what stops us from doing a Diaconescu? Excluded middle  
doesn't hold in the setoid model, even though we only get P \/ not P  
where A \/ B = [A + B].  But this would still require that we have P  
+ not P in the underlying set. So what goes wrong?


We define the type of non-empty subsets of Bool as

NE = Sigma Q : Bool- Prop.Sigma x:Bool.Q x

We define the equivalence relation of extensional equality of subsets

~ : NE - NE - Prop

(Q,_) ~ (R,_) = forall b:Bool.Q b - R b

Now we derive:

h : NE/~ - [ NE ]

which is just the indentity on the underlying elements. The point is  
that obviously ~ implies the trivial equality of [..].


Now, if we were able to lift h we get

lift h : [ NE/~ - NE]

Obviously, NE/~ isn't a setoid with a trivial equality!

The Diaconescu argument shows that we can prove for any P:Prop

H : NE/~ - NE
--
Dia H : P \/ not P = [P + not P]

and combining the two using bind we get

(lift h) = Dia : P \/ not P

see below for a Epigram 2+n style proof of Dia.

We can also see what goes wrong in general: The principle

f : A - B/~
-
lift f : (A - B)/~'

fails because given the setoid A = (A0,~A) the premise gives us an  
underlying function f0:A0 - B (for simplicity we assume that B is  
trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same  
function to construct an element of  A - B we need to show that  a  
~A b implies f0 a = f0 b, and there is no reason to believe this -  
unless ~A is the equality.


The main question is how to characterize abstractly the types A for  
which lift is valid. Syntactically we could say All types not  
containing quotients but this is not very nice. I'd like a semantic  
condition for the type.


Cheers,
Thorsten

P.S.
For completeness: Dia itself can be constructed as in the COQ script:  
we use


T,F : Bool - Prop

T b = (b=true) \/ P
F b = (b=false) \/ P

by applying H to the equivalence classe T,F and projecting out  
the components we get


t,f : Bool
t = fst (H T)
f = fst (H F)
snd (H T) : t=true \/ P
snd (H F) : f=false \/ P

By analyzing the cases of the propositional components we get two  
cases in which we can prove P (hence we are done with P \/ not P) and  
one where we have


t=true
f=false

In this case we can prove not P: we assume p:P and using this we can  
prove T b, F b for any b and hence T b - F b and therefore  
T=F but then t=f and true=false and we have derived a contradiction.


On 1 Feb 2007, at 03:10, Bas Spitters wrote:


Hi Thorsten and others,

On Tuesday 30 January 2007 21:22:53 [EMAIL PROTECTED] wrote:
I do indeed think that Observational Type Theory with quotient  
types should
be the language of a Predicative Topos. I don't see in the moment  
that the
setoid model would introduce anything which isn't provable in the  
Type
Theory and at least in the moment I don't see how to prove the  
countable

axiom of choice in OTT. Bas, could you 

Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Bas Spitters
Hi Thorsten,

On Thursday 01 February 2007 08:55:30 Thorsten Altenkirch wrote:
 thank you - indeed this is a very interesting observation. This was
 the proof I had in mind when I first claimed that the axiom of choice
 is provable in OTT. However, I was deluded in believing that OTT/
 predicative topoi exactly characterize the theory of the setoid
 model. As you clearly point out this is not the case. To me this is
 an incompleteness of the formal system (OTT/predicative topoi) wrt
 the intended interpretation. This should be fixable, leading to OTT+X
 or predicative topoi + X which should be complete wrt the setoid
 model. More categorically we could say that X characterizes the
 predicative topoi obtained by an exact completion of an LCCC - I think.

First of all, I am not sure whether a fix is needed. My recent experience in 
constructive mathematics is that it is actually quite pleasant to work 
without countable choice. Initial experience shows that it may lead to better 
algorithms implicit in the proofs. (Most of this is in my work with Thierry 
Coquand.) As you know, choice breaks abstract datatypes. See for instance the 
encoding of ADT as existential types by Mitchell and Plotkin. This is not 
possible in dependent type theory precisely because we have choice (this was 
pointed out to me by Jesper Carlstrom some time ago). I understand one 
motivation for your work on OTT as an attempt to bring back (some?) ADTs in 
type theory. It would be a pity to throw them out again without a good 
reason.

Having said that here are some quick remarks on your proposal below. 
Having choice for N-N as somewhat uncommon. It is not present in Bishop's 
constructive mathematics, i.e. more or less the setoid model of ML type 
theory. However, it is present in Brouwerian intuitionism and in some 
realizability models. Brouwer does not have choice for (N-N)-N.

Martin Hofmann has some discussion on choice and extensionality in his thesis, 
but uses a syntactic criterion somewhat like the one that you outline.

One semantic candidate for X could be `all types have a projective cover'. 
This is what is used in realizability theory and what Erik Palmgren 
translated to type theory. A type P is projective if for all f:A-B and every 
function g:P-B there is a function h:P-A with f o h = g. Projective 
types have choice. The idea is that the projective types are Bishop's 
pre-sets or the types in the setoid construction.

Best,

Bas

---
Research Group Foundations/ Institute for Computing and Information Sciences
Radboud University Nijmegen www.cs.ru.nl/~spitters/


Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Conor McBride

Hi Thorsten

I'm not sure I understand what's going on here.

Thorsten Altenkirch wrote:

Indeed, in the setoid model we can construct a function

f : A - [B]
--
lift f : [A - B]

if the setoid A is trivial, i.e. has the identity as its equivalence 
relation.


I can do it if A is decided. If you give me a : A, then I pick

 lift f = iI const (f a) Ii

or, in less idiomatic longhand

 lift f = do
   c - return const
   b - f a
   return (c b)

If you give me A - 0, it's easy.


f : A - B/~
-
lift f : (A - B)/~'


Again, if you give me some a : A, I say

 lift f = const (f a)  -- const respects the equivalence because  const 
b a ~' const b' a if b ~ b'


But hang on - what stops us from doing a Diaconescu? Excluded middle 
doesn't hold in the setoid model, even though we only get P \/ not P 
where A \/ B = [A + B].  But this would still require that we have P + 
not P in the underlying set. So what goes wrong?


We define the type of non-empty subsets of Bool as

NE = Sigma Q : Bool- Prop.Sigma x:Bool.Q x


Note that NE is inhabited, eg by

 moo = (const 1; true; ()).


We define the equivalence relation of extensional equality of subsets

~ : NE - NE - Prop

(Q,_) ~ (R,_) = forall b:Bool.Q b - R b

Now we derive:

h : NE/~ - [ NE ]

which is just the indentity on the underlying elements. The point is 
that obviously ~ implies the trivial equality of [..].


Now, if we were able to lift h we get

lift h : [ NE/~ - NE]


 return (const moo) : [ NE/~ - NE]


Obviously, NE/~ isn't a setoid with a trivial equality!

The Diaconescu argument shows that we can prove for any P:Prop

H : NE/~ - NE
--
Dia H : P \/ not P = [P + not P]


 Dia (const moo) : P \/ not P


see below for a Epigram 2+n style proof of Dia.


Under the circumstances, I really hope you've cocked this up.


We can also see what goes wrong in general: The principle

f : A - B/~
-
lift f : (A - B)/~'

fails because given the setoid A = (A0,~A) the premise gives us an 
underlying function f0:A0 - B (for simplicity we assume that B is 
trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same 
function to construct an element of  A - B we need to show that  a ~A 
b implies f0 a = f0 b, and there is no reason to believe this - unless 
~A is the equality.


I just about swallow that. But if A0 is decided, you need to use the 
spec part (which you're eliding for simplicity) to force me to use f0 in 
the way you're suggesting.



P.S.
For completeness: Dia itself can be constructed as in the COQ script: 
we use

T,F : Bool - Prop


T b = (b=true) \/ P
F b = (b=false) \/ P

by applying H to the equivalence classe T,F and projecting out the 
components we get


t,f : Bool
t = fst (H T)
f = fst (H F)
snd (H T) : t=true \/ P
snd (H F) : f=false \/ P


Are you sure? I thought

 H had return type NE, giving
 (P; a; p) = fst (H T), (Q, b, q) := fst(H F) : Bool - Prop
 where a,b : Bool, p : P a, q : Q b

but no connection necessary between T and P, F and Q.

Now, I know that my pathological functions are not the functions you're 
thinking of, but it does rather show that the real action, whatever it 
is, lies in the spec parts which you're throwing away.


More later

Conor

PS I blogged a bit about implementing OTT...



Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch

Hi Conor,


I'm not sure I understand what's going on here.


This happens if you don't type check your definitions. I got carried  
away with my non-dependent simplification of the story.

Thank you for actually reading it.


Indeed, in the setoid model we can construct a function

f : A - [B]
--
lift f : [A - B]
if the setoid A is trivial, i.e. has the identity as its  
equivalence relation.


I can do it if A is decided. If you give me a : A, then I pick

 lift f = iI const (f a) Ii


Indeed, however your trick won't work for the dependent version:

f : Pi a:A.[B a]
-
lift f: [Pi a:A.B a]


f : A - B/~
-
lift f : (A - B)/~'


Again, if you give me some a : A, I say

 lift f = const (f a)  -- const respects the equivalence because   
const b a ~' const b' a if b ~ b'


Dito. We need

f : Pi a:A.(B a)/(~ a)
-
lift f: (Pi a:A.B a)/~'

where ~' is defined as before: f ~' g = Pi a:A.f a ~ g a but for  
f,g : Pi a:A.B a and ~ is actually a family of equivalence relations  
~' : Pi a:A.(B a) - (B a) - Prop.




We define the type of non-empty subsets of Bool as

NE = Sigma Q : Bool- Prop.Sigma x:Bool.Q x


Note that NE is inhabited, eg by

 moo = (const 1; true; ()).


We define the equivalence relation of extensional equality of subsets

~ : NE - NE - Prop

(Q,_) ~ (R,_) = forall b:Bool.Q b - R b

Now we derive:

h : NE/~ - [ NE ]


We define

h0 : Pi (P,_):NE . [ Sigma b:2.P b ]
h0 (P,p) = return p

and observe that this trivially preserves ~ and hence we obtain

h : Pi (P,_):NE/~ . [ Sigma b:2.P b ]


Now, if we were able to lift h we get

lift h : [ NE/~ - NE]


 return (const moo) : [ NE/~ - NE]


lift h : [ Pi (P,_):NE/~ . Sigma b:2.P b ]

and your version ceases to work.


Obviously, NE/~ isn't a setoid with a trivial equality!

The Diaconescu argument shows that we can prove for any P:Prop

H : NE/~ - NE
--
Dia H : P \/ not P = [P + not P]




Corrected:

H : Pi (P,_):NE/~ . Sigma b:2.P b

Dia H : P \/ not P = [P + not P]



 Dia (const moo) : P \/ not P


see below for a Epigram 2+n style proof of Dia.


Under the circumstances, I really hope you've cocked this up.


I have.




We can also see what goes wrong in general: The principle

f : A - B/~
-
lift f : (A - B)/~'

fails because given the setoid A = (A0,~A) the premise gives us an  
underlying function f0:A0 - B (for simplicity we assume that B is  
trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same  
function to construct an element of  A - B we need to show that   
a ~A b implies f0 a = f0 b, and there is no reason to believe this  
- unless ~A is the equality.


I just about swallow that. But if A0 is decided, you need to use  
the spec part (which you're eliding for simplicity) to force me to  
use f0 in the way you're suggesting.


You are right. The reasoning only works for the dependent version.




P.S.
For completeness: Dia itself can be constructed as in the COQ  
script: we use

T,F : Bool - Prop

T b = (b=true) \/ P
F b = (b=false) \/ P

by applying H to the equivalence classe T,F and projecting out  
the components we get


t,f : Bool
t = fst (H T)
f = fst (H F)
snd (H T) : t=true \/ P
snd (H F) : f=false \/ P


Are you sure? I thought

 H had return type NE, giving
 (P; a; p) = fst (H T), (Q, b, q) := fst(H F) : Bool - Prop
 where a,b : Bool, p : P a, q : Q b

but no connection necessary between T and P, F and Q.


This should now work with the correct type of H.

Cheers,
Thorsten

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.



Re: [Epigram] Definitional equality in observational type theory

2007-02-01 Thread Thorsten Altenkirch

Hi Bas,


thank you - indeed this is a very interesting observation. This was
the proof I had in mind when I first claimed that the axiom of choice
is provable in OTT. However, I was deluded in believing that OTT/
predicative topoi exactly characterize the theory of the setoid
model. As you clearly point out this is not the case. To me this is
an incompleteness of the formal system (OTT/predicative topoi) wrt
the intended interpretation. This should be fixable, leading to OTT+X
or predicative topoi + X which should be complete wrt the setoid
model. More categorically we could say that X characterizes the
predicative topoi obtained by an exact completion of an LCCC - I  
think.


First of all, I am not sure whether a fix is needed. My recent  
experience in

constructive mathematics is that it is actually quite pleasant to work
without countable choice. Initial experience shows that it may lead  
to better
algorithms implicit in the proofs. (Most of this is in my work with  
Thierry
Coquand.) As you know, choice breaks abstract datatypes. See for  
instance the
encoding of ADT as existential types by Mitchell and Plotkin. This  
is not
possible in dependent type theory precisely because we have choice  
(this was

pointed out to me by Jesper Carlstrom some time ago). I understand one
motivation for your work on OTT as an attempt to bring back (some?)  
ADTs in

type theory. It would be a pity to throw them out again without a good
reason.


I'd like to understand this better - in the moment I am unconvinced.   
Instead of choice, I'd like


f : Pi a:A.(B a)/(~ a)
-
lift f: (Pi a:A.B a)/~'

for discrete types A, which means that I work in the internal  
language of the setoid model. Quotient types, even with lift, seem to  
be a good way to capture ADTs.


Also if you want to reject lift, it would be good to have a model  
construction (maybe like the setoid model) which refutes it. Other  
things which you want may become true in this model.




Having said that here are some quick remarks on your proposal below.
Having choice for N-N as somewhat uncommon. It is not present in  
Bishop's
constructive mathematics, i.e. more or less the setoid model of ML  
type

theory. However, it is present in Brouwerian intuitionism and in some
realizability models. Brouwer does not have choice for (N-N)-N.

Martin Hofmann has some discussion on choice and extensionality in  
his thesis,

but uses a syntactic criterion somewhat like the one that you outline.


I alreay realized that I should reread Martin's thesis.



One semantic candidate for X could be `all types have a projective  
cover'.

This is what is used in realizability theory and what Erik Palmgren
translated to type theory. A type P is projective if for all f:A-B  
and every

function g:P-B there is a function h:P-A with f o h = g. Projective
types have choice. The idea is that the projective types are  
Bishop's

pre-sets or the types in the setoid construction.


I'll think about this.

Cheers,
Thorsten

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.



Re: [Epigram] Definitional equality in observational type theory

2007-01-31 Thread Bas Spitters
Hi Thorsten and others,

On Tuesday 30 January 2007 21:22:53 [EMAIL PROTECTED] wrote:
 I do indeed think that Observational Type Theory with quotient types should
 be the language of a Predicative Topos. I don't see in the moment that the
 setoid model would introduce anything which isn't provable in the Type
 Theory and at least in the moment I don't see how to prove the countable
 axiom of choice in OTT. Bas, could you explain, please?

Assuming that OTT is the internal type theory of a predicative topos, say a 
PiW-pretopos (which it seems to be the case), it is not possible to prove 
countable choice in OTT. The simple reason is that every topos is a 
PiW-pretopos and that countable choice(CAC) does not hold in the topos of 
sheaves over the reals. Therefore CAC can not hold in the internal type 
theory (i.e. OTT).

Now consider the setoid model. The crucial observation is that the setoid 
Nat=(N,=_Nat) carries the finest possible equality. 
Let X=(X',=_X) be a setoid.
If we know:
 forall n in Nat there exists x in X such that (R n x), 
then, by the construction of the setoid model, there is a function on the 
underlying types f:N-X' such that 
forall n, (R n (f n))
because Nat carries the finest equality f lifts to a function on the setoid 
level since:
If n=_Nat m, then (f n)=_X (f m).
Write f':Nat = X for this lifted function. Then 
forall n in Nat, (R n (f' n)).
Thus proving countable choice in the setoid model.


This is a well-known argument in Bishop's constructive mathematics. Bishop's 
treatment of sets lead to the development of setoids by Hofmann. The lecture 
notes of the TYPES summer school in Chalmers by Erik Palmgren give a nice 
presentation of Bishop set theory in type theory.

Bas


Re: [Epigram] Definitional equality in observational type theory

2007-01-29 Thread Thorsten Altenkirch

Hi Robin,

The paper says Observational reasoning can be simulated in  
Intensional

Type Theory by the use of setoids, i.e. types with an explicit
equivalence relation.

I'm not clear on what the differences are between OTT and simulating
observational reasoning with setoids in ITT. Clearly OTT has an
explicit equivalence relation (=) which is polymorphic over  
(certain)

types. So does the paper mean explicit in some other sense?


I am not sure I understand your question. Let my try to answer anyway.

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.


Cheers.
Thorsten



And doesn't OTT have the same problems (equality not automatically
substitutive, complications in formalising category theory, lots of
explicit coercions) that the paper says ITT has? I don't see how OTT
helps with any of those problems, but the way that OTT is contrasted
with ITT suggests that it should. I must be misunderstanding  
something.


--
Robin




Re: [Epigram] Definitional equality in observational type theory

2007-01-29 Thread Bas Spitters
Dear Thorsten, Robin,

Now that the discussion has turned to setoids and observational type theory, I 
could not help myself from responding. (Thorsten and I had quite some 
off-line discussion about this).

I generally agree with Thorsten's description of observational type theory as 
internalizing the setoid construction. One clearly feels the need for such 
machinery when working with Coq. (Although this seems to have improved 
somewhat with the inclusion of the new setoid_rewrite tactic.)

However, I would like to point out that there seems to be an important 
distinction between the category of setoids and the extensional type theory 
defined by observational type theory. Let me first say how they are similar. 
Both of these categories should have the structure of a predicative topos. 
The search for the right definition of a predicative analogue of topos theory 
was started by Moerdijk and Palmgren. A topos is a model of higher-order 
intuitionistic logic. We should have

topos   pred. topos
   ==  -
iHOLext type theory

However, predicative toposes should also generalize toposes. Currently, the 
notion of a Pi W-pretopos seems to be a good candidate for the notion 
of predicative topos. In any case, observational type theory should give 
rise to the internal type theory of a predicative topos.

However, the predicative topos of setoids models the axiom of countable 
(dependent) choice. This implies that the Dedekind real numbers and the 
Dedekind real numbers coincide. For general (predicative) toposes the 
Dedekind construction of real numbers and the Cauchy definition of real 
numbers need not be the same. Since it is unlikely that observational type 
theory includes the axiom of countable choice we will have to take this into 
account when programming, say, the real numbers in epigram.

To conclude, when using the setoid construction in intensional type theory we 
can use all the results from Bishop's constructive mathematics when 
programming/proving. This is no longer the case in observational type theory. 
Hopefully, it is possible to develop a good replacement.

Bas

PS: I know this may sound too theoretical to some, but it seems to have a real 
effect on programming, say, real numbers in epigram.

---
Research Group Foundations/ Institute for Computing and Information Sciences
Radboud University Nijmegen www.cs.ru.nl/~spitters/


Re: [Epigram] Definitional equality in observational type theory

2007-01-26 Thread Robin Green
Thanks to all who replied.

I have another couple of questions, more fundamental this time.

The paper says Observational reasoning can be simulated in Intensional
Type Theory by the use of setoids, i.e. types with an explicit
equivalence relation.

I'm not clear on what the differences are between OTT and simulating
observational reasoning with setoids in ITT. Clearly OTT has an
explicit equivalence relation (=) which is polymorphic over (certain)
types. So does the paper mean explicit in some other sense?

And doesn't OTT have the same problems (equality not automatically
substitutive, complications in formalising category theory, lots of
explicit coercions) that the paper says ITT has? I don't see how OTT
helps with any of those problems, but the way that OTT is contrasted
with ITT suggests that it should. I must be misunderstanding something.

-- 
Robin


Re: [Epigram] Definitional equality in observational type theory

2007-01-25 Thread Thorsten Altenkirch

Hi Robin,

thank you for your comments. Indeed we are currently revising this  
paper, hence your comments are especially welcome.



I've been reading Towards Observational Type Theory. I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read wider I'll understand more of it.


We should certainly strive to fix this...



However, one rule which jumped out at me is this, on page 9,  
because it

seems silly (apologies if my email client mangles this even after I've
tried to fix it up - I've never tried pasting type rules from PDFs  
into

it before):

Γ |- S≡T  Γ |- Q:S=T  Γ |- s:S
--
  T
 Γ |- s[QS ≡ s : T


It seems silly to include a definitional equality as a premise,  
because
I _thought_ the whole point of definitional equality was that S≡T  
means

that S and T are freely co-substitutable, and type-checking will
automatically substitute S for T or T for S _whenever_ required. (For
example, it is often noted that Coq will automatically reduce (i.e.
substitute) n+0 to n in a dependent type - but only if you write n+0
the right way round! I can't remember offhand which way round  
works.)




You are right to say that this rule is unusual. In the implementation  
it creates a dependency between defintional equaliy and reduction  
which doesn't appear in conventional systems.


It can be justified by observing that in intensional Type Theory we  
have tat


s [refl S ≡ s

where refl S : S=S. However, due to proof-irrelevance any term Q : S  
= S will be definitionally equal to refl S, hence if p:S=S then


s [p ≡ s



So anyway, surely any derivation which needed that rule could also
use this rule instead:

  Γ |- Q:S=S  Γ |- s:S
--
  S
 Γ |- s[QS ≡ s : S

(which is trivial), substituting S for T before applying it, and
substituting Ts for some of the Ss afterwards.



You are right - your rule is equivalent and more concise. However, a  
type checker will have to implement the first rule. To check whether
s [Q reduces to s you have to verify whether the types in the type  
of Q:S = T are definitionally equal, i.e. whether S ≡ T.



Where have I gone wrong?



Indeed nowhere.

There is some discussion of related issues in the Epigram developers  
blog:


http://www.e-pig.org/epilogue/

is particular in the Epigram 2 design doc.

Cheers,
Thorsten
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.




Re: [Epigram] Definitional equality in observational type theory

2007-01-25 Thread Wouter Swierstra

Hi Robin,

I just saw Thorsten answered your e-mail. I'd better finish what I  
started though.


I'm not an expert on OTT, but here are a few thoughts.

The real rule for coercion is the one on page 3. It doesn't require  
the types to be definitionally equal. Section 5 mainly speculates on  
adding two extensions:


* Definitional proof irrelevance

* Definitionally defining all coherence proofs to be refl and  
coercions within the same type to be the identity.


Like Thorsten says, this is a bit tricky and makes evaluation and  
equality mutually recursive - which is a bit odd. If you're looking  
to understand OTT, I wouldn't get too worked up about this rule -  
it's a bit technical and the really important stuff is in the first  
few sections.


I'm not sure if it helps, but here's a bit of Agda code  
implementing OTT:


www.cs.nott.ac.uk/~wss/Misc/ott.agda

I certainly understood much more of the paper after writing the Agda.  
I'm not sure if reading it will have quite the same effect, but it  
might be worth a shot.


All the best,

  Wouter

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.