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

[Dan Doel]

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