Skip to content

Commit

Permalink
tweaks: bib, type class section, list of contributors
Browse files Browse the repository at this point in the history
  • Loading branch information
jamesmckinna committed Sep 6, 2024
1 parent e064228 commit 1191437
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 4 deletions.
3 changes: 2 additions & 1 deletion paper/paper.bib
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,7 @@ @misc{agda-stdlib-v2.0

@misc{agda-stdlib,
title = {{The Agda standard library}},
year = {2007--present},
url = {https://github.com/agda/agda-stdlib},
note = {A full list of the contributors can be seen under \url{LICENCE.md} at the above {URL}}
note = {A full list of the contributors can be seen under \url{LICENCE} at the above {URL}}
}
6 changes: 3 additions & 3 deletions paper/paper.md
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ Relatedly, `agda-stdlib` has been used as a test bed for the design of the Agda

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], and other ITPs like Coq and Lean's MathLib use them extensively as a core feature of their design, `agda-stdlib` has so far found little need to exploit such an approach.
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.
While Agda supports a very general form of instance search, the ability to use qualified, parameterized modules as first-class objects appears to reduce the need for it 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 `agda-stdlib` is also constructive.
Non-constructive methods, such as classical reasoning, can be achieved by passing the relevant axioms as module parameters.
Expand All @@ -122,7 +122,7 @@ This part of the test suite is sparser, as this has not yet been a major priorit

# Notable achievements in version 2.0

We outline the state of `agda-stdlib` version 2.0 [@agda-stdlib-v2.0], where we believe we have successfully addressed some of the significant design challenges present in versions 1.0-1.7. Key improvements include:
We outline the state of `agda-stdlib` version 2.0 [@agda-stdlib-v2.0] (with HTML-annotated sources at: \url{https://agda.github.io/agda-stdlib/v2.0/}), 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.

Expand All @@ -143,6 +143,6 @@ Jesper Cockx and
Andrea Vezzosi,
without whom Agda itself would not exist.

The authors of this paper are listed approximately in order of contribution to the library.
The authors of this paper are listed approximately in order of contribution to the library. A full list of contributors to `agda-stdlib` may be found in the `LICENCE` in the GitHub source tree.

# References

1 comment on commit 1191437

@jamesmckinna
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We might now have room for a (very) short additional paragraph (2-4 lines?), and/or a couple of additional references (eg: one for Containers @gallais ?).

Please sign in to comment.