Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding an implementation of the Data.Map module #291

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

viktorcsimma
Copy link
Contributor

It can be found in Haskell.Data.Map. I've also added a mechanism to import Haskell.Data.Something modules as Data.Something.

@jespercockx
Copy link
Member

Thank you for this PR, I think it's a great idea to add support for Data.Map to agda2hs. However, I have some questions about the intended purpose of this PR:

  • If the goal is to provide bindings to the existing Data.Map library from the containers library, then I would argue that we should not provide an implementation but just postulates that provide the API (plus possibly the properties of maps). By providing the full implementation, we would encourage people to rely on those implementation details, which I don't think is a good idea.
  • If the idea is to provide an agda2hs re-implementation of Data.Map, then there should be COMPILE AGDA2HS pragmas so that we get actual Haskell code. (And then also this should probably not be part of this repository.)

What you did here is what we have done for the Haskell prelude, but I do not think this approach makes sense for other packages (such as containers here), because every time we add more functionality in this way, we assert that the Agda and Haskell implementations correspond precisely to each other, and thus increase our trusted code base.

Also, I think the mechanism for renaming Haskell.Something imports to Something seems like it would belong in a separate PR.

@viktorcsimma
Copy link
Contributor Author

I see... my goal is to simply provide bindings to the Haskell library. So I think I'll change them to postulates; that makes more sense to me, too.

And I'll try to spin off the import mechanism.

@viktorcsimma viktorcsimma marked this pull request as draft March 2, 2024 09:47
@viktorcsimma
Copy link
Contributor Author

I've rewritten it; now it's done until delete. There are also some properties of the operations postulated.

I include the test files for the import rewriting feature here, too, as they depend on Haskell.Data.Map.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants