What should go in stdlib?

[gmalecha]

In addition to the important question of what goes in the prelude, another question is: "What goes in the library?"

Is there a list somewhere of the functionality we will include?

• bool/numbers
• list/option/sums/products
• string, ascii
• finite sets
• finite maps
• vector, hlist, member, fin

How about concepts (e.g. common type classes from Haskell)?

• functor/applicative/monad
• monoid/semi-group
• lens
• classes for maps, sets, etc
• decidable equality

I imagine that some of the things that I've listed here should be split into other libraries (luckily with opam/nix it should be easy). Other pieces should be in here. So, where will we draw the line?

Personally, I lean a bit towards a collection of repositories that focus on individual concepts but standardized in some way, though small repos have their own downsides as well

[gmalecha]

@Zimmi48, Is there a forum for the discussion? There are lots of things marked "to discuss" but when/where do they get discussed?

[Zimmi48]

@gmalecha The place to discuss is these issues AFAICT. FTR there was an initial WG discussion raised by myself (Oct 4th, 2017) about the standard library. Here it is: https://youtu.be/euwh_ToBiYo?t=2h6m54s
And here's where, towards the end of this discussion, @maximedenes really launches the stdlib2 project: https://youtu.be/euwh_ToBiYo?t=2h38m29s

[herbelin]

Everything listed above seems indeed relevant for a standard library. Indeed, compared to the current standard library who tends to miss them, I think that basic concepts such as monading programming, orders, adjunctions, boolean reflection, groupoid structure of equality, telescopes, enumerability, cardinality, set-theoretic operations, etc., etc. should occur somewhere, and, somehow, with standardized notations.

I believe that we should start from somewhere. @maximedenes, do you have a calendar? For instance, we could start from the list library on which we have a lot of contents available dispatched over many various contributions? Or, to start from a kind of library which is missing most, e.g. for monadic programming?

Personally, I lean a bit towards a collection of repositories that focus on individual concepts but standardized in some way, though small repos have their own downsides as well

Since I hardly see one person alone able to rebuild a standard library in even, say, a one-year schedule, a collection of repositories (managed by different groups of people?) would maybe indeed be a good way to proceed.

[spitters]

I imagine that one would somehow like to compare with the stdlibs of ocaml and haskell.
The Vocal project aims to provide a verified basic library for ocaml.
https://vocal.lri.fr/
https://hal.inria.fr/hal-01561094

Maybe it is of some use?

I seem to recall a similar effort for haskell, but I cannot currently find it.

[herbelin]

The Vocal project aims to provide a verified basic library for ocaml.

This is a very good initiative. (And somehow, FMaps and FSets were among the first experiences motivated by verifying components of OCaml's standard library.)

I wonder what will be their approach for partial functions, such as the head of a list: returning a result in the exception monad with a Failure "hd" exception (added: or, probably better, a proof of emptiness), giving non emptiness as a precondition, or returning a default value (when the domain is known non-empty). The three styles have different advantages, depending on situations, and I never could make up my mind on whether we should give a preference to one or two or provide all of them. (In a system supporting undefinedness in direct style, we could even have a fourth variant returning the "undefinedness".)

[spitters]

I guess the only way to find out is to ask @backtracking .

[spitters]

I was thinking about this project by @jwiegly
https://github.com/jwiegley/coq-haskell

and @swierich 's project has a similar aim.
https://github.com/antalsz/hs-to-coq

[gmalecha]

@herbelin for the Coq prelude, I would expect to have the error monad definition as the primitive. The default variant can be written from that.

@spitters there is no shortage of "alternative standard libraries" for Coq these days. It would be a great benefit to the community to get a retrospective on their experiences and use that as the basis for this project. I imagine that a good chunk of code and proofs could be adopted from existing libraries as well.

[gallais]

I imagine that one would somehow like to compare with the stdlibs of ocaml and haskell.

It's probably also worth looking at the ones for other theorem provers. See what they implement
but also what they prove. Be it (alphabetically):

• Agda https://github.com/agda/agda-stdlib
• F* https://github.com/FStarLang/FStar/tree/master/ulib
• Idris https://github.com/idris-lang/Idris-dev/tree/master/libs
• Lean https://github.com/leanprover/mathlib

I know I'll be looking for things to steal from y'all. :)

[Zimmi48]

• Lean https://github.com/leanprover/mathlib

mathlib (in Lean) isn't technically a standard library and from what I heard from other experts, Lean isn't (yet) to be considered as a source of inspiration for library development...