[Agda] Tentative guidelines for working with coinductive types

[Nils Anders Danielsson]

On 2009-01-15 03:14, Noam Zeilberger wrote:
> On Thu, Jan 15, 2009 at 02:23:48AM +0000, Nils Anders Danielsson wrote:
>> On 2009-01-14 20:36, Noam Zeilberger wrote:
>>> [...] it might end up being easier and less bug-prone to adopt the
>>> more general, destructor-based view of coinductive types.

[...]

> But it's only a *fragment* of a more general type theory with
> arbitrary coalg definitions by multiple destructors. I'm wondering
> whether it might be better to consider the general case.

I don't think that it would be easier or less bug-prone to /implement/,
or more expressive. It might be nicer to use, since there would be no
need to wrap code in ♯_ and ♭. I suspect that I would still prefer the
approach with ∞ + data, because that way I get to use indexed inductive
families with coinductive components.

-- 
/NAD


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.