What should go in stdlib? about stdlib2 HOT 10 OPEN

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. :)

from stdlib2.

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

from stdlib2.

@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

from stdlib2.

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.

from stdlib2.

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.

from stdlib2.

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".)

from stdlib2.

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

from stdlib2.

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

from stdlib2.

@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.

from stdlib2.

• 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...

from stdlib2.