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

`toJSON` keyword? #336

Open
Gabriel439 opened this Issue Jan 3, 2019 · 15 comments

Comments

Projects
None yet
5 participants
@Gabriel439
Copy link
Contributor

Gabriel439 commented Jan 3, 2019

I'm opening up an issue to discuss this comment:

#125 (comment)

... which is also related to this repository:

https://github.com/akshaymankar/dhall-recursive-json

The informal proposal is to add a new JSON primitive type and a toJSON keyword that converts any Dhall expression to the corresponding JSON expression. The repository linked above has the toJSON keyword taking a type argument followed by the expression to convert to JSON, but we can simplify that a bit to remove the type argument since we can infer the type from the expression to convert (similar to how the Some keyword behaves).

Conceptually the JSON type is an opaque type (i.e. similar to how we treat Double). You can create it using toJSON but you can't do anything with it within the language. The only interesting thing you can do with it is embed it within a larger expression that you convert to JSON. In other words, this is legal:

let x : JSON = toJSON 1
let y : JSON = toJSON True
in  toJSON [ x, y ]

... which would correspond to the following JSON expression:

[ 1, true ]

Note that normalizing toJSON just normalizes its argument. In other words, if we were to normalize the above Dhall expression the normal form would be:

toJSON [ toJSON 1, toJSON True ]

Type-checking toJSON would essentially entail verifying that the Dhall expression is convertable to JSON (which can be made precise, but this is just an informal exposition of the idea). If that check succeeds then the inferred type is JSON.

The non-trivial aspect to this is that each language binding would now be responsible for converting any value of type JSON to a JSON expression within the host language. For example, the Haskell bindings to Dhall would now have an Interpret instance for decoding into the Haskell representation of a JSON value:

instance Interpret Data.Aeson.Value where ...

I'll respond to this in a separate comment with my own thoughts on this proposal.

cc: @akshaymankar

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Jan 3, 2019

My view on this is that I'm in favor but currently I'm trying to pause changes to the language evolution to give the dhall-clj/dhall-purescript/dhall-python implementations a chance to catch up with the standard.

The main reasons I'm in favor are:

  • dhall is positioning itself as a YAML replacement and in order to do so it should natively support JSON. This also dovetails with the proposal to support importing values as JSON: #121
  • It's very simple to implement

The main issue I can foresee is that an implementation might have to pick a standard JSON type to decode into. For some language ecosystems this is easy because there is one right way to do JSON, such as Python (which has a standard JSON library) or Haskell (which has a de-factor standard JSON library in aeson). In other ecosystems this is not the case, such as Scala (which has multiple competing JSON libraries).

However, even in the worst case scenario like Scala an implementation can either (A) define its own a bare-bones JSON data structure to decode into or (B) just be opinionated and pick a JSON library to use.

Note that we have turned down some similar proposals such as:

  • Native support for IP addresses: #217
  • Native support for timestamps: #80

My main reasons for supporting JSON compared to the other primitive types is that:

  • Supporting JSON natively is necessary to properly displace YAML

    YAML does not support IP or timestamp primitive types either, so we lose nothing comparatively if we don't support them. However, if we ever decide to also displace TOML then at some point we will need to support timestamps natively, too.

  • We get a lot of "bang for our buck" standardizing support for JSON compared to other primitive types

    In particular, if we combine this proposal with support for importing expressions as JSON then Dhall effectively can be used as an all-in-one solution for JSON data muxing. Also, Dhall then provides a very nice migration story for existing JSON pipelines.

However, like I mentioned above, I'd like to wait until we have more native language bindings to Dhall before trying this since I think native language support will have a bigger impact on Dhall adoption than JSON support.

@jneira

This comment has been minimized.

Copy link
Contributor

jneira commented Jan 4, 2019

I am not sure about this: wouldn't be enough to use the existent utility dhall-json (with the changes proposed in #125 (comment))?

This could lead to users to ask for other formats, like toYAML itself (the main format to replace with dhall, right?) and extend the support to import as JSON that could be lead to standarize an opitionated way to make conversions.

IMHO conversions with other formats (any of them, in the present or future) should be keeping in official tooling, to try keep dhall itself as simple as possible.

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Jan 4, 2019

Thinking about this more, there is a much simpler way to do this. You can (almost) implement the Dhall to JSON conversion in pure Dhall

I have a branch illustrating how to do this here:

https://github.com/dhall-lang/dhall-lang/tree/gabriel/json_pure_dhall

... and here is an example program to assemble and render a JSON expression:

