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

Compile merging Optionals correctly in dhall-nix #2446

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

DarkKirb
Copy link

@DarkKirb DarkKirb commented Sep 6, 2022

This is done by checking the type of the merge input, and emitting special code for Optionals.

This commit fixes #2443.

Please let me know if i did something poorly, i do not know haskell.

This is done by checking the type of the merge input, and emitting
special code for Optionals.

This commit fixes dhall-lang#2443
@Gabriella439
Copy link
Collaborator

Sorry for the long delay in responding to this.

I think there is a simpler approach that doesn't require threading through the context or inferring the type of any expressions. Rather, what you can do is to check if the argument to the Merge expression is of the form Some _ or App None _ and then change the translation. This makes use of the fact that the expression passed to loop is already pre-normalized so if it's an Optional value then it can only be one of those two cases

I can also implement my suggestion myself if you want, especially given how delayed my review was

@DarkKirb
Copy link
Author

DarkKirb commented Jan 4, 2023

#2443 is only an issue for merges where the expression cannot be reduced to a form merge {Some = _, None = _} [Some _|None _].

some cases like λ(a: Natural) → merge { None = 0, Some = λ(a: Natural) → a } (Some a) compiles correctly, however λ(a: {None: Natural, Some: Natural → Natural }) → merge a (Some 1) also results in the nonsensical a: 1 a (i think that would be fixed with your suggestion though), the original test case wouldn’t be however

@Gabriella439
Copy link
Collaborator

What about in the general case translating the merge keyword to something like:

merge handlers unionLiteral

=>

if builtins.attrNames handlers == [ "Some", "None" ]
then … special case for Optional …
else … normal case …

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.

[dhall-nix] merge operator on Optional not transpiled correctly
2 participants