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

Don't blindly walk under Lam (fixes #124) #126

Merged
merged 9 commits into from
Sep 4, 2018
Merged

Don't blindly walk under Lam (fixes #124) #126

merged 9 commits into from
Sep 4, 2018

Conversation

ocharles
Copy link
Member

@ocharles ocharles commented Sep 1, 2018

Issue #124 demonstrates a problem where an alpha-normalized expression
no longer works with dhall-to-cabal. For example, a version expression
is

\( Version : Type ) -> \( v : Text -> Version ) -> v "1.0.0"

The following is equivalent, because names shouldn't matter:

\( foo : Type ) -> \( bar : Text -> foo ) -> bar "1.0.0"

dhall-to-cabal would fail to extract a version from this expression, as
it walks under two lambdas and then expects to find the exact variable
"v".

Instead, we now take the given expression and fully saturate it with
applications of the variable names we expect.

This same fix has been implied everywhere we were pattern matching on
Lam. Essentially, we should never pattern match on Lam, instead we
should App the variables we need and normalize.

A very tiny unit test suite has been added so we can add tests to types
in the future.

quasicomputational and others added 4 commits September 1, 2018 07:29
Issue #124 demonstrates a problem where an alpha-normalized expression
no longer works with dhall-to-cabal. For example, a version expression
is

    \( Version : Type ) -> \( v : Text -> Version ) -> v "1.0.0"

The following is equivalent, because names shouldn't matter:

    \( foo : Type ) -> \( bar : Text -> foo ) -> bar "1.0.0"

dhall-to-cabal would fail to extract a version from this expression, as
it walks under two lambdas and then expects to find the exact variable
"v".

Instead, we now take the given expression and fully saturate it with
applications of the variable names we expect.

This same fix has been implied everywhere we were pattern matching on
Lam. Essentially, we should never pattern match on Lam, instead we
should App the variables we need and normalize.

A very tiny unit test suite has been added so we can add tests to types
in the future.
@ocharles
Copy link
Member Author

ocharles commented Sep 1, 2018

@jneira Could you give this branch a try?

@jneira
Copy link
Collaborator

jneira commented Sep 1, 2018

@ocharles it works perfectly, thanks!

@ocharles ocharles merged commit 8801086 into master Sep 4, 2018
@ocharles ocharles deleted the gh-124 branch September 4, 2018 21:34
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.

3 participants