[Agda] Starting work on v2.0 of the Agda Standard Library

[Matthew Daggitt]

Dear all,

After a recent discussion on Zulip, various members of the Agda community
have come to the conclusion that we have accumulated enough bad design
decisions in the Agda standard library that it is now worth starting work
on a v2.0. This isn't envisaged to be a radical overhaul, and although we
will be fixing things that require unavoidable backwards incompatible
changes, we still expect the vast majority of code written with v1.7 to
work in v2.0. We will however be removing all code that was deprecated
before the release of v1.0.

We know making breaking changes is always somewhat unpopular. However, the
art of designing large developments in dependently-typed systems such as
Agda is still relatively poorly understood, and we believe that in the long
term it's more important to find and implement the right design decisions,
rather than build upon the sub-optimal ones! After the temporary
disruption, we hope that the changes will make all the users of the
standard library's lives easier going forward.

Obviously community feedback on this process is vital! Over the coming
weeks and months, in the hope of starting discussions with those
interested, we'll be posting on Zulip and on the mailing list about the
bigger changes before we start work on them. Equally, if there's any parts
of the standard library that you've always thought could be done better,
now's the time to open an issue on the issue tracker
<https://github.com/agda/agda-stdlib/issues>.

Many thanks,
Matthew, on behalf of the Agda Team
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210706/b6f0d996/attachment.html>