Add containers.agda-lib to lib directory

[HeinrichApfelmus]

This pull request adds a library lib/containers/containers.agda-lib which imports large chunks of the Data.Map and Data.Set modules from the containers package, including proofs.

Comments

• I have chosen to not add the prefix Haskell. to the module names Data.Map.Prop and Data.Set.Prop, because:

  • Strictly speaking, these modules do not correspond to an existing Haskell module, …
  • … but the properties proven have value as exported Haddock comments. In other words, once we can export properties to comments (related to Preserve comments #114), we can later make Data.Map.Prop part of, say, a containers-prop.cabal package and make the proven properties available as a Haskell package. (The properties cannot be reused for proofs in Haskell Land, but at least they can be exported as "this has been proven!" to Haskell Land.)

• I was not quite sure whether to choose the name Data.Set.Prop or Data.Set.Law. John Hughes appears to use both "law" and "property" synonymously, while using "law" more often. Perhaps a good distinction is that the "laws" are closer to being complete while "properties" are mostly "haphazard" consequences.

[omelkonian]

Great stuff!

What is urgently missing before we can merge is a test suite that ensures we get the desired Haskell output.

Other than that, you've imposed a rather idiosyncratic style throughout that should be reversed in favour of consistency with the rest of the repo. It'd be easier if I pushed a styling commit after yours if you gave me access to your branch. Otherwise, let me know if you need explicit indications.`

[HeinrichApfelmus]

Thanks! 😊

What is urgently missing before we can merge is a test suite that ensures we get the desired Haskell output.

As this code binds an existing Haskell library, it does not produce any Haskell output by itself. I suppose the next best thing is that we add an Agda module that imports Data.Map and has non-trivial Haskell output, so we check that Data.Map is imported correctly?

Or do you mean the "Haddock output" for e.g. Data.Map.Prop that I have alluded to? That would require more support from agda2hs, e.g. by moving functionality from agda2hs-fixer to agda2hs.

At the very least, we can check in CI that the proofs in Data.Map.Prop and Data.Set.Prop are correct!

Other than that, you've imposed a rather idiosyncratic style throughout that should be reversed in favour of consistency with the rest of the repo. It'd be easier if I pushed a styling commit after yours if you gave me access to your branch. Otherwise, let me know if you need explicit indications.`

Yeah, sorry about that. 😅 I like to squander vertical space for the purpose of Haddock output. I also like rewrite — it saves a lot of time as opposed to explicit cong and equational reasoning.

This branch is coming from a fork, I have invited you to my fork. (Alternatively, you could invite me to the original repo, I don't mind either way).

[omelkonian]

Yeah, sorry about that. 😅 I like to squander vertical space for the purpose of Haddock output. I also like rewrite — it saves a lot of time as opposed to explicit cong and equational reasoning.

OK, you have plans for producing Haddock, so that makes sense now. Then it's OK to leave the style as is for now, and revisit later if needed.

Perfectly fine to use rewrite, just make sure you group together with rewrite H1 | H2 | ... | Hn.

[omelkonian]

As this code binds an existing Haskell library, it does not produce any Haskell output by itself. I suppose the next best thing is that we add an Agda module that imports Data.Map and has non-trivial Haskell output, so we check that Data.Map is imported correctly?

Exactly! A simple test that uses a handful of operations on sets and maps and typechecks correctly with proper imports.

Or do you mean the "Haddock output" for e.g. Data.Map.Prop that I have alluded to? That would require more support from agda2hs, e.g. by moving functionality from agda2hs-fixer to agda2hs.

Nah, it's fine to leave this for the future.

[HeinrichApfelmus]

Exactly! A simple test that uses a handful of operations on sets and maps and typechecks correctly with proper imports.

I have now added a commit with two modules Test.Agda2Hs.Data.Map and Test.Agda2Hs.Data.Set that do this.

I have decided to put them in a containers-prop.cabal cabal package, because:

• When exporting Data.Map.Prop as Haddock in the future, the plan is to do it as part of a package containers-prop.cabal.
• This setup keeps the CI simple — cabal takes the place of make rules.

[omelkonian]

Excellent!!