[Agda] initial T-algebra for an endofunctor T, via sized types

[Andrew Pitts]

> On 8 Nov 2019, at 11:21, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> 
> Hi,
>  
> I didn’t see Wouter’s comment but I guess I can add another unhelpful comment along the same lines. Really a strictly positive operator should be a container and we do need some syntactic sugar for this so that we just have to write something similar as what you do (didn’t even know there were strict positivity annotations). The same criticism applies to the whole sized type story: a reasonable implementation of sized types should be just syntactic sugar for programs we can define without them.
>  
> But I realize you want to use agda as it is and my principled complaints are not helping. However, they are the reason that I haven’t taken these adhoc extensions serious. I am still waiting that somebody provides a reasonable explanation (i.e. semantics / translation) for them.
>  
> Thorsten

I think expressing semantical scepticism is justified, and long may you do so. 

But such scepticism is perhaps more justified for the semantic status of Agda’s notion of “strictly positive" than it is for its sized types, where we have some fine papers by Abel and Pientka (and maybe others) about its theory. (Although there is more to understand: I think your first paragraph expresses the hope that sized types are a conservative extension of some more well-understood, core type theory — it would be good to have results settling that sort of question one way or another.)

Andy
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191108/ec91dd37/attachment.html>