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.

Sign up for GitHub

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

Jump to bottom

Enable with optimizations #1052

Merged
merged 5 commits into from
Aug 19, 2020
Merged

Enable with optimizations #1052

merged 5 commits into from
Aug 19, 2020

Conversation

Gabriella439
Copy link
Contributor

The motivation for this change is:

dhall-lang/dhall-haskell#1960

This change to the standard gives implementations greater freedom
in how they desugar a with expression, in order to permit more
efficient implementations. The standard now also suggests a more
efficient implementation to help implementation authors.

This is technically a breaking change to the binary encoding of
a non-normalized with expression, but semantic integrity checks
are unaffected by this change.

@Gabriella439
Enable with optimizations
e724249 
The motivation for this change is:

dhall-lang/dhall-haskell#1960

This change to the standard gives implementations greater freedom
in how they desugar a `with` expression, in order to permit more
efficient implementations.  The standard now also suggests a more
efficient implementation to help implementation authors.

This is technically a breaking change to the binary encoding of
a non-normalized `with` expression, but semantic integrity checks
are unaffected by this change.
@Gabriella439
Copy link
Contributor Author

This is an alternative proposal for #1050 based on a discussion with @Nadrieril

Gabriella439 added a commit to dhall-lang/dhall-haskell that referenced this pull request Aug 13, 2020
@Gabriella439
Implement more efficient with desugaring
e880c72 
… as permitted by dhall-lang/dhall-lang#1052
@Gabriella439 Gabriella439 mentioned this pull request Aug 13, 2020
Merged
@Gabriella439
Copy link
Contributor Author

Here is the matching change to the Haskell implementation: dhall-lang/dhall-haskell#1993

@Gabriella439 Gabriella439 mentioned this pull request Aug 13, 2020
Closed
@Nadrieril
Copy link
Member

Could you add a few normalization and typeckecking tests? Right now the feature is essentially untested if I'm following correctly

@Gabriella439
Copy link
Contributor Author

@Nadrieril: There are type-checking and normalization tests for with; they just weren't affected by this change. However, I can still add the test you mentioned in #1050 (comment)

philandstuff
philandstuff reviewed Aug 13, 2020
View reviewed changes
Copy link
Collaborator

@philandstuff philandstuff left a comment

Choose a reason for hiding this comment

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

I’d like some time to test this with dhall-golang and feed back, not sure when I’ll get to it but can I at least request a hold on merging of a week to give me a chance?

@Gabriella439
Copy link
Contributor Author

@philandstuff: Yeah, I'm not in a rush

philandstuff
philandstuff reviewed Aug 19, 2020
View reviewed changes
Copy link
Collaborator

@philandstuff philandstuff left a comment

Choose a reason for hiding this comment

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

This is basically great 👍

A couple of smallish things:

Use of shift

I basically agree with @Nadrieril in #1050 (comment) that shift is an artefact of the standard but not necessary in an implementation. Currently dhall-golang doesn't have a shift. This feature nudges implementations towards a shift-based implementation of with-desugaring, but my leanings are more towards implementing with as a first-class term, not as a desugaring.

The current dhall-golang implementation is here: https://github.com/philandstuff/dhall-golang/compare/std-pr-1052-with but I'm planning to directly implement typechecking and evaluation on with expressions, and not do it via a desugaring step.

That said, there's nothing in this PR that prevents me doing that. The tests will still pass.

Test coverage

We don't have any typechecking tests for compound paths in a with (such as r with x.y = v). Might I suggest:

{- WithNestedA.dhall -}
{- This test illustrates that the `with` keyword is permitted to override
   existing fields nested within a child record
-}
{ a = { p = 2, q = "hi" }, b = 5.6 } with a.p = True
{- WithNestedB.dhall -}
{ a : { p : Bool, q : Text }, b : Double }

@Gabriella439
Copy link
Contributor Author

@philandstuff: The main reason for standardizing in terms of a desugaring is because the type-checking and normalization judgments directly on with are a bit complex to specify using logical notation. If we were using Haskell code for the semantics then it would be easier to define with as a standalone judgment

