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

[Aaron Bohannon]

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
>