[Agda] Coinductive families

[Anton Setzer]

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.

The reason is that record{...} looks like a constructor.

If we instead define

a : Stream
head a = 0
tail a = a

then it is clear that  a doesn't expand at all, and
tail a   reduces to a which stays.

So I think using a new keyword (or reusing the old keyword codata which 
is no longer
in use) for coalgebras is a better solution.


I think

codata Stream (A : Set) : Set where
   head : Stream A -> A
   tail    : Stream A -> Stream A

ninfty : Stream Nat
head ninfty = 0
head (tail ninfty) = 0
tail (tail ninfty) = ninfty

looks neat and clear.

Anton
Anton