[Agda] Re: [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad)

[Thorsten Altenkirch]

In extensional Type Theory Streams over A are isomorphic to Nat -> A.  
Hence there is no need (at least from a foundational point of view) to  
add streams once you have functional extensionality.

Actually all coinductive types can be encoded as omega-limits once you  
have functional extensionality. The encoding of Nat -> A is just an  
instance of this general construction.

The problem is that adding axioms destroys canonicity. Overcoming this  
problem is the main point of OTT (Observational Type Theory).

Thorsten

On 24 Nov 2008, at 17:09, Aaron Bohannon wrote:

> OK.  You have convinced me that coinductive data types in Coq are
> mismatched with their traditional mathematical counterparts in
> essentially the same way as Coq's function types are mismatched with
> function spaces in a set-theoretic setting.  I, personally, don't find
> that particularly surprising nor worrisome.  It does bring one
> technical question to mind, though:  I know it is sound to add an
> axiom of extensionality to Coq for any function space -- is it also
> sound to add an axiom of extensionality for codata?  That is, may I
> safely assert that a standard definition of bisimilarity on a
> coinductive data type implies the default (intensional) equality
> ("=")?  (I don't know if this question is relevant to Agda.)
>
> - Aaron
>
> On Mon, Nov 24, 2008 at 7:42 AM, Dan Doel <dan.doel at gmail.com> wrote:
>> On Saturday 22 November 2008 10:25:51 pm Dan Doel wrote:
>>> And, I think that the coinductive syntax is misleading on this  
>>> front, when
>>> you see:
>>>
>>>  j ~ cosuc i
>>>
>>> You may think, "j is built from an i and a cosuc constructor", but  
>>> *this is
>>> not the case*.
>>
>> I was thinking about the codata situation a bit earlier, and had  
>> sort of a
>> flash of insight (which after looking up older posts on the  
>> subject, I realized
>> was something that had been said before, but I hadn't fully  
>> understood yet)
>> that this is probably the key difference between the codata in Agda/ 
>> Coq, and
>> Anton Setzer's coalgebra formulation, and may be the key thing that  
>> codata
>> gets "wrong." In fact, the codata approach not only leads one to  
>> believe that
>> a coinductive value is built from constructors, it treats things as  
>> if that
>> were the case!
>>
>> In long, a couple of the problems with codata are that 'evaluation  
>> doesn't
>> preserve types' and 'it seems that if we just evaluate some of the  
>> terms more,
>> we could show that one is equal to the other, but equating two  
>> values in this
>> way is undecidable in general.' But, both of these assume that  
>> coinductive
>> values are subject to evaluation in the first place, and that said  
>> evaluation
>> leaves you with some nested constructors as with inductive values!  
>> However, if
>> my understanding of Setzer's coalgebra formulation is correct, it  
>> is not
>> correct to say that values with coinductive type are subject to any  
>> reduction
>> at all (or at least, it shouldn't be, I think). Only observation is.
>>
>> Perhaps the best illustration is:
>>
>> out : Conat -> Conat
>> out cozero    = cozero
>> out (cosuc n) = cosuc n
>>
>> This is the type of function people use in Coq and Agda to force  
>> evaluation
>> when they desire it for proofs and whatnot. However, consider if we  
>> look at
>> something like the coalgebra approach:
>>
>> coalgebra Conat : Set where
>>   _* : Conat -> 1 + Conat
>>
>> -- these are the equivalents of cozero and cosuc used as  
>> 'constructors'
>> -- on the right hand side of an equation (or in an indexed family  
>> definition
>> -- for that matter).
>> cozero : Conat
>> cozero * = inl ()
>>
>> cosuc : Conat -> Conat
>> (cosuc n) * = inr n
>>
>> anaConat : {a : Set} -> (a -> 1 + a) -> a -> Conat
>> anaCona f a = bimap id (anaConat f) (f a)
>>
>> We may ask what the equivalent of out is. There are two  
>> possibilities:
>>
>> out1 : Conat -> 1 + Conat
>> out1 n = n *
>>
>> out2 : Conat -> Conat
>> (out2 n) * = n *
>>
>> However, neither of these perform the same function as out. In the  
>> first case,
>> we cannot even begin to ask if 'out1 c == c' because they don't  
>> even have the
>> same type (or if we have a heterogeneous equality, the answer is  
>> simply "no")!
>> On the other hand, we can ask if 'out2 c == c', since they have the  
>> same type,
>> but, if c is not subject to evaluation, then neither is 'out2 c',  
>> so we simply
>> compare the terms directly, notice they aren't identical, and the  
>> answer is
>> "no" (again).
>>
>> So, the fact that we can prove that "out c == c" under codata,  
>> because we can
>> evaluate coinductive values and compare the 'constructors' and  
>> constituent
>> terms we get from doing so seems to be the anomaly. So, I think,  
>> tentatively,
>> that it should be the case that 'out c /= c'. This, of course, makes
>> intensional equality pretty worthless, but perhaps that's the way  
>> it should
>> be, as equality for coinductive types is rather inherently  
>> extensional, and it
>> isn't difficult to produce coinductive values that are equal but not
>> (instensionally) provably so anyhow:
>>
>> i : Conat
>> i = anaConat inl 5
>>
>> j : Conat
>> j = anaConat inl "a string"
>>
>> w : Conat
>> w * = inl w
>>
>> All of these are extensionally equal, but you'll never be able to  
>> unfold them
>> to a point where they match each other; their equality can only be  
>> shown by
>> proving they are bisimulations of one another.
>>
>> (I realize this is significantly less onerous than 'out c /= c',  
>> but I'd
>> tentatively suggest coinductive types are already even worse about  
>> intensional
>> equality than functions are; functions are similar to coinductive  
>> types,
>> inasmuch as many are infinite (set/list of input-output pairs), and  
>> their
>> equality is specified in terms of the observations you can make of  
>> them
>> (application to values), but we have rules for reducing lambda  
>> terms to others
>> that denote equivalent functions, whereas there are no such rules  
>> (that I know
>> of) for coinductive types in general.)
>>
>> Of course, making intensional equality worthless for coinductive  
>> types may
>> make them too cumbersome to work with, and may not be the right  
>> choice for Coq
>> or Agda (at the moment at least). But, I think this may be the root  
>> of the
>> problem with the codata approach.
>>
>> As I said, this insight isn't particularly new (although I was  
>> pleased to have
>> come up with it on my own :)), but it hadn't been mentioned in this  
>> thread
>> yet.
>>
>> Cheers,
>> -- Dan
>>
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


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.