Stakeholders

[JacquesCarette]

(More philosophy... Caveat: a proper write-up will likely need multiple passes)

Who are we designing this library for? In part, obviously, ourselves, i.e. the people who contribute code to it have a stake of some sort to do so. But the question isn't really about the people involved (end-users included), but rather the roles they inhabit. Most people inhabit multiple roles, and their desires while in that role changes. The main roles that I see:

• End-user: At the end of the day, we would really like to have (happy) users of the library. I see the 'end-user' role as someone who just wants to get things done. They have needs (being able to find things, understanding how to use it once they find it, understanding when things fail). Users also vary widely in sophistication (i.e. background knowledge that they possess.) To me it is entirely appropriate for the library to have different 'zones' which presupposes rather different knowledge bases from the user. Of course that also means that such information should be flagged and findable. Long-time users want stability, so that their work is not continuously obsoleted. Of course, if the library gets 'stale' (because alternate libraries did not make the same design mistakes, or offer better tools), stability may become secondary.
• Maintainer: There are two classes of 'maintainer' roles, that occupied by humans and that occupied by tooling and automation.
  • Human: Their main concern is to stay sane. Being able to understand the rules (style guide, etc), the overall organization are important. Scale is also a huge issue: if all work requires tedious edits everywhere, maintenance efficiency drops quickly. So human maintainers tend to like a lot of abstraction (it reduces effort and code bloat). For scalability, small focused modules are best.
  • Tooling: CI, linting, documentation generators, tests, and eventually much more. This relies on the library being organized and following a variety of conventions that the tooling can cue on.
• Developer: As a separate role from 'Maintainer' as the emphasis is different, i.e. new (D) vs pre-existing (M). There is a lot of overlap in people between those roles. The concerns are different: how to integrate into existing library, how to get it to the level that it will be integrated, and so on.
• Learner: Again, there are different classes of learners, with different desires.
  • Of Agda: I think it should be a reasonable thing for learners of Agda to read lots of stdlib and learn decent style from it. However, see above on 'assumed background'. We should not cater to 'newbies' in the whole library! But unless there are strong reasons to do so, we should not make simple things obscure either.
  • Of Mathematics: A library of mathematics is meant to support usage (so the external API should make sense and be at the same level of mathematics as what it provides) but is a rotten place to learn. The internals of a library should be free to use whatever advanced feature it wants, without ever having to be apologetic for it.
  • Of Implementation Techniques: While never being apologetic for implementation means, someone who has the right background should be able to read stdlib source and learn (something) from it.
• Researcher: Again, this divides up.
  • User: basically builds their work atop the library. They want some level of stability, just like end users. But their threshold tends to be different (i.e. a bit more willing to accept instability, as long as things work when they pin to old versions.)
  • Of Mechanized Mathematics: this is a combination of end-user and developer.
  • Meta-mathematician: this is a 'learner' of techniques, but much more systematic. i.e. rather than for themselves, is looking for patterns of various kinds. Has very specialized needs... that are too much of a burden to cater to. [Main reason to mention: high density of overlap between current maintainers and this role.]

There are also roles that I think we don't need to worry about:

• AI: None of their concerns should concern us.
• Funders: While we should not repel them, taking their concerns into consideration while developing the library does not make sense to me.

[jamesmckinna]

Is there a way to accommodate learners/beginners (more) via the README hierarchy? Most are explicitly didactic, but often about rather detailed design philosophy than 'this is what module sub-hierarchy affords, and how it works, and why you should use it like this, and how' although to be fair, some if that rubric us covered, but not necessarily at a 'beginner' level.

So: what/where should that be?

Hidden question: can we (re-)organise stdlib so that it functions also as a (self-)teaching resource/textbook-of-itself?

Cf. The discussion in #595 #603 where a particular (unimplemented!) affordance is described (on-the-fly expansion of definitions to aid understanding) which seems to speak to a concern which cuts across all kinds of stakeholder. As well as identifying these kinds, we might do well also to speculate on what kinds of such additional affordances might attach to role.

[JacquesCarette]

One can certainly layer things on top of stdlib that is better suited to learners/beginners. PLFA does a decent job at it.

We could try to (re-)organize stdlib so that one could self-learn from it assuming the learner has an appropriate knowledge base. That's really the hard part, deciding what that ought to be.

For the various affordances, to me this seems like IDE features. We should not make the library 'fight' a good IDE, but should also not make sub-optimal decisions because a good IDE does not yet exist!

[gallais]

One stakeholder that is missing I think are the developers of Agda itself who use
the standard library (among other things) to detect regressions, measure performance
improvements, decide whether a feature can be excised from the codebase or not.