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

[Thorsten Altenkirch]

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


From: Agda <agda-bounces at lists.chalmers.se> on behalf of Andrew Pitts <andrew.pitts at cl.cam.ac.uk>
Date: Thursday, 7 November 2019 at 11:01
To: agda list <agda at lists.chalmers.se>
Subject: [Agda] initial T-algebra for an endofunctor T, via sized types

Recently I have been more or less forced into using Agda’s sized types to get a certain development to go through and it has set me thinking about the use of sized types with inductive definitions. The current documentation stub says

"Sizes help the termination checker by tracking the depth of data structures across definition boundaries”

and then goes on to give an extended example to do with coinduction; but of course sizes are useful for induction too.

To get a better feel for what one can achieve, I tried using sizes to construct the (provably) initial algebra for a postulated strictly positive endofunctor on Set and eventually succeeded; but the construction was much more elaborate than I expected (and involved the use of quotient types). You can see it here:

<https://www.cl.cam.ac.uk/~amp12/agda/initial-T-algebras/>

Did I somehow over-complicate things? Am I re-inventing a construction that already exists?

Andy Pitts







This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




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