Convert JSON data to Dhall given a Dhall type expression necessary to make the translation unambiguous.

Reasonable requirements for conversion are:

1. The Dhall type expression t passed as an argument to json-to-dhall should be a valid type of the resulting Dhall expression
2. A JSON data produced by the corresponding dhall-to-json from the Dhall expression of type t should (under reasonable assumptions) reproduce the original Dhall expression using json-to-dhall with type argument t

Only a subset of Dhall types consisting of all the primitive types as well as Optional, Union and Record constructs, is used for reading JSON data:

• Bools
• Naturals
• Integers
• Doubles
• Texts
• Lists
• Optional values
• unions
• records

Additionally, you can read in arbitrary JSON data into a Dhall value of type https://prelude.dhall-lang.org/JSON/Type if you don't know the schema of the JSON data in advance.

This library can be used to implement an executable which takes any data serialisation format which can be parsed as an Aeson Value and converts the result to a Dhall value. One such executable is json-to-dhall which is used in the examples below.

Primitive types

JSON Bools translate to Dhall bools:

$ json-to-dhall Bool <<< 'true'
True
$ json-to-dhall Bool <<< 'false'
False

JSON numbers translate to Dhall numbers:

$ json-to-dhall Integer <<< 2
+2
$ json-to-dhall Natural <<< 2
2
$ json-to-dhall Double <<< -2.345
-2.345

Dhall Text corresponds to JSON text:

$ json-to-dhall Text <<< '"foo bar"'
"foo bar"

Lists and records

Dhall Lists correspond to JSON lists:

$ json-to-dhall 'List Integer' <<< '[1, 2, 3]'
[ +1, +2, +3 ]

Dhall records correspond to JSON records:

$ json-to-dhall '{foo : List Integer}' <<< '{"foo": [1, 2, 3]}'
{ foo = [ +1, +2, +3 ] }

Note, that by default, only the fields required by the Dhall type argument are parsed (as you commonly will not need all the data), the remaining ones being ignored:

$ json-to-dhall '{foo : List Integer}' <<< '{"foo": [1, 2, 3], "bar" : "asdf"}'
{ foo = [ +1, +2, +3 ] }

If you do need to make sure that Dhall fully reflects JSON record data comprehensively, --records-strict flag should be used:

$ json-to-dhall --records-strict '{foo : List Integer}' <<< '{"foo": [1, 2, 3], "bar" : "asdf"}'
Error: Key(s) @bar@ present in the JSON object but not in the corresponding Dhall record. This is not allowed in presence of --records-strict:

By default, JSON key-value arrays will be converted to Dhall records:

$ json-to-dhall '{ a : Integer, b : Text }' <<< '[{"key":"a", "value":1}, {"key":"b", "value":"asdf"}]'
{ a = +1, b = "asdf" }

Attempting to do the same with --no-keyval-arrays on will result in error:

$ json-to-dhall --no-keyval-arrays '{ a : Integer, b : Text }' <<< '[{"key":"a", "value":1}, {"key":"b", "value":"asdf"}]'
Error: JSON (key-value) arrays cannot be converted to Dhall records under --no-keyval-arrays flag:

Conversion of the homogeneous JSON maps to the corresponding Dhall association lists by default:

$ json-to-dhall 'List { mapKey : Text, mapValue : Text }' <<< '{"foo": "bar"}'
[ { mapKey = "foo", mapValue = "bar" } ]

The map keys can even be union types instead of Text:

$ json-to-dhall 'List { mapKey : < A | B >, mapValue : Natural }' <<< '{"A": 1, "B": 2}'
[ { mapKey = < A | B >.A, mapValue = 1 }, { mapKey = < A | B >.B, mapValue = 2 } ]

Flag --no-keyval-maps switches off this mechanism (if one would ever need it):

$ json-to-dhall --no-keyval-maps 'List { mapKey : Text, mapValue : Text }' <<< '{"foo": "bar"}'
Error: Homogeneous JSON map objects cannot be converted to Dhall association lists under --no-keyval-arrays flag

Optional values and unions

Dhall Optional Dhall type allows null or missing JSON values:

$ json-to-dhall "Optional Integer" <<< '1'
Some +1

$ json-to-dhall "Optional Integer" <<< null
None Integer

$ json-to-dhall '{ a : Integer, b : Optional Text }' <<< '{ "a": 1 }'

{ a = +1, b = None Text }

For Dhall union types the correct value will be based on matching the type of JSON expression:

$ json-to-dhall 'List < Left : Text | Right : Integer >' <<< '[1, "bar"]'
[ < Left : Text | Right : Integer >.Right +1

, : Text | Right : Integer.Left "bar" ]

$ json-to-dhall '{foo : < Left : Text | Right : Integer >}' <<< '{ "foo": "bar" }'
{ foo = < Left : Text | Right : Integer >.Left "bar" }

In presence of multiple potential matches, the first will be selected by default:

$ json-to-dhall '{foo : < Left : Text | Middle : Text | Right : Integer >}' <<< '{ "foo": "bar"}'
{ foo = < Left : Text | Middle : Text | Right : Integer >.Left "bar" }

This will result in error if --unions-strict flag is used, with the list of alternative matches being reported (as a Dhall list)

$ json-to-dhall --unions-strict '{foo : < Left : Text | Middle : Text | Right : Integer >}' <<< '{ "foo": "bar"}'
Error: More than one union component type matches JSON value
...
Possible matches:

: Text | Middle : Text | Right : Integer.Left "bar" > -------- : Text | Middle : Text | Right : Integer.Middle "bar"

Weakly-typed JSON

If you don't know the JSON's schema in advance, you can decode into the most general schema possible:

$ cat ./schema.dhall
https://prelude.dhall-lang.org/JSON/Type

$ json-to-dhall ./schema.dhall <<< '[ { "foo": null, "bar": [ 1.0, true ] } ]'
  λ(JSON : Type)
→ λ(string : Text → JSON)
→ λ(number : Double → JSON)
→ λ(object : List { mapKey : Text, mapValue : JSON } → JSON)
→ λ(array : List JSON → JSON)
→ λ(bool : Bool → JSON)
→ λ(null : JSON)
→ array
  [ object
    [ { mapKey = "foo", mapValue = null }
    , { mapKey = "bar", mapValue = array [ number 1.0, bool True ] }
    ]
  ]

You can also mix and match JSON fields whose schemas are known or unknown:

$ cat ./mixed.dhall
List
{ foo : Optional Natural
, bar : https://prelude.dhall-lang.org/JSON/Type
}

$ json-to-dhall ./mixed.dhall <<< '[ { "foo": null, "bar": [ 1.0, true ] } ]'
[ { bar =
        λ(JSON : Type)
      → λ(string : Text → JSON)
      → λ(number : Double → JSON)
      → λ(object : List { mapKey : Text, mapValue : JSON } → JSON)
      → λ(array : List JSON → JSON)
      → λ(bool : Bool → JSON)
      → λ(null : JSON)
      → array [ number 1.0, bool True ]
  , foo =
      None Natural
  }
]