editing pass; too many changes to document, diff is best way to get a…

…n idea.

paper/paper.md

@@ -14,7 +14,7 @@ authors:
 	orcid: 0000-0000-0000-0000
     affiliation: 2
   - name: Carette, Jacques
-	orcid: 0000-0000-0000-0000
+	orcid: 0000-0001-8993-9804
     affiliation: 3
   - name: McKinna, James
 	orcid: 0000-0001-6745-2560
@@ -48,20 +48,21 @@ Unlike the standard libraries of traditional programming languages, the Agda sta
 
 # Statement of need
 
-Most programming languages include a "standard" library offering a basic set of algorithms, data structures, and operating system operations.
+Most programming languages include a "standard" library offering a basic set of algorithms, data structures, and operating system procedures.
 However, there are two reasons why a standard library is particularly important in Agda compared to traditional programming languages.
 
 First, like other theorem provers, the Agda language provides only a minimal core set of primitives from which programs can be constructed.
 As a result, many concepts traditionally considered part of a language must be defined within the program itself.
-While this approach reduces compiler complexity and enhances its reliability, it also means that users have access to fewer built-in definitions initially.
-For example, in a fresh Agda environment, there is no predefined notion of an integer or a string, let alone more complex data structures such as arrays or maps.
+This approach reduces compiler complexity and enhances its reliability, and also shows the strength of the core language
+itself as it can indeed push these concepts out to the library.
+For example, in a fresh Agda environment, there is no predefined notion of an integer or a string, let alone more complex data structures such as arrays or maps. Thus the crucial need for a standard library.
 
-Second, Agda users often seek to prove that programs constructed using data types from the standard library are "correct." Therefore, the standard library must provide not only the operations for these data types but also proofs of their correctness (e.g., proving that integer addition is commutative or that string concatenation is associative).
-Without the Agda standard library, something as simple as defining a function to reverse a string and proving that it preserves the length of the string would require hundreds of lines of code.
+Second, Agda users often seek to prove that programs constructed using data types from the standard library are "correct." 
+Therefore, the standard library needs to provide all the necessary building blocks: not just operations for these data types but also proofs of their basic properties (e.g., that integer addition is commutative or string concatenation is associative). Starting from just the language, something as simple as defining a string reversing function and proving that it preserves the length of the string would require hundreds of lines of code.
 
 # Impact
 
-The Agda standard library has been used in a wide range of projects, too numerous to list exhaustively.
+The Agda standard library (hereafter: `agda-stdlib`) has been used in a wide range of projects, too numerous to list exhaustively.
 A diverse selection of such projects, not intended as endorsements over any others, includes:
 
 - Formalisation of category theory [@hu2021categories]
@@ -74,58 +75,58 @@ A diverse selection of such projects, not intended as endorsements over any othe
 
 - Verification of routing protocols [@daggitt2023routing]
 
-As one of the largest existing Agda libraries, the standard library has had a synergistic relationship with the development of Agda itself, prompting the implementation of several new language features.
-For example, the standard library is designed to be compatible with several different compiler options, including `--cubical` and `--safe`.
-To enable this, in 2019 Agda categorised all language options into two categories of ''infective'' and ''coinfective'', allowing the library to precisely partition code that can be used under certain flag combinations.
-This categorisation enables the library to integrate safe code natively defined in Agda with code that uses unsafe operating system calls, while maintaining the safety guarantees of the former.
+`agda-stdlib` has had a synergistic relationship with the development of Agda itself, prompting the implementation of several new language features.
+For example, `agda-stdlib` is designed to be compatible with several different compiler options, including `--cubical` and `--safe`.
+To enable this, in 2019 Agda categorised all language options into two categories of ''infective'' and ''coinfective'', allowing any library to precisely partition code that can be used under certain flag combinations.
+This categorisation enables libraries to integrate safe Agda code with code that uses unsafe operating system calls, while maintaining the safety guarantees of the former.
 
