[Agda] Tentative guidelines for working with coinductive types

[Noam Zeilberger]

On Thu, Jan 15, 2009 at 02:23:48AM +0000, Nils Anders Danielsson wrote:
> On 2009-01-14 20:36, Noam Zeilberger wrote:
> >
> >My one thought about the proposed changes to Agda is that, while
> >they do make good sense, it might end up being easier and less
> >bug-prone to adopt the more general, destructor-based view of
> >coinductive types.
> 
> I think that the simplest implementation of the destructor-based view
> would be almost identical to what I suggested.
> 
> In the simplest case we can settle for a single "corecord" type,
> analogously to the codata type which I suggested, and almost identical
> to the "coalg" type which Anton suggested in "Getting codata right":
> 
>   corecord ∞ (A : Set) : Set where
>     ♭ : A

I agree that your proposal precisely implements the destructor-based
view of the ∞ coalg constructor, but my question is whether to limit
Agda to this single coalg constructor.  Yes, you can translate
arbitrary codata definitions into this fragment using Anton's approach
in "Getting codata right".  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.

Noam