search

coq / stdlib2

GNU Lesser General Public License v2.1
39 stars 9 forks source link

What should go in stdlib? #7

Open gmalecha opened 6 years ago

gmalecha commented 6 years ago

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?

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

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

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

Zimmi48 commented 6 years ago

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

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

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

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

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

spitters commented 6 years ago

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

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

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

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

Zimmi48 commented 6 years ago

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