Refactor base library structure and port additional Haskell functions

[loki259]

Summary

This PR reorganizes large parts of the Agda2Hs base library to better separate primitive definitions from higher-level utilities and to align the module structure more closely with the hierarchy found in the Haskell library.

In addition to the structural refactoring, several modules were expanded with additional definitions ported from Haskell.

Main changes

• Introduced new modules mirroring the Haskell version of the library:

  • Added Data.String
  • Added Data.Functor
  • Added Data.Foldable
  • Added Data.Traversable
  • Added Control.Applicative

• Refactored Prim modules so they mainly contain class definitions and minimal primitive functionality:

  • Moved _<$>_, _<&>_, _$>_, void from Prim.Functor to Data.Functor
  • Moved _=<<_, mapM₋, sequence₋ from Prim.Monad to Control.Monad and Data.Foldable and moved bindIO from Prim.Monad to Prim.IO
  • Moved lines, words, unlines, unwords from Prim.String to Data.String
  • Moved all functions in Prim.List except _++_, head, last, tail, init, map to Data.List
  • Moved lengthNat from Prim to Prim.List
  • Moved reverse, _!!ᴺ_, _!!_, lookup from Prelude to Data.List

• Added additional type classes and instances and refactored existing type class
  definitions:

  • Reworked IO instances (Functor, Applicative, Monad) so they are now defined explicitly in terms of bindIO and returnIO.
  • Added Alternative class record and instances (defined in new module Prim.Alternative)
  • Added MonadPlus class record and instances (defined in new module Prim.MonadPlus)
  • Moved MonadFail from Prim.Monad into its own module Prim.MonadFail and added instance for IO
  • Added MonoidFirst and MonoidLast Monoid instances in Prim.Monoid
  • Refactored Applicative to include liftA2 as additional method (with corresponding default record)
  • Refactored the method set of Foldable to match the Haskell version (moving any, all, and, or, concat, concatMap, notElem to Data.Foldable and adding fold, foldMap', foldr', foldl', foldr1, foldl1, maximum, minimum)
  • Moved Semigroup from Prim.Monoid into its own module Prim.Semigroup
  • Introduced submodules for instances of type classes

• Expanded several modules with additional definitions ported from Haskell (still missing definitions are listed in a comment at the end of the respective file):

  • Expanded Control.Monad (also changed signature of existing guard definition to match the Haskell version)
  • Expanded Data.List (also updated the definition of nub and removed some property proofs based on the outdated definition)
  • Ported Data.Functor
  • Ported Data.Foldable
  • Ported Data.Traversable
  • Ported Control.Applicative
  • Expanded Prelude by updating module imports (also updated documentation of missing definitions from the Haskell prelude)

• Updated imports and reexports throughout the codebase to reflect the new module structure

Motivation

The goal of these changes is to make the structure of the library more consistent with the organization familiar from Haskell, while keeping the Prim modules focused on primitive definitions. This separation also makes it easier to extend the library with additional standard definitions in the future and avoids many cyclic module dependencies when reusing definitions from other parts of the library.

Notes

Because many of the refactorings depend on each other (often due to running into problems with cyclic imports), the changes are grouped into a single commit.

[jespercockx]

Thank you for the nice PR! Generally things look good but I have a few small requests for changes. Also, could you please investigate the failure on CI (at least the non-Nix ones).

[loki259]

Also, could you please investigate the failure on CI (at least the non-Nix ones).

I could use some help in fixing the issues responsible for the remaining test failures (as already posted on Zulip):

When I reexport definitions in another module (which I did with a lot of the newly ported functions that are part of the Prelude but needed to be defined elsewhere) the Haskell files produced by Agda2Hs seem to import those definitions from the module where they were originally exported instead of from the module where the corresponding Agda file imports them from.
Specifically, there are some tests that fail now because while the Agda file imports everything from the Prelude the compiled Haskell version of the file imports identifiers from Control.Monad or Data.List for example (although the relevant identifiers are reexported from the Prelude and importable from there on the Agda side).
Is there something I am not aware of when it comes to how reexports are handled in Agda2Hs (or in Agda generally)? I read the imports section in the documentation but I couldn't find anything on this matter.

Another issue I have is that type class instances are seemingly not reexported unless I list the instances explicitly along with the class definition in the using clause of the public import. Listing them is of course not the end of the world but it will make adding new instances a bit cumbersome in the future because the import lists for the respective module need to be adjusted wherever the new instance should also be reexported.
Is there a way around this? Can I somehow explicitly export the instances all at once?

[jespercockx]

You're not missing anything, proper re-exports are still on the todo-list (see #126). As a workaround I guess you could replace the re-exports by postulates for now, possibly together with an equality proof that these postulates are equal to the real versions (this is not a very nice solution but I can't really think of a better one atm).

