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

Improve Prelude.JSON.render output #1118

Merged
merged 3 commits into from
Dec 4, 2020
Merged

Conversation

Gabriella439
Copy link
Contributor

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.

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

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.

@SiriusStarr
Copy link
Collaborator

... or even remove `Text/show` as a built-in after deprecation.

I would be fine with removing Text/show so long as text escaping ends up in the Prelude. I think it's important to have a quick and easy Text.escapeFor.Dhall and/or Text.escapeFor.Json or whatnot, because I currently can just slap Text/show on the problem and assume it works rather than having to remember every single thing that needs to be escaped for Json and invariably forgetting one.

@Gabriella439 Gabriella439 merged commit ccc8bcf into master Dec 4, 2020
@Gabriella439 Gabriella439 deleted the gabriel/improve_json_render branch December 4, 2020 05:26
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.

None yet

3 participants