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

[Dan Doel]

On Monday 24 November 2008 12:09:06 pm 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.)

I'm not sure I'm fully qualified to give a definitive answer to your question. 
However, my gut reaction is that it is as safe to add an extensionality axiom 
for coinductives as it is for functions. Certainly, I'd expect an extensional 
type theory that includes codata of some sort to allow it. So unless it 
combines in some weird way with the pseudo-constructor semantics of Coq/Agda 
(which I doubt), I imagine it's sound.

The one problem with such a thing is that I think it might be hard to work out 
a generic-enough bisimilarity relation to be useful. Functions are easy with:

  forall x -> f x = g x

but a generic bisimilarity is essentially:

  a * = b *

Where the _* operator needs to Just Work for any coinductive type (just like 
function application), and in most cases, equality on the shapes and 
bisimilarity on the coinductives are mutually recursive. So, unless you don't 
mind manually adding an axiom for every coinductive type you create (or you 
have macros, I guess), this is going to be a pain in a language that doesn't 
know about bisimilarity, and define it for you.

Like I said, though, I'm somewhat new at this, so I'll defer to the type 
theory gurus if they have some fancy bisimilarity formulation, or example of 
where extensionality for coinductives is unsound. :)

-- Dan