@Gabriella439 Gabriella439 merged commit b046b84 into master Aug 19, 2020
@sjakobi sjakobi deleted the gabriel/with_encoding_2 branch August 19, 2020 16:52
Gabriella439 added a commit to dhall-lang/dhall-haskell that referenced this pull request Aug 19, 2020
@Gabriella439
Implement more efficient with desugaring (#1993)
48fcd20 
… as permitted by dhall-lang/dhall-lang#1052
@philandstuff philandstuff mentioned this pull request Aug 19, 2020
Merged
@travisbrown travisbrown mentioned this pull request Sep 3, 2020
Merged
philandstuff added a commit that referenced this pull request Sep 20, 2020
@philandstuff
Implement with directly rather than via desugaring
98da299 
I found it confusing to implement the recent `with`
optimizations (#1052) because `with` expressions are currently neither
pure sugar nor first-class expressions.

Also, there is arguably still scope for pathological behaviour, since
an abstract function like

    \(r : {a : {b : {c : Natural}} }) -> r with a.b.x = 1 with a.b.y = 2

will be evaluated to a function which potentially evaluates `r` 6
times (in an implementation which does not evaluate arguments before
passing them to a function).

This commit defines type inference and beta-normalization for `with`
expressions directly, rather than via a desugaring step.  As a
side-effect, desugaring of abstract `with` expressions no longer
happens; they are left as plain `with` expressions.  This is a
breaking change.

There is another consideration, which is there are currently a number
of simplifications for right-biased record merge expressions which the
current `with`-desugaring can piggyback on.  For example, currently:

    (e with k = v).k

evaluates to `v`, because of the simplification of expressions of the
form `(l // { k = v, rs... }).k`.  This commit does not attempt to
preserve those simplifications, but we could introduce some
`with`-simplifications in later commits if desired.
philandstuff added a commit that referenced this pull request Sep 20, 2020
@philandstuff
Implement with directly rather than via desugaring
9d5ac2a 
I found it confusing to implement the recent `with`
optimizations (#1052) because `with` expressions are currently neither
pure sugar nor first-class expressions.

Also, there is arguably still scope for pathological behaviour, since
an abstract function like

    \(r : {a : {b : {c : Natural}} }) -> r with a.b.x = 1 with a.b.y = 2

will be evaluated to a function which potentially evaluates `r` 6
times (in an implementation which does not evaluate arguments before
passing them to a function).

This commit defines type inference and beta-normalization for `with`
expressions directly, rather than via a desugaring step.  As a
side-effect, desugaring of abstract `with` expressions no longer
happens; they are left as plain `with` expressions.  This is a
breaking change.

There is another consideration, which is there are currently a number
of simplifications for right-biased record merge expressions which the
current `with`-desugaring can piggyback on.  For example, currently:

    (e with k = v).k

evaluates to `v`, because of the simplification of expressions of the
form `(l // { k = v, rs... }).k`.  This commit does not attempt to
preserve those simplifications, but we could introduce some
`with`-simplifications in later commits if desired.
@philandstuff philandstuff mentioned this pull request Sep 20, 2020
Merged
philandstuff added a commit that referenced this pull request Sep 20, 2020
@philandstuff
Implement with directly rather than via desugaring
52c2761 
I found it confusing to implement the recent `with`
optimizations (#1052) because `with` expressions are currently neither
pure sugar nor first-class expressions.

Also, there is arguably still scope for pathological behaviour, since
an abstract function like

    \(r : {a : {b : {c : Natural}} }) -> r with a.b.x = 1 with a.b.y = 2

will be evaluated to a function which potentially evaluates `r` 6
times (in an implementation which does not evaluate arguments before
passing them to a function).

This commit defines type inference and beta-normalization for `with`
expressions directly, rather than via a desugaring step.  As a
side-effect, desugaring of abstract `with` expressions no longer
happens; they are left as plain `with` expressions.  This is a
breaking change.

There is another consideration, which is there are currently a number
of simplifications for right-biased record merge expressions which the
current `with`-desugaring can piggyback on.  For example, currently:

    (e with k = v).k

evaluates to `v`, because of the simplification of expressions of the
form `(l // { k = v, rs... }).k`.  This commit does not attempt to
preserve those simplifications, but we could introduce some
`with`-simplifications in later commits if desired.
philandstuff added a commit that referenced this pull request Sep 28, 2020
@philandstuff @Gabriella439
Implement with directly rather than via desugaring (#1073)
e663cb3 
* Implement `with` directly rather than via desugaring

I found it confusing to implement the recent `with`
optimizations (#1052) because `with` expressions are currently neither
pure sugar nor first-class expressions.

Also, there is arguably still scope for pathological behaviour, since
an abstract function like

    \(r : {a : {b : {c : Natural}} }) -> r with a.b.x = 1 with a.b.y = 2

will be evaluated to a function which potentially evaluates `r` 6
times (in an implementation which does not evaluate arguments before
passing them to a function).

This commit defines type inference and beta-normalization for `with`
expressions directly, rather than via a desugaring step.  As a
side-effect, desugaring of abstract `with` expressions no longer
happens; they are left as plain `with` expressions.  This is a
breaking change.

There is another consideration, which is there are currently a number
of simplifications for right-biased record merge expressions which the
current `with`-desugaring can piggyback on.  For example, currently:

    (e with k = v).k

evaluates to `v`, because of the simplification of expressions of the
form `(l // { k = v, rs... }).k`.  This commit does not attempt to
preserve those simplifications, but we could introduce some
`with`-simplifications in later commits if desired.

* small tweaks

* oops, remove duplicate alpha-normalization rule

* Update standard/beta-normalization.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* fix type inference rule

as caught by @Nadrieril

* better mnemonic variable names

as caught by @Gabriel439

* Allow creation of intermediate records

also tidy up the judgments a bit, add tests for the new judgments,
remove tests for the old desugaring behaviour.

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Update standard/type-inference.md

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>

* Add a test for partially-abstract `with` expressions

This caught a bug in dhall-golang.

Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@philandstuff philandstuff philandstuff approved these changes

@Nadrieril Nadrieril Nadrieril approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@Gabriella439 @Nadrieril @philandstuff