[Agda] Coinductive families

[Dan Doel]

On Monday 04 October 2010 8:45:42 pm Anton Setzer wrote:
> Although a record is close to a coalgebra, I think there are two problems:
> 
> - in Agda record types have the eta rule, which leads to
> non-normalisation in coalgebras.
>    Restricting it for recursive types and allowing it for non-recursive
> types seems to me confusing for the
>    user.
> If we define
> 
> a : Stream
> a  = record{head = 0; tail = a }
> 
> misleads the user into thinking that this will expand to
> 
> a = record{head = 0; tail = record{head = 0; tail = record{  ... }}}
> 
> Even if s/he doesn't expect this, she might expect some partial expansion.

Yes, I didn't mean to suggest (if I did) that eta would work with recursive 
records. Unfortunately, I know of no way to get equality of coinductive types 
via bisimulation without adopting some level of extensionality. And yes, it 
would be strange for eta to work sometimes and not others.

I just thought it was worth noting that eta can correspond to coinduction as 
well as induction, and that, being:

  unfold observe x = x

if we think of 'record { proj1 = e1 ; proj2 = e2 ... }' as specifying what the 
projections of the value being defined will be, it looks more like coinduction 
than induction. But perhaps I'm biased.

-- Dan