Dhall.JSONToDhall

Convert JSON data to Dhall in one of two ways:

• By default, the conversion will make a best-effort at inferring the corresponding Dhall type
• Optionally, you can specify an expected Dhall type necessary to make the translation unambiguous.

Either way, if you supply the generated Dhall result to dhall-to-json you should get back the original JSON.

Only a subset of Dhall types are supported when converting from JSON:

• Bool

• Natural

• Integer

• Double

• Text

• List

• Optional

• unions
• records

• Prelude.Type.Map

• Prelude.Type.JSON - You can always convert JSON data to this type as a last resort if you don't know the schema in advance.

You can use this code as a library (this module) or as an executable named json-to-dhall, which is used in the examples below.

By default the json-to-dhall executable attempts to infer the appropriate Dhall type from the JSON data, like this:

$ json-to-dhall <<< 1
1

... but you can also provide an explicit schema on the command line if you prefer a slightly different Dhall type which still represents the same JSON value:

$ json-to-dhall Integer <<< 1
+1

You can also get the best of both worlds by using the type subcommand to infer the schema:

$ json-to-dhall type <<< '[ "up", "down" ]' | tee schema.dhall
List Text

... and then edit the ./schema.dhall file to better match the type you intended, such as:

$ $EDITOR schema.dhall
$ cat ./schema.dhall
List < up | down >

... and then use the edited schema for subsequent conversions:

$ json-to-dhall ./schema.dhall <<< '[ "up", "down" ]'
[ < down | up >.up, < down | up >.down ]

Primitive types

JSON Bools translate to Dhall bools:

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

JSON numbers translate to Dhall numbers:

$ json-to-dhall <<< 2
2
$ json-to-dhall <<< -2
-2
$ json-to-dhall <<< -2.1
-2.1
$ json-to-dhall Natural <<< 2
2
$ json-to-dhall Integer <<< 2
+2
$ json-to-dhall Double <<< 2
2.0

JSON text corresponds to Dhall Text by default:

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

... but you can also decode text into a more structured enum, too, if you provide an explicit schema:

$ json-to-dhall '< A | B >' <<< '"A"'
< A | B >.A

Lists and records

Dhall Lists correspond to JSON lists:

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

You can even decode an empty JSON list to Dhall:

$ json-to-dhall <<< '[]'
[] : List <>

... which will infer the empty <> type if there are no other constraints on the type. If you provide an explicit type annotation then the conversion will use that instead:

$ json-to-dhall 'List Natural' <<< '[]'
[] : List Natural

Dhall records correspond to JSON records:

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

If you specify a schema with additional Optional fields then they will be None if absent:

$ json-to-dhall '{ foo : List Natural, bar : Optional Bool }' <<< '{ "foo": [ 1, 2, 3 ] }'
{ bar = None Bool, foo = [ 1, 2, 3 ] }

... and Some if present:

$ json-to-dhall '{ foo : List Natural, bar : Optional Bool }' <<< '{ "foo": [ 1, 2, 3 ], "bar": true }'
{ bar = Some True, foo = [ 1, 2, 3 ] }

If you specify a schema with too few fields, then the behavior is configurable. By default, the conversion will reject extra fields:

$ json-to-dhall '{ foo : List Natural }' <<< '{ "foo": [ 1, 2, 3 ], "bar": true }'

Error: Key(s) bar present in the JSON object but not in the expected Dhall record type. This is not allowed unless you enable the --records-loose flag:

Expected Dhall type:
{ foo : List Natural }

JSON:
{
    "foo": [
        1,
        2,
        3
    ],
    "bar": true
}

... as the error message suggests, extra fields are ignored if you enable the --records-loose flag.

$ json-to-dhall --records-loose '{ foo : List Natural }' <<< '{ "foo": [ 1, 2, 3 ], "bar": true }'
{ foo = [ 1, 2, 3 ] }

You can convert JSON key-value arrays to Dhall records, but only if you supply an explicit Dhall type:

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

You can also disable this behavior using the --no-keyval-arrays:

$ json-to-dhall --no-keyval-arrays '{ a : Natural, 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:

You can also convert JSON records to Dhall Maps, but only if you supply an explicit schema:

