headers
Thorsten Altenkirch | 1 Feb 2007 08:55
Picon
Gravatar

Re: Definitional equality in observational type theory

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
(Continue reading)

Permalink | Reply | 4 comments |
headers
Bas Spitters | 1 Feb 2007 10:20
Picon
Favicon

Re: Definitional equality in observational type theory

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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Conor McBride | 1 Feb 2007 10:28
Picon

Re: Definitional equality in observational type theory

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)/~'
(Continue reading)

Permalink | Reply | 1 comment |
headers
Thorsten Altenkirch | 1 Feb 2007 22:32
Picon
Gravatar

Re: Definitional equality in observational type theory

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)/~'
>
(Continue reading)

Permalink | Reply | 0 comments |
headers
Thorsten Altenkirch | 1 Feb 2007 22:41
Picon
Gravatar

Re: Definitional equality in observational type theory

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Robin Green | 8 Feb 2007 03:37
Gravatar

Re: Observational type theory (was: definitional equality in observational type theory)

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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Conor McBride | 9 Feb 2007 12:47
Picon

Re: Observational type theory

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Conor McBride | 12 Feb 2007 23:08
Picon

Re: [epigram-help] implicit arguments

Hi

I hope you don't mind me copying this reply to the mailing list, as it 
may be of more general interest.

Jonathan Lee wrote:
> I've been trying the tutorial and I'm coming to the part about the
> (vec x) function.  I'm a bit confused on how the implicit syntax as
> when I input:
>
>     ( n : Nat ;  x : X  !
> let  !--------------------!
>     ! vec_n x : Vec n X )

Mea culpa. Since writing the tutorial, I broke this example (and one or 
two others) when I made a change to the system's default strategy for 
ordering implicit arguments relative to each other and to the explicit 
arguments. You can see the symptoms in the Horace buffer

---------------------------------------------------------------
     (  n : Nat ;  x : X  !               
let  !--------------------! ;  vec _ n x []
     ! vec _n x : Vec n X )               
---------------------------------------------------------------

{Undo} {Reset} {Quit}                            

n : * ;  n' : Nat ;  x : n |- vec _ n x : Vec n' n

{Elaborate}
(Continue reading)

Permalink | Reply | 1 comment |
headers
Conor McBride | 12 Feb 2007 23:15
Picon

Re: [epigram-help] implicit arguments

Conor McBride wrote:

I also apologise for the way Mozilla Thunderbird arbitrarily turns my 
code into jigsaw puzzles.

I hate computers.

All the best

Conor
Permalink | Reply | 0 comments |
headers
Pierre Casteran | 13 Feb 2007 08:34
Picon

reversing a vector

Hello,

  with vectors and vappend defined as in the Tutorial, I tried to define 
vrev as follows :

     (     xs : Vec n X     !                        
let  !----------------------!                        
     ! vrev _n xs : Vec n X )                        

     vrev _ n xs <= rec xs                           
     { vrev _ n xs <= case xs                        
       { vrev _ zero vnil => vnil                    
         vrev _ (suc n) (vcons x xs)                 
           => vappend _ n (vrev _ n xs) (vcons x vnil)
       }                                             
     }     

The last clause was rejected, (I presume) because of the non-unification of
(suc n) with (plus n (suc zero)). Is that right ?
Is there a way to use some commutatitivy of plus (like using JMeq in 
Coq) ? 
Or any other way to define vrev ?

Cheers,
Pierre
Permalink | Reply | 2 comments |

Gmane