[Agda] Coinductive families

[Dan Doel]

On Tuesday 05 October 2010 5:41:58 am Thorsten Altenkirch wrote:
> I tried to guess what "it" is. :-)

Sorry. :)

> Reading on, it seems that you are saying that the termination checker
> should be aware of destructors in the sense that a destructor should make
> things structurally smaller but that this would lead to non-termination
> (for open terms).
> 
> Is this a sensible summary? I don't have a good answer, actually I haven't
> thought of this.

My ultimate point is that I don't think whether a type is presented as a sum 
of constructors or a product of destructors can really be so easily divorced 
from whether that type is inductive or coinductive. This is because an 
inductive type *is* a type defined by a one-step constructor and an associated 
recursive elimination, and a coinductive type is defined by a one-step 
destructor, and a recursive introduction. These aren't just presentational 
differences.

You can use the recursive eliminator of an inductive type to define 
destructors, and you can figure out what the constructors of an inductive type 
would look like based on the destructors you want to define (and dually...). 
But the basis for programming with, and recursion over those inductive types 
will still be the constructors, and not the destructors. So you have to be 
sure that programming with the latter behaves like some translation into the 
former. And not simply doing the translation can lead to problems, like non-
termination for inductives, and lack of subject reduction for coinductives* 
(maybe others).

Perhaps another indicator is that in the Agda approach that has emerged, with 
all constructors, rarely does one see functions whose types contain ∞ T. We 
always write functions over T, because it is what interacts appropriately with 
dependent pattern matching on constructors. But this is analogous to using FνF 
everywhere instead of νF. The two are isomorphic, but.... (And if we were to 
get rid of the magic ∞ style of coinduction, ∞ T is all we'd have ready access 
to for a directly defined coinductive type, not T.)

Hopefully that's a little clearer?

-- Dan

[*] If we have

  codata Conat : Set where
    constructor
      cozero : Conat
      cosuc  : Conat -> Conat

we know that for n : Conat, being able to match on n and obtaining n = cozero 
or n = cosuc m definitionally causes problems. But an appropriate extensional 
equality should allow us to prove that

  ∀ n. (n = cozero) ⊎ (∃ m. n = cosuc m)

that is, if Conat is really a final coalgebra (instead of just weakly final), 
either n and cozero are the same element of Conat, or n and cosuc m are the 
same element, because a final coalgebra should contain one unique value for 
each possible sequence of observations (I think that's appropriate intuition). 
So the problem doesn't seem to come from us treating unequal things as equal, 
but from what we think cosuc, cozero and equality mean (unless extensional 
type theories with coinductives also have problems; I'm not sure if there are 
any to sample).