Improve Prelude.JSON.render output#1118
Merged
Gabriella439 merged 3 commits intomasterfrom Dec 4, 2020
Merged
Conversation
Now that we have language support for `Text/replace` we don't need to use `Text/show` any longer. In particular, one of the limitations of `Text/show` was that we were using it both to render valid Dhall values and also to render valid JSON strings, which constrained it to produce weird output for `$` (`\u0024`). However, now that we have `Text/replace` we can use a JSON-specific escaping strategy. This also implies that we can make two further improvements (not included in this pull request): * We could standardize the behavior of `Text/show` in terms of `Text/replace` … or even remove `Text/show` as a built-in after deprecation. * We can now improve the behavior of `Text/show` to escape `$` as `\$` instead of `\u0024` … now that it's no longer used for escaping JSON strings.
sjakobi
approved these changes
Nov 25, 2020
Collaborator
sjakobi
left a comment
There was a problem hiding this comment.
I was curious how this would affect the size of the binary encoded Prelude:
$ echo https://raw.githubusercontent.com/dhall-lang/dhall-lang/master/Prelude/package.dhall | dhall --alpha | dhall encode | wc
3 1043 93241
$ echo https://raw.githubusercontent.com/dhall-lang/dhall-lang/22bb26a72e727977ad0a1a17a8e7652328a80170/Prelude/package.dhall | dhall --alpha | dhall encode | wc
59 1267 102105
So the cache size is about 9.5% bigger now, which doesn't seem too bad.
Collaborator
I would be fine with removing |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Now that we have language support for
Text/replacewe don't needto use
Text/showany longer. In particular, one of the limitationsof
Text/showwas that we were using it both to render valid Dhallvalues and also to render valid JSON strings, which constrained it
to produce weird output for
$(\u0024). However, now that wehave
Text/replacewe can use a JSON-specific escaping strategy.This also implies that we can make two further improvements (not
included in this pull request):
We could standardize the behavior of
Text/showin terms ofText/replace… or even remove
Text/showas a built-in after deprecation.We can now improve the behavior of
Text/showto escape$as\$instead of\u0024… now that it's no longer used for escaping JSON strings.