[Agda] Agda's coinduction incompatible with initial algebras

[Thorsten Altenkirch]

On 6 Oct 2011, at 11:46, Nils Anders Danielsson wrote:

> 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.

Exactly.

I have the impression that we are putting too much into the Type System.
There is a certain beauty in the simplicity of Type Theory.

> 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.

I completely agree.

On a theoretical level I'd like to see a translation from sized types into
using eliminators. Is it clear that this is possible at least in principle.

How do sized types interact with induction recursion?
wiith induction-induction?
And mixed induction/coinduction ?

Cheers,
Thorsten

> 
> -- 
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda