Dhall.JSONToDhall

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
  }
]

JSON to Dhall

parseConversion :: Parser Conversion

Standard parser for options related to the conversion method

data Conversion

JSON-to-dhall translation options

Constructors

Conversion

Fields

• strictRecs :: Bool
• noKeyValArr :: Bool
• noKeyValMap :: Bool
• unions :: UnionConv
• omissibleLists :: Bool

Instances

Show Conversion

Defined in Dhall.JSONToDhall

Methods

showsPrec :: Int -> Conversion -> ShowS

show :: Conversion -> String

showList :: [Conversion] -> ShowS

defaultConversion :: Conversion

Default conversion options

resolveSchemaExpr

Arguments

:: Text

type code (schema)

-> IO ExprX

Parse schema code to a valid Dhall expression and check that its type is actually Type

typeCheckSchemaExpr :: (Exception e, MonadCatch m) => (CompileError -> e) -> ExprX -> m ExprX

Check that the Dhall type expression actually has type Type >>> :set -XOverloadedStrings >>> import Dhall.Core

>>> typeCheckSchemaExpr id =<< resolveSchemaExpr "List Natural"
App List Natural

>>> typeCheckSchemaExpr id =<< resolveSchemaExpr "+1"
*** Exception:
Error: Schema expression is succesfully parsed but has Dhall type:
Integer
Expected Dhall type: Type
Parsed expression: +1

dhallFromJSON :: Conversion -> ExprX -> Value -> Either CompileError ExprX

The main conversion function. Traversing/zipping Dhall type and Aeson value trees together to produce a Dhall term tree, given Conversion options:

>>> :set -XOverloadedStrings
>>> import qualified Dhall.Core as D
>>> import qualified Dhall.Map as Map
>>> import qualified Data.Aeson as A
>>> import qualified Data.HashMap.Strict as HM

>>> s = D.Record (Map.fromList [("foo", D.Integer)])
>>> v = A.Object (HM.fromList [("foo", A.Number 1)])
>>> dhallFromJSON defaultConversion s v
Right (RecordLit (fromList [("foo",IntegerLit 1)]))

Exceptions

data CompileError

Constructors

TypeError (TypeError Src Void)

BadDhallType ExprX ExprX

Mismatch ExprX Value

MissingKey Text ExprX Value

UnhandledKeys [Text] ExprX Value

NoKeyValArray ExprX Value

NoKeyValMap ExprX Value

ContainsUnion ExprX

UndecidableUnion ExprX Value [ExprX]

Instances

Show CompileError

Defined in Dhall.JSONToDhall

Methods

showsPrec :: Int -> CompileError -> ShowS

show :: CompileError -> String

showList :: [CompileError] -> ShowS

Exception CompileError

Defined in Dhall.JSONToDhall

Methods

toException :: CompileError -> SomeException

fromException :: SomeException -> Maybe CompileError

displayException :: CompileError -> String

showCompileError :: String -> (Value -> String) -> CompileError -> String