$ json-to-dhall 'List { mapKey : Text, mapValue : Text }' <<< '{ "foo": "bar" }'
toMap { foo = "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 } ]

You can similarly disable this feature using --no-keyval-maps:

$ 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

If your schema is a record with a List field and omit that field in the JSON, you'll get an error:

$ json-to-dhall  '{ a : List Natural }' <<< '{}'


Error: Key a, expected by Dhall type:
List Natural
is not present in JSON object:
{}

You can use the --omissible-lists option to default to an empty list in this case

$ json-to-dhall --omissible-lists  '{ a : List Natural }' <<< '{}'
{ a = [] : List Natural }

Optional values and unions

JSON null values correspond to Optional Dhall values:

$ json-to-dhall <<< 'null'
None <>

... and the schema inference logic will automatically wrap other values in Optional to ensure that the types line up:

$ json-to-dhall <<< '[ 1, null ]'
[ Some 1, None Natural ]

A field that might be absent also corresponds to an Optional type:

$ json-to-dhall <<< '[ { "x": 1 }, { "x": 2, "y": true } ]'
[ { x = 1, y = None Bool }, { x = 2, y = Some True } ]

For Dhall union types the correct value will be based on matching the type of JSON expression if you give an explicit type:

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

Also, the schema inference logic will still infer a union anyway in order to reconcile simple types:

$ json-to-dhall <<< '[ 1, true ]'
[ < Bool : Bool | Natural : Natural >.Natural 1
, < Bool : Bool | Natural : Natural >.Bool True
]

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:
< Left : Text | Middle : Text | Right : Integer >.Left "bar"
--------
< Left : 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
    ( toMap
        { bar = array [ number 1.0, bool True ]
        , foo = null
        }
    )
  ]

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

The schema inference algorithm will also infer this schema of last resort when unifying a simple type with a record or a list:

$ json-to-dhall <<< '[ 1, [] ]'
[ λ(JSON : Type) →
  λ ( json
    : { array : List JSON → JSON
      , bool : Bool → JSON
      , double : Double → JSON
      , integer : Integer → JSON
      , null : JSON
      , object : List { mapKey : Text, mapValue : JSON } → JSON
      , string : Text → JSON
      }
    ) →
    json.integer +1
, λ(JSON : Type) →
  λ ( json
    : { array : List JSON → JSON
      , bool : Bool → JSON
      , double : Double → JSON
      , integer : Integer → JSON
      , null : JSON
      , object : List { mapKey : Text, mapValue : JSON } → JSON
      , string : Text → JSON
      }
    ) →
    json.array ([] : List JSON)
]

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 and resolve imports

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 successfully 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 Aeson
>>> import qualified Data.HashMap.Strict as HM

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

Schema inference

data Schema

A Schema is a subset of the Expr type representing all possible Dhall types that inferSchema could potentially return

Constructors

Bool

Natural

Integer

Double

Text

List Schema

Optional Schema

Record RecordSchema

Union UnionSchema

ArbitraryJSON

Instances

Semigroup Schema

(<>) unifies two schemas

Defined in Dhall.JSONToDhall

Methods

(<>) :: Schema -> Schema -> Schema

sconcat :: NonEmpty Schema -> Schema

stimes :: Integral b => b -> Schema -> Schema

Monoid Schema

Defined in Dhall.JSONToDhall

Methods

mempty :: Schema

mappend :: Schema -> Schema -> Schema

mconcat :: [Schema] -> Schema

newtype RecordSchema

Aeson record type that inferSchema can infer

Constructors

RecordSchema

Fields

• getRecordSchema :: Map Text Schema

Instances

Semigroup RecordSchema

Defined in Dhall.JSONToDhall

Methods

(<>) :: RecordSchema -> RecordSchema -> RecordSchema

sconcat :: NonEmpty RecordSchema -> RecordSchema

stimes :: Integral b => b -> RecordSchema -> RecordSchema

data UnionSchema

A union type that inferSchema can infer

This type will have at most three alternatives:

• A Bool alternative
• Either a Natural, Integer, or Double alternative
• A Text alternative

These alternatives will always use the same names and types when we convert back to a Dhall type, so we only need to keep track of whether or not each alternative is present.

We only store simple types inside of a union since we treat any attempt to unify a simple type with a complex type as a strong indication that the user intended for the schema to be ArbitraryJSON.

Constructors

UnionSchema

Fields

• bool :: Any

  True if the union has a Bool alternative

• number :: UnionNumber

  Up to one numeric alternative

• text :: Any

  True if the union has a Text alternative

Instances

Eq UnionSchema

Defined in Dhall.JSONToDhall

Methods

(==) :: UnionSchema -> UnionSchema -> Bool

(/=) :: UnionSchema -> UnionSchema -> Bool

Semigroup UnionSchema

Unify two union types by combining their alternatives

Defined in Dhall.JSONToDhall

Methods

(<>) :: UnionSchema -> UnionSchema -> UnionSchema

sconcat :: NonEmpty UnionSchema -> UnionSchema

stimes :: Integral b => b -> UnionSchema -> UnionSchema

Monoid UnionSchema

Defined in Dhall.JSONToDhall

Methods

mempty :: UnionSchema

mappend :: UnionSchema -> UnionSchema -> UnionSchema

mconcat :: [UnionSchema] -> UnionSchema

inferSchema :: Value -> Schema

Given a JSON Value, make a best-effort guess of what the matching Dhall type should be

This is used by {json,yaml}-to-dhall if the user does not supply a schema on the command line

schemaToDhallType :: Schema -> Expr s a

Convert a Schema to the corresponding Dhall type

Exceptions

data CompileError

Constructors

TypeError (TypeError Src Void)

BadDhallType ExprX ExprX

Mismatch ExprX Value JSONPath

MissingKey Text ExprX Value JSONPath

UnhandledKeys [Text] ExprX Value JSONPath

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