let JSON =
      https://raw.githubusercontent.com/dhall-lang/dhall-lang/gabriel/json_pure_dhall/Prelude/JSON/package.dhall sha256:76a75f75e9ab6cd78d18b123f10946cc7778a3d734e50978d635505cae8c062a

let value =
      JSON.object
      [ { mapKey =
            "foo"
        , mapValue =
            JSON.array [ JSON.bool True, JSON.number 1.0 ]
        }
      , { mapKey = "bar", mapValue = JSON.string "!" }
      ]

in  JSON.render value
$ dhall-to-text <<< './example.dhall' 
{ "foo": [ true, 1.0 ], "bar": "!" }

This gives us most of the benefits of the proposal without any changes to the language. With a little extra work we could even render pretty-printed JSON, too, entirely in Dhall. This would effectively obsolete the dhall-to-json executable.

The only missing piece is that Dhall needs a new Text/show primitive to escape its own Text literals so that we can render Dhall strings as JSON strings. If we have that then we could implement Dhall conversions to all sorts of configuration formats (including YAML) without having to extend the language. Also, Text/show is a useful general-purpose primitive to add to the language, consistent with the other /show primitives.

Or in other words, this is essentially reusing the same trick as the dhall-nethack project to embed support for JSON within the language by implementing the abstract syntax tree and the rendering function in pure Dhall.

@ocharles

This comment has been minimized.

Copy link
Contributor

ocharles commented Jan 4, 2019

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Jan 6, 2019

@ocharles: There are two reasons I prefer to name this function Text/show:

The first reason is that it's consistent with the naming of the Natural/show, Integer/show, and Double/show utilities, which render the equivalent Dhall representation.

The second reason is that in my mind there is a slight semantic difference between Text/escape and Text/show, which is that I would expect the former to render the escaped text without surrounding quotes and the latter to render with surrounding quotes. In other words:

Text/escape "abc\ndef" = "abc\\ndef"

Text/show "abc\ndef" = "\"abc\\ndef\""

What I was proposing to add to the language was the latter functionality (with surrounding quotes, so that the rendered result is both valid Dhall source code and also a valid JSON string literal).

