[Agda] Coinductive families

[Thorsten Altenkirch]

Hi Dan,

you are right if we think of coinductive types as terminal coalgebras
then it is clear that the destructor (i.e. the coalgebra) is
fundamental and the constructor is derived. However, it is not clear
wether they should be presented this way in dependently typed
programming. 

The alternative, we have been exploring, is to to say that infinite
objects are always introduced by allowing a delayed expression as a
value. This is even true for functions, which are infinite and which
are introduced by lambda abstraction. Similarily we can introduce an
infinite data object by allowing suspended expressions as values using
♯ (and correspondingly ∞ on the level of types).

This way we disentangle the question wether data should be presented
as sums or products from the question wether it should be finite of
infinite. 

I think this is beneficial for design and refactoring when you want to
move between finite and infinite representations easily. I.e. at some
point you may have just used lists but decide that you need to allow
for infinite lists as well, moving from lists to colists. This move
should not force you to rewrite your whole program from a constructor
based representation to a destructor based one. Indeed, ideally you
would like that List is a subtype of Colist. Related to this is the
possibility to have mixed inductive/coinductive definitions without
having to nest data inside codata. E.g. I find the mixed definition of
stream processors and the associated programs quite easy to understand
while the orthodox nested constructor based data inside destructor
based codata causes me headaches and I need half a day to write a
program which I don't really understand. But maybe this is only me. 

You are correct to say that there are issues with this approach. One
of them is that our naive extension of the termination checker doesn't
work very well for nested definitions (see
http://www.cs.nott.ac.uk/~txa/publ/InvertedQuantifiers.pdf). And more
foundational it seems that we have to go via the partial meaning of
programs to explain total programs (and I don't even know exactly how
to do this).

In this sense the coinductive types as terminal coalgebras view is
easier to understand - we only need to talk about total things and
there is a clear categorical semantics. We have been thinking about
how to connect the two, i.e. the suspension view and the coalgebra
view. But I still wonder wether somehow the supension view is an
alternative and maybe intuitively preferable approach to explain
infinite data.

Cheers,
Thorsten


On 5 Oct 2010, at 12:27, Dan Doel wrote:

> 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).

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101005/f1c26d0e/attachment.html