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

Always drop "Haskell." prefix from module names #379

Open
wants to merge 2 commits into
base: master
Choose a base branch
from

Conversation

jespercockx
Copy link
Member

This supersedes #297. The idea (due to @omelkonian) is that any module starting with Haskell. should be treated as defining part of the FFI with Haskell and should thus not be checked for having COMPILE pragmas, but instead be assumed to exist on the Haskell side while dropping the Haskell. prefix from the module name.

@jespercockx
Copy link
Member Author

jespercockx commented Nov 22, 2024

Three things to consider before merging this:

  • There is a risk of introducing a name collision between Haskell.Foo.Bar and Foo.Bar. Can we do anything about this?
  • Should we enforce that Haskell. modules do not produce any output?
  • Can we make it clearer to the user that defining a Haskell. module is an unsafe thing to do? We can certainly add a note to the documentation, but is there anything else we can do?

@jespercockx
Copy link
Member Author

Related: #316

@viktorcsimma
Copy link
Contributor

viktorcsimma commented Nov 30, 2024

This is a nice idea:) I often utilise similar concepts, and this would be of great help.

  • For the first one: I have checked this and GHC, in this case, prefers the user-defined module. So Foo.Bar would trump Haskell.Foo.Bar in this case. See example.zip here. But I do not have an idea on how to circumvent this, apart from a note in the docs.
  • For the second: I think we should. If the output were Foo.Bar, it would trump the Haskell builtin version, which we probably do not want. If it were Haskell.Foo.Bar, it would be an ordinary agda2hs-generated module.
  • For the third: what about hiding the feature behind a flag? Like with --erasure in Agda. Then, if the user defines a module beginning with Haskell., we fail and tell them to change the name, or add the flag if they know what they are doing. (It would be even better if we could add this flag to a language pragma at the top of the file.)

@jespercockx
Copy link
Member Author

Regarding the first two: actually, if we implement the second and enforce no Haskell code being generated from Haskell. files, then there is no risk of conflicts. There is one module in our own prelude that does not conform to this restriction (https://github.com/agda/agda2hs/blob/master/lib/Haskell/Extra/Loop.agda), but I don't think anyone is using it so we could just drop it.

I like the idea of having a pragma that should be in every module under Haskell., that way we can prevent users from accidentally running into this feature.

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