Improve documentation of modules

[alhassy]

List of needed documentation

• README.Algebra
• README.Axiom
• README.Category
• README.Codata
• README.Data
• README.Data.Nat.Induction (exists but doesn't do much explaining or go into <-wellFounded)
• README.Function
• README.IO
• README.Induction
• README.Reflection
• README.Relation

Other

• Syntax guidelines

Original post

tldr: It's hard to find stuff in the standard library; and when you do find it,
it's not always clear how to use it, where to use it, or why it's defined the way it is!

A prime hindrance to a successful library is the inability of its users
to locate desirable utilities or documentation about them, thereby being
forced to use extra third-party tools to accomplish such tasks.

The de facto IDE for Agda is Emacs. It comes with the ‘jump to definition’
utility, which unfortunately requires the user to actually inspect the definitions
of functions since the standard library is unreasonably poorly documented.
The trouble is multiplied by the exceedingly fast growth of the library itself,
thereby making it harder to locate material let alone find out how to use it.

In contrast, Haskell's community provides well-documented code which it
uses to create online information hubs. It is a shame that Agda is heavily
influenced by the Haskell community, yet not so much in this pragmatic sense.

Perhaps we could standardise documentation for the library similar to how Haskell does it,
or --since Agda is primarily Emacs-based-- go for a more literate approach and use Org-mode!

[MatthewDaggitt]

I agree, improved documentation is strongly desirable.

I personally don't have much experience with either the Haskell documentation or the emacs Org-mode. I'd be interested in further opinions/suggestions by regular users on what they'd like to see?

[gallais]

I find it a lot easier to push documentation following specific demands for clarification
rather than abstract calls to actions. Otherwise I am overwhelmed by the possibilities
and don't really know where to start.

If we do start listing target modules people are interested in, then I'll happily contribute.

[EdNutting]

I would greatly appreciate examples on how to use the various things for proving properties of Lists/Vecs using Propositional Equality and Any/All - I seem to spend a lot of time struggling with writing proofs very manually about functions over lists/vecs and I guess things would be easier if I knew how to use something more sophisticated than subst (which I'm still not confident in using).

Examples in the docs of how but more importantly when a given abstraction/general property may be used would be very helpful.

[ice1000]

A very very personal opinion from a by-passer:

The short-hands for functions in this lib (like Asymmetric, Trans, Associative, Commutative) are actually making the library unreadable -- I'd say forall a b -> a + b = b + a is more readable than Commutative _+_, especially for those who want to use these properties as functions and call them.

BTW there's a clickable website which is similar to a document here: https://agda.github.io/agda-stdlib/

[xekoukou]

@ice1000 I agree that they are very difficult to read. On the other hand, they do need to be defined this way so as to have a uniform approach to all similar properties.

In my opinion , the solution should be to be able to interactively decide on the normalization of subexpressions. (the actual expression remains Asymmetric but you see the normalized expression.)

Most of the problems can be solved by creating a web based interactive environment. And turning agda into a library so as to create a server , and so that anyone can add extensions to the server with additional interactive functionality.

This is the future of programming in my opinion.

[MatthewDaggitt]

I would greatly appreciate examples on how to use the various things for proving properties of Lists/Vecs using Propositional Equality and Any/All - I seem to spend a lot of time struggling with writing proofs very manually about functions over lists/vecs and I guess things would be easier if I knew how to use something more sophisticated than subst (which I'm still not confident in using).

Okay once I get the main stuff for v1.0 out the way, I'll try and come up with some better examples in README for the more common datatypes. If we later decide to go down a different route for the documentation then at least they'll be available to copy across.

The short-hands for functions in this lib (like Asymmetric, Trans, Associative, Commutative) are actually making the library unreadable -- I'd say forall a b -> a + b = b + a is more readable than Commutative +, especially for those who want to use these properties as functions and call them.

Hmm this one is trickier. I agree with you that knowing exactly how to use these properties (or trying to give implicit arguments) can be very tricky as the names, ordering and type of arguments are all hidden. On the other hand @xekoukou is right, the use of them is important in ensuring consistency, particularly those that are then packaged up in records. I'm not sure what the answer is within the existing setup. Maybe we could start unfolding a few of the properties that have less obvious definitions.

[JacquesCarette]

In my opinion, what is needed is that the source of the library use Commutative etc, even some of the weirder ones, but when users inspect the type of those fields, what gets shown is the expanded version. What would be required for that would be some evaluation annotation, I guess, that says that this type must always be normalized.

[andreasabel]

I second the addition to examples to the library.
Each (file) module could have a (file) submodule .Example explaining the use of the primitives.
Usually, when adding new functionality to the library, one has a use case (in mind or worked out), and this would amount to put it down with the new functionality.
I would not mind if 80% of the library source would consist of .Examplemodules. They do not need to be compiled always and they export nothing.

[JacquesCarette]

The .Example idea is indeed quite good. If such a convention is adopted (i.e. the tooling supports it), then it would be best to let the examples develop organically. I definitely think it would be a bad idea to mandate anything in that direction. The Agda ecosystem is not yet large enough for that. [Rant about the various critical sizes of a software community before various quality-related protocols can safely be added omitted; but CRAN is a good case of the good things that happen when you do it right.]

[emilyhorsman]

Perhaps we could standardise documentation for the library similar to how Haskell does it,
or --since Agda is primarily Emacs-based-- go for a more literate approach and use Org-mode!

(Emphasis mine.) Org mode would be challenging until agda/agda#2837 is resolved.

Make Agda Literate Again!

In speaking of programming communities: communities which condone MAGA jokes are not ones many people feel safe participating in.

[gallais]

To clarify: 👍 on the second part; I don't have any opinion wrt org-mode vs. basic comments.

[EdNutting]

Proposal: To rename the issue to:

Improve documentation of modules

Or:
Improve documentation of common abstractions
(Though that might be worth splitting into a separate issue)