search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
584 stars 238 forks source link

Improve documentation of modules #595

Open alhassy opened 5 years ago

alhassy commented 5 years ago

List of needed documentation

Other

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

@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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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

EdNutting commented 5 years ago

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)

MatthewDaggitt commented 5 years ago

Okay well it looks like the vague consensus is to try and improve the number and quality of Example files throughout the library. If at some point someone volunteers to get something more elaborate set up then at least the Examples file will provide a good starting point.

nad commented 5 years ago

Each (file) module could have a (file) submodule .Example explaining the use of the primitives.

The idea was to use the modules under README for things like that. Only the modules under src are "exported" from the library. In either case there is the problem that the current highlighting mechanism does not make it easy to link from X to README.X or X.Example. Perhaps something could be done about that.

I sometimes refer to names that are not in scope in my code, like in "This definition satisfies property X, see Some-other-module.the-definition-satisfies-X". Comments of that kind easily get out of date. It would be nice with some way to ensure that the thing that is referred to actually exists. The same mechanism could perhaps be used to include pointers to modules with documentation.

MatthewDaggitt commented 5 years ago

Added a list of documentation files it would be good to have to the top of this issue. Obviously not exhaustive so feel free to add requests.

If anyone would like to volunteer to write any of them, please do!

pnlph commented 5 years ago

The README folder follows the same strcture as src, right? Eg Properties.agda could have its own file in Nat folder? Right now its README examples are in Nat.agda

MatthewDaggitt commented 5 years ago

The README folder follows the same strcture as src, right? Eg Properties.agda could have its own file in Nat folder? Right now its README examples are in Nat.agda

Yes, it could in theory. However I'm not sure it's worth creating a README file for every single file in the library. I think it's a lot more cohesive to have a single file for Data.X, Data.X.Properties, Data.X.Base, Data.X.Relation etc. That way, that's the definitive file to go read when you want to learn about X. This also reflects our eventual goal to have Data.X exporting nearly all the main submodules, Data.X.Properties etc. in addition to Data.X.Base.

pnlph commented 4 years ago

I still do not know which convention was adopted if the README or the .Example approach?

I suggest making a decision about this and then creating the corresponding stdlib documentation guidelines. Once the guidelines are clear it will be easier for everybody to volunteer and commit.

We probably do not have to do this from scratch, the guidelines could lean on Haddock documentation and markup guidelines.

pnlph commented 4 years ago

I just saw that from the conclusion of #613 that the .Example approach is preferred, so the README folder should actually disappear?

With respect to the conclusion of #595, would it make sense to turn all the README files into Example files and do away with the README folder entirely? It seems confusing to have two parallel sets of documentation.

Originally posted by @MatthewDaggitt in https://github.com/agda/agda-stdlib/issues/613#issuecomment-463994304

gallais commented 4 years ago

It feels wrong to use #613 to justify coming to a decision in #595 when #595 was used to justify coming to a decision in #613.

Now that README/ has been revamped and follows a structure similar to the main library, I think discoverability has been improved quite a bit.

pnlph commented 4 years ago

Oh sorry, i mistakenly took for granted that, because #587 is abandoned, the other option was the case.

Then the README approach still holds, right?

MatthewDaggitt commented 4 years ago

Then the README approach still holds, right?

Yes, we've been adding extensively to the README section recently and not adding any new .Examples files so I think we can view that as a decision!