[Agda] Agda's coinduction incompatible with initial algebras

[Nils Anders Danielsson]

On 2011-10-05 18:13, Andreas Abel wrote:
> These two systems have not been integrated, since there is a history
> of dispute stretching several years what we should go for. [With a
> current cease-fire, but no peace treaty. Maybe I should not have
> touched this issue.]

This sounds a little dramatic. :)

I agree that Agda's current mechanism for termination/productivity
(especially the latter) is not good enough. The compositionality
provided by sized types is very nice. There may also be other approaches
that can give us compositionality, but so far sized types seem to be
ahead in the game.

However, sized types are quite /complicated/. The design in MiniAgda
involves extra data type indices, irrelevance, subtyping for sizes,
continuity conditions, positivity/negativity annotations, and perhaps
more.

Despite all this complexity I'm still interested in sized types, because
they seem to make some programs much easier to write. Perhaps we can
find a decent compromise. I would like to see a design with the
following properties:

* Newcomers to the language can write simple structural recursion
   without knowing anything about sized types.

* When they decide to start using sized types they shouldn't have to
   change a large fraction of their existing code (adding size indices
   etc.).

We have discussed such a design in the past, but I don't think we ever
came up with anything good.

-- 
/NAD