The main issue I foresee with this is that JSON does not support the \$ escape sequence that Dhall does, so Text/show would have to replace the dollar sign in "\${""}" with \u0024 if it precedes a { in order to be both JSON-compatible and Dhall-compatible. Or in other words:

Text/show "\${""}" = "\"\\u0024{\"\"}\""
@akshaymankar

This comment has been minimized.

Copy link

akshaymankar commented Jan 8, 2019

I tried using the json_pure_dhall branch and realized that converting arbitrary records to JSON is not easy. Users have to write conversion for each type of record to List {mapKey: Text, mapValue: JSON} which is very tedious, especially if records are big.

Also, I think rendering YAML as text might get very tricky in dhall. Although, some other tool could be used to convert JSON to YAML.

On the other hand, my original hack of putting toJSON and JSON in startingContext doesn't work as well as I thought it would because I cannot use them directly in imported files. I think this is because starting context is only applied to inital file. I can, however, wrap all files which render JSONs with λ(JSON : Type) → λ(toJSON : ∀(Value: Type) → ∀(v: Value) → JSON). Its not very nice, but I can deal with it until a better solution is available.

So, I think it would be best (at least for generating JSONs and YAMLs) toJSON was recognized by dhall as a builtin function and JSON was recognized as builtin Type.

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Jan 11, 2019

@akshaymankar: You can customize the context for imports using loadWith. Specifically, the startingContext field of the Status type should work for transitive imports. If it doesn't then that sounds like a bug that should be fixed.

@hanshoglund

This comment has been minimized.

Copy link

hanshoglund commented Jan 25, 2019

I came across a related idea: a primitive that converts arbitrary expressions to the Textof their (normalized) Dhall representation. E.g. toDhall : forall (a : Type) -> a -> Text

@Gabriel439 do you think there would be any soundness/normalization issues with such a primitive?

Some context askvader/askvader#1

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Jan 25, 2019

@hanshoglund: The main issue with that is that it would violate parametricity, meaning that there are fewer guarantees (free theorems) you get for polymorphic expressions. The second issue is that it requires you to standardize how arbitrary expressions are rendered (i.e. should they be Unicode or ASCII, how much spacing to use, etc.).

@hanshoglund

This comment has been minimized.

Copy link

hanshoglund commented Jan 25, 2019

@Gabriel439

Standard representation: That seems solvable, just requires picking a normal form of the syntax (e.g. the one already provided by the formatter).

Parametricity: Good point. So this is basically the seq problem? Of course, one could take the "put seq in a type class" approach, but that would preclude exporting anything involving functions (not a problem, in the JSON case, suggesting that the "create JSON strings in Dhall" approach is sensible there - using dict passing in place type classes of course).

My use case for this was staging, e.g. consider top-level configuration expression for a computing cluster containing functions that we want to transfer to various nodes, where they are to be applied to runtime configuration values (example below). I guess this is not solvable without weakening parametricity.

let RuntimeInfo = { actualIp : Text, clusterSize : Natural, ... }
let ServerConf = ... 
let topLevel = { serverConfig : RuntimeInfo -> ServerConf, minSize : Natural, maxSize : Natural, ... }
@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Jan 25, 2019

@hanshoglund: Could you expand a bit more on the staging use case? The reason I ask is that it's not clear why you need to represent Dhall expressions as text literals Dhall in order to be able to stage them.

@hanshoglund

This comment has been minimized.

Copy link

hanshoglund commented Jan 25, 2019

@Gabriel439: My current implementation involves a custom evaluator (using the Haskell API) that evaluates part of the top-level expression (to obtain e.g. servers to boot), but leaves other parts unevaluated for later execution (e.g. to be copied to the booted servers as text). This works fine, but requires ad-hoc work on the Haskell side managing ASTs and so on. This is fair enough: I'm in a sense writing a custom (distributed) normalizer for Dhall expressions and the fact that I can do this by reusing most of the standard one through its Haskell API is great.

The idea behind toDhall was to represent the staging in Dhall itself, and thus removing the need for a custom evaluator. On the other hand the loss of parametricity indicate that this might not actually simplify things as much as I first thought. I'll probably stick to my original idea :).

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Jan 31, 2019

@akshaymankar: Would your original concern about using the json_pure_dhall branch be resolved if Dhall had a keyword for converting records to lists of key-value pairs? See this comment for more details:

#234 (comment)

If we had that, then you could convert a Dhall record to a JSON recordd, like this:

let JSON =
      https://raw.githubusercontent.com/dhall-lang/dhall-lang/gabriel/json_pure_dhall/Prelude/JSON/package.dhall sha256:76a75f75e9ab6cd78d18b123f10946cc7778a3d734e50978d635505cae8c062a

let record =
      { foo =
          JSON.array [ JSON.bool True, JSON.number 1.0 ]
      , bar =
          JSON.string "!"
      }

let value = JSON.object (toMap record)

in  JSON.render value
@akshaymankar

This comment has been minimized.

Copy link

akshaymankar commented Feb 3, 2019

Would toMap be able to convert any record to assoc list or would it have to be a record with all the values of type JSON?
It would be great if it works on all record types, but I can already see a couple of implementation problems with it. For instance would it be an error if one of the values is a function? Implementing this kind of check could get tricky.
But if it doesn't work on any record type, I am not sure if this solves the tediousness of converting a big record with recursive elements to JSON.

Gabriel439 added a commit that referenced this issue Feb 6, 2019

Add `Text/show` built-n
There are two motivations for adding this built-in:

* For consistency with `Natural/show`, `Integer/show`, etc.

* To enable the implementation of a Dhall-to-JSON conversion in pure Dhall

  ... as described in:

  #336 (comment)

Carefully note that dollar signs are escaped as `\u0024` because that is the
only representation that is both JSON-compatible (since JSON does not
support the `\$` escape sequence) and Dhall-compatible (since failure to
escape `$` may accidentally generate an unintended string interpolation).
@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

Gabriel439 commented Feb 7, 2019

@akshaymankar: I believe toMap should probably not automatically recurse because then there would be no way to opt out of the automatic recursion behavior for nested records.

However, I think the way I'm going to proceed is to try to convert a few JSON configuration formats to Dhall using the json_pure_dhall branch once the Text/show support is merged so I can get a better idea of what's necessary to make this easy.

Gabriel439 added a commit that referenced this issue Feb 13, 2019

Add `Text/show` built-in (#365)
There are two motivations for adding this built-in:

* For consistency with `Natural/show`, `Integer/show`, etc.

* To enable the implementation of a Dhall-to-JSON conversion in pure Dhall

  ... as described in:

  #336 (comment)

Carefully note that dollar signs are escaped as `\u0024` because that is the
only representation that is both JSON-compatible (since JSON does not
support the `\$` escape sequence) and Dhall-compatible (since failure to
escape `$` may accidentally generate an unintended string interpolation).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.