-Additionally, the library has directly influenced the language by requesting the ability to attach custom messages to definitions, which are then displayed by the compiler when the definitions are used, enabling the implementation of deprecation warnings.
+Additionally, the development needs of `agda-stdlib` has directly influenced the language by requesting the ability to attach custom messages to definitions, which are then displayed by the compiler when the definitions are used, enabling the implementation of deprecation warnings. This lets ends users more easily evolve their code along with the evolution of `agda-stdlib`.
 
 # Design
 
 Designing a standard library for an ITP such as Agda presents several challenges.
 
-Firstly, as discussed, the standard library contains many of the foundational mathematical results used to prove program correctness.
-Even though the library currently focuses on discrete mathematics - reflecting the bias in its user base towards programming language theory - organising this material into a coherent and logical structure is extremely challenging [@carette2020leveraging].
-There is a constant tension between being as general as possible (e.g., defining operations over general algebraic structures) and providing clear, straightforward, and intuitive definitions (e.g., defining operations concretely over integers).
-Additionally, there is a persistent temptation to introduce new representations of existing mathematical objects that are easier to work with for a particular problem, which comes at the cost of duplicating the theory for the new representation.
-Theorem provers like Isabelle [@paulson1994isabelle] and Coq [@coq2024manual] approach these problems by having very minimal standard libraries and encouraging the use of external libraries developed by the community, which reduces the emphasis on ensuring the existence of canonical definitions for certain concepts.
-On the other hand, MathLib [@van2020maintaining] for Lean aims to provide a repository of canonical definitions.
-The design of the Agda standard library leans more towards the Lean approach, with a high bar set for adding alternative formalisations of the same result.
+Firstly, as discussed, `agda-stdlib` contains much of the foundational mathematics used to prove program correctness.
+While the focus on discrete mathematics and algebra reflects the bias in its user base towards programming language theory, organising this material into a coherent and logical structure is extremely challenging [@carette2020leveraging].
+There is constant tension between being as general as possible (e.g., defining operations over general algebraic structures) and providing clear, straightforward, and intuitive definitions (e.g., defining operations concretely over integers).
+Additionally, there is a persistent temptation to introduce new representations of existing mathematical objects that are easier to work with for a particular application, which comes at the cost of duplicating the theory for the new representation.
+Theorem provers like Isabelle [@paulson1994isabelle] and Coq [@coq2024manual] approach these problems by having very minimal standard libraries and encouraging the use of external libraries developed by the community, which reduces the emphasis on ensuring the existence of canonical definitions for certain concepts, at the cost of lack of interoperability between variabous packages.
+On the other hand, like `agda-stdlib`, MathLib [@van2020maintaining] for Lean aims to provide a repository of canonical definitions. 
 
 A second challenge is that Agda was the first major ITP to fully embrace dependently-typed programming as the default.
-With the exception of Idris, a more recent entrant to the field [@brady2013idris], other major theorem provers either do not support dependent types or encourage them only to be used sparingly.
-In contrast, nearly everything in the Agda standard library makes use of dependent types, with proofs consisting of evidence-bearing terms of the relevant dependent types.
+With the exception of Idris, a more recent entrant to the field [@brady2013idris], other major theorem provers either do not support dependent types or encourage spare usage.
+In contrast, nearly everything in `agda-stdlib` makes use of dependent types, with correctness-related invariants being closely integrated with definitions.
+Furthermore most proofs consist of evidence-bearing terms for the relevant types, rather than being "irrelevant".
 As a result, the library provides relatively sophisticated features like polymorphic n-ary functions [@allais2019generic], regular expressions which provide proof of membership when compiled and applied, and proof-carrying `All` and `Any` predicates for containers [citation?].
-While this provides powerful tools for users, learning how to design such a large-scale, dependently-typed library is an on-going journey.
+While this provides powerful tools for users, learning how to design such a large-scale, dependently-typed library is an on-going journey. `agda-stdlib` is the first library to tackle this challenge.
 Relatedly, the standard library has been used as a test bed for the design of the Agda language itself, as evidenced by the library's inclusion of three different notions of co-inductive data types.
 
 Agda’s unique support for dependently-parameterized modules has also significantly influenced the library’s design.
