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

Substitutions #1650

Merged
merged 14 commits into from
Feb 6, 2020
Merged

Substitutions #1650

merged 14 commits into from
Feb 6, 2020

Conversation

mmhat
Copy link
Collaborator

@mmhat mmhat commented Jan 30, 2020

Substitutions are another way of extending the language:
The idea is to to substitute certain variables with expressions defined
in the interpreter before type checking.

This commit resolves #794 .
This commit resolves #879 .
This commit resolves #1502 .

Substitutions are another way of extending the language:
The idea is to to substitute certain variables with expressions defined
in the interpreter before type checking.

This commit resolves dhall-lang#794.
This commit resolves dhall-lang#879.
@sjakobi
Copy link
Collaborator

sjakobi commented Jan 30, 2020

Interesting! :)

Could you give an example of how to use this?

@MonoidMusician
Copy link
Contributor

Aside from a slightly different handling of variables, what advantage does this offer compared to just wrapping the expression with certain let bindings? (Let bindings are morally subsituted before typechecking, but they must make sense on their own before substitution, of course.)

@mmhat
Copy link
Collaborator Author

mmhat commented Feb 1, 2020

@sjakobi Have a look at my last commits. I added a section about substitutions to the tutorial. A full working example is included in the test suite.

@mmhat
Copy link
Collaborator Author

mmhat commented Feb 1, 2020

@MonoidMusician Although let-wrapping works I always found it rather 'hacky'. I'd argue that the approach in this pull request is cleaner. Besides, it works with inputFile without generating Dhall code (see this comment).

@mmhat
Copy link
Collaborator Author

mmhat commented Feb 1, 2020

Hm, it is a bit unclear to me why the Hydra CI is failing. Can anybody help?

@Gabriella439
Copy link
Collaborator

@mmhat: CI requires everything that is exported to be documented

@Gabriella439
Copy link
Collaborator

Gabriella439 commented Feb 2, 2020

@MonoidMusician: Another thing this can do that a let binding cannot is that the substitution can be forwarded to transitive imports

@Gabriella439
Copy link
Collaborator

@mmhat: The new Dhall.Substitution module also needs documentation for the module header

Copy link
Collaborator

@sjakobi sjakobi left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a few random comments. I really this in any case! 👍

dhall/src/Dhall.hs Outdated Show resolved Hide resolved
dhall/src/Dhall/Substitution.hs Outdated Show resolved Hide resolved
dhall/src/Dhall.hs Outdated Show resolved Hide resolved
-- >
-- > myexample :: IO Result
-- > myexample = let
-- > evaluateSettings = Lens.over Dhall.substitutions (Data.Map.insert "Result" resultType) Dhall.defaultEvaluateSettings
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder whether it would be better if the collection of substitutions were opaque instead of a plain Map.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since substitutions are a simple mapping and the Map datatype is a common one the user will get an immediate intuition how to construct/update/... the data structure.
I think this contributes more to the usability than an opaque type. Of course it makes it more difficult to change this feature in the future because it might break other peoples code.
I'm not sure about this trade off myself...

dhall/src/Dhall/Substitution.hs Outdated Show resolved Hide resolved
@Gabriella439
Copy link
Collaborator

@mmhat: I added you as a collaborator, so you can merge whenever you are ready, either by clicking "Squash and merge" when CI is green or by adding the "merge me" label to your pull request (which will take care of auto-merging for you once CI is green)

@mmhat mmhat added the merge me label Feb 6, 2020
@mergify mergify bot merged commit a794cd8 into dhall-lang:master Feb 6, 2020
@mmhat mmhat deleted the substitution branch February 6, 2020 03:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
4 participants