Skip to content

Implement with directly rather than via desugaring#1073

Merged
philandstuff merged 11 commits intomasterfrom
make-with-a-first-class-expression
Sep 28, 2020
Merged

Implement with directly rather than via desugaring#1073
philandstuff merged 11 commits intomasterfrom
make-with-a-first-class-expression

Conversation

@philandstuff
Copy link
Copy Markdown
Collaborator

@philandstuff philandstuff commented Sep 20, 2020

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
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 philandstuff force-pushed the make-with-a-first-class-expression branch from 9d5ac2a to 52c2761 Compare September 20, 2020 13:36
philandstuff
philandstuff commented Sep 20, 2020
View reviewed changes
Nadrieril
Nadrieril reviewed Sep 20, 2020
View reviewed changes
@Nadrieril
Copy link
Copy Markdown
Member

Nadrieril commented Sep 20, 2020

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).

That's not a very convincing argument: the same would happen with

\(f: Int -> Int) -> Natural/fold 6 Natural f 0

That said, I find the new rules much shorted and clearer than the desugaring, so I'm weakly in favor of this change (weakly because I'd have to implement it ^^)

Gabriella439
Gabriella439 reviewed Sep 21, 2020
View reviewed changes
Copy link
Copy Markdown
Contributor

@Gabriella439 Gabriella439 left a comment

Choose a reason for hiding this comment

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

Looks great! Just a few minor suggestions

philandstuff and others added 5 commits September 21, 2020 21:49
@philandstuff @Gabriella439
Update standard/beta-normalization.md
62867ed 
Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>
@philandstuff @Gabriella439
Update standard/type-inference.md
9c74426 
Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>
@philandstuff
fix type inference rule
36ade1c 
as caught by @Nadrieril
@philandstuff
better mnemonic variable names
f1d7de5 
as caught by @Gabriel439
@philandstuff
Allow creation of intermediate records
e38bba7 
also tidy up the judgments a bit, add tests for the new judgments,
remove tests for the old desugaring behaviour.
@philandstuff
Copy link
Copy Markdown
Collaborator Author

philandstuff commented Sep 22, 2020

Ok I've updated the PR to allow { a = 5 } with b.c = 10 to typecheck and evaluate to { a = 5, b = { c = 10 } }. I've also updated the tests to reflect the new judgment rules, and removed the old WithUnderscore tests which were based on the old desugaring.

I've also made a corresponding change to the dhall-golang implementation: philandstuff/dhall-golang#53

Gabriella439 added a commit to dhall-lang/dhall-haskell that referenced this pull request Sep 24, 2020
@Gabriella439
Implement with without syntactic sugar
2f818e3 
… as standardized in dhall-lang/dhall-lang#1073
@Gabriella439 Gabriella439 mentioned this pull request Sep 24, 2020
Merged
Gabriella439
Gabriella439 approved these changes Sep 24, 2020
View reviewed changes
Copy link
Copy Markdown
Contributor

@Gabriella439 Gabriella439 left a comment

Choose a reason for hiding this comment

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

I also made the matching change in the Haskell implementation here: dhall-lang/dhall-haskell#2055

philandstuff and others added 3 commits September 26, 2020 10:54
@philandstuff @Gabriella439
Update standard/type-inference.md
8355845 
Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>
@philandstuff @Gabriella439
Update standard/type-inference.md
81a302d 
Co-authored-by: Gabriel Gonzalez <Gabriel439@gmail.com>
@philandstuff
Add a test for partially-abstract with expressions
735e738 
This caught a bug in dhall-golang.
@Gabriella439
Copy link
Copy Markdown
Contributor

Gabriella439 commented Sep 28, 2020

@philandstuff: I believe this is clear to merge

@philandstuff philandstuff merged commit e663cb3 into master Sep 28, 2020
@philandstuff philandstuff deleted the make-with-a-first-class-expression branch September 28, 2020 05:15
mergify bot pushed a commit to dhall-lang/dhall-haskell that referenced this pull request Sep 28, 2020
@Gabriella439 @sjakobi
Implement with without syntactic sugar (#2055)
29199f5 
* Implement `with` without syntactic sugar

… as standardized in dhall-lang/dhall-lang#1073

* Fix `dhall-nix` build

… by restoring the `desugarWith` utility, even if it's only used by
`dhall-nix`

* Align whitespace

… as caught by @sjakobi

Co-authored-by: Simon Jakobi <simon.jakobi@gmail.com>

Co-authored-by: Simon Jakobi <simon.jakobi@gmail.com>
@philandstuff philandstuff mentioned this pull request Oct 6, 2020
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Nadrieril Nadrieril Nadrieril left review comments

@Gabriella439 Gabriella439 Gabriella439 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.

3 participants

@philandstuff @Nadrieril @Gabriella439