For exporting instances, I don't think it should be necessary to explicitly import them at all, just importing the module should be sufficient to bring them in scope for instance resolution on the Agda side. Or is the problem that they are somehow not exported on the Haskell side?

[loki259]

Oh okay, I didn't see that there was already an issue for this reexport problem.
Your postulates workaround makes sense (although I am not sure where to put those equality proofs) but wouldn't it be easier to just import the relevant definitions qualified and to then define properly exported aliases to them? For example, instead of having open import Haskell.Data.List public using (or) in the Prelude module we could add

or : ⦃ Foldable t ⦄ → t Bool → Bool
or = Haskell.Data.List.or

This avoids postulates and seems a bit simpler to me. What do you think?

Regarding the instance exports: There is no problem on the Haskell side but on the Agda side I cannot just use open import Haskell.Control.Monad to make use of the module's guard function, for example, because it depends on instances of the Alternative class being in scope. Those instances are imported in Control.Monad but apparently they are not reexported by default.
I can of course add a second import statement that exposes the instances from Prim.Alternative directly to the Agda file, but I think it would be cleaner if the Agda version would only need to import modules of functions that it uses (not modules where instances are defined, just like the Haskell version).
I already validated that I can achieve that by explicitly reexporting all instances of the Alternative class from Control.Monad but I was wondering if there is a better way to go about it since this approach forces us to update the list of exported instances in multiple files whenever a new instance is added in the source module. Can I somehow export all the instances at once?

[jespercockx]

This avoids postulates and seems a bit simpler to me. What do you think?

Yes, if that works it's a much better solution!

I already validated that I can achieve that by explicitly reexporting all instances of the Alternative class from Control.Monad but I was wondering if there is a better way to go about it since this approach forces us to update the list of exported instances in multiple files whenever a new instance is added in the source module. Can I somehow export all the instances at once?

I believe it should also be sufficient to just give a name to the module that you want to re-export the instances from, e.g.

import Prim.Alternative
module Alternative = Prim.Alternative

Could you give that approach a try to see if if works?

[loki259]

Unfortunately, my approach of introducing explicit alias definitions in place of reexports didn't work as well as expected:
There seem to be test cases where Agda2Hs introduces a qualified Prelude import for some definitions although the Prelude is already imported implicitly. This happens even when there is already another qualified Prelude import.
There is also a bigger problem: In contrast to using Agda's builtin reexport mechanism, the explicit aliasing approach creates import conflicts in terms of name collisions on the Agda side whenever a different module with a subset of the definitions from the Prelude is also imported (for example when importing the Prelude and Control.Monad).
From what I can see these two problems are responsible for about half of the current test failures. There are, however, also a few tests where I have really no idea what broke them and why certain definitions that are clearly exported from the Prelude seem to no longer be in scope in these files.
Anyways, even if I was able to identify what causes these other tests to fail, I don't think we can make the explicit reexports work without fixing some of the Agda2Hs internals related to #126 first. This conclusion probably also holds for your suggestion of using postulates. Maybe you can take a look at the failing test cases yourself and tell me if you agree with my assessment.

On the positive side, I found a solution for the instance export problem:
I first implemented your suggestion of using named modules when importing type class modules but that created a lot of name conflicts and brought me to the idea of instead exporting the instances as part of Instances submodules on the side of the type class modules. This avoids the need for finding a new name for the whole type class module whenever definitions need to be imported and one can instead just explicitly import the Instances submodule (optionally renaming that submodule in case of conflicts with Instances submodules from other type classes).

[jespercockx]

Ah, that is unfortunate. It seems this is blocked on implementing re-exports properly then. I would like to look at it but I also have a few open issues in Agda itself I need to fix first for the release of 2.9, so I'm not sure when I'll be able to get to it. In case anyone else want to give it a go, I would be happy to provide some pointers.