[Agda] how to type this?

[Thorsten Altenkirch]

> I want to consider functions f that take infinite sequences x_0,  
> x_1, x2_, .... to values in a result type R. So, at first sight, we  
> have something like
>
>     f : prod_i X_i -> R.
>
> But I want the type X_i to depend on the elements x_0, ... x_(i-1)  
> in addition to i. That is, x_i is to have type (X_i x_0 ... x_(i-1)).
>
> If the sequence x_i were finite, I know how to do that.

Nisse has already replied to this.

> How can this be expressed in Agda (or in type theory) in the  
> infinite case in a simple and mathematically elegant way? (I prefer  
> to avoid co-induction if possible.)

I sense that there is a contradiction between " a simple and  
mathematically elegant way" and "I prefer to avoid co-induction if  
possible". It is always possible to code up coinductive definitions  
using functions (the constructive literature is full of this), but I  
think this is neither simple nor elegant.

Btw, Nisse was using the new implementation of coinduction which  
allows you to mix inductive and coinductive defintions, see http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Codatatypes
We also have a recently rejected paper about this:
http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html

Cheers,
Thorsten

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.