-Although type classes are a common mechanism for creating interfaces and overloading syntax in other functional languages such as Haskell [@haskell2010], the Agda standard library has so far found little need to use them extensively.
-While Agda supports a very general form of type classes via instance search, the ability to use qualified, parameterized modules as first-class objects appears to reduce their necessity compared to other functional languages.
+Although type classes are a common mechanism for creating interfaces and overloading syntax in other functional languages such as Haskell [@haskell2010], and other ITPs like Coq and Lean's MathLib use then extensively as a core feature of their design, the Agda standard library has so far found little need to use them much.
+While Agda supports a very general form of instance search, the ability to use qualified, parameterized modules as first-class objects appears to reduce their necessity compared to the languages mentioned above. 
 Additionally, module parameters enable the safe and scalable embedding of non-constructive mathematics into a constructive system.
-Since Agda is entirely constructive, the vast majority of the standard library is also constructive.
-However, the library provides the option to perform non-constructive, classical reasoning, such as the law of excluded middle, by passing the relevant axioms as module parameters.
-This allows users to write such code without directly having to postulate the non-constructive axioms, which would prevent them from using the code with the `--safe` compiler flag.
+Since Agda is entirely constructive, the vast majority of `agda-stdlib` is also constructive.
+Non-constructive classical reasoning can be achieved by passing the relevant axioms as module parameters.
+This enables users to write provably 'safe' non-constructive code, i.e. with having to *postulate* non-constructive axioms.
 
 # Testing
 
-One of the advantages of creating a standard library for an ITP is that proving the correctness of the defined operations is an integral part of the library itself.
-As a result, there is no need for test suites to verify functional correctness.
-However, the library’s test suite does address two critical areas.
-The first area is the foreign function interface with the underlying operating system (e.g., reading from the command line, file access, timers).
-Since the correctness of the bindings to external libraries or the underlying OS' primitives cannot be reasoned about in Agda itself, these operations are included in the test suite.
+One of the advantages of ITPs is that correctness proofs are regarding as an integral part of creating a collection of structures and operations.
+Thus there is no need for test suites to verify functional correctness.
+However the library’s test suite does address two critical areas.
+First is the foreign function interface with the underlying operating system (e.g., reading from the command line, file access, timers).
+Correctness of bindings to an external library or the underlying OS' primitives cannot be reasoned about in Agda itself, these operations are tested externally, i.e. in a test suite.
 The second area is performance.
-The performance of a program cannot be analysed within Agda, making it necessary to include performance tests.
-Although the library currently includes a few performance tests, this has not so far been a major priority for the community, and remains an area in need of further work.
+Performance also cannot be analysed internally, making it necessary to include performance tests.
+This part of the test suite is sparser, as this has not yet been a major priority for the community.
 
 # Notable achievements in version 2.0
 
-This short paper outlines the state of version 2.0 of the Agda standard library, in which we believe we have successfully addressed some of the significant design challenges present in version 1.0. Key improvements include:
+We outline the state of version 2.0 of `agda-stdlib`, where we believe we have successfully addressed some of the significant design challenges present in versions 1.0-1.7. Key improvements include:
 
 - Minimized Dependency Graphs: We have reduced the depth of dependency graphs within the library, ensuring that the most commonly used modules rely on fewer parts of the library. This change has resulted in significantly faster load times for users during interactive development.
 
-- Standardisation of Mathematical Object Construction: We have standardised the construction of mathematical objects such as groups, rings, orders, equivalences, etc., from their sub-objects, enhancing consistency and usability.
+- Standardisation: We have standardised the construction of mathematical objects such as groups, rings, orders, equivalences, etc., from their sub-objects, enhancing consistency and usability. We have also worked on standardizing morphisms of such objects.
 
 - Introduction of a Tactics Library: We’ve introduced a small but growing tactics library. Experiments have shown that these tactics are currently slower than those in comparable systems, indicating a potential area for future improvements in Agda itself.