How to convert structure to json in dhall?

Question

How do I convert arbitrary structure into json?

let Prelude = ./include/Prelude.dhall
let JSON = Prelude.JSON
let Foo = { a: Natural, t: Text }
let foo = { a = 10, b = "foo" }
in (DO_MAGIC foo) : JSON.Type

I know there is toMap builtin function, but it expects a homogeneous record.

What I actually trying to do is to write OpenAPI specification in dhall. Most parts of it are simple and nice, but json schema that describe incoming data shape is recursive, which is hard in Dhall. What I want would be expressed in Haskell like following

data Schema
  = SInteger { minimum :: Maybe Int, example :: Maybe Int } 
  | SString { format :: Maybe String, length :: Maybe Int }
  | Object [(String, Schema, Bool)] -- (name, schema, required)
  deriving (ToJSON)

Since it looked hard in Dhall, I decided that I would go this way:

data SInteger = SInteger { minimum :: Maybe Int, example :: Maybe Int }
data SString = SString { format :: Maybe String, length :: Maybe Int }
data Object = Object [(String, Schema, Bool)] -- (name, schema, required)

integer :: SInteger -> Schema
string :: SString -> Schema
object :: Object -> Schema

type Schema = JSON

but on this road I am stuck too. I am willing to sacrifice some of type rigidity for not patching dhall-json.

Answer 1

The basic idea is outlined in this guide:

• How to translate recursive code to Dhall

… and here is how that looks in the context of your example:

let List/map = https://prelude.dhall-lang.org/v17.1.0/List/map.dhall

let JSON = https://prelude.dhall-lang.org/v17.1.0/JSON/Type

let JSON/render = https://prelude.dhall-lang.org/v17.1.0/JSON/render

let SInteger = { minimum : Optional Integer, example : Optional Integer }

let SString = { format : Optional Text, length : Optional Natural }

let SObject =
      λ(Schema : Type) → List { name : Text, schema : Schema, required : Bool }

let Constructors =
      λ(Schema : Type) →
        { Integer : SInteger → Schema
        , String : SString → Schema
        , Object : SObject Schema → Schema
        }

let Schema
    : Type
    = ∀(Schema : Type) → ∀(schema : Constructors Schema) → Schema

let integer
    : SInteger → Schema
    = λ(x : SInteger) →
      λ(Schema : Type) →
      λ(schema : Constructors Schema) →
        schema.Integer x

let string
    : SString → Schema
    = λ(x : SString) →
      λ(Schema : Type) →
      λ(schema : Constructors Schema) →
        schema.String x

let object
    : List { name : Text, schema : Schema, required : Bool } → Schema
    = λ(x : SObject Schema) →
      λ(Schema : Type) →
      λ(schema : Constructors Schema) →
        let Input = { name : Text, schema : Schema@1, required : Bool }

        let Output = { name : Text, schema : Schema, required : Bool }

        let adapt =
              λ(y : Input) →
                { schema = y.schema Schema schema } ∧ y.{ name, required }

        in  schema.Object (List/map Input Output adapt x)

let toJSON
    : Schema → JSON
    = λ(schema : Schema) →
      λ(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
          }
        ) →
        schema
          JSON
          { Integer =
              λ(x : SInteger) →
                json.object
                  ( toMap
                      { minimum =
                          merge
                            { None = json.null, Some = json.integer }
                            x.minimum
                      , example =
                          merge
                            { None = json.null, Some = json.integer }
                            x.example
                      }
                  )
          , String =
              λ(x : SString) →
                json.object
                  ( toMap
                      { format =
                          merge
                            { None = json.null, Some = json.string }
                            x.format
                      , length =
                          merge
                            { None = json.null
                            , Some =
                                λ(n : Natural) →
                                  json.integer (Natural/toInteger n)
                            }
                            x.length
                      }
                  )
          , Object =
              λ(x : SObject JSON) →
                let Input = { name : Text, schema : JSON, required : Bool }

                let Output = { mapKey : Text, mapValue : JSON }

                let adapt =
                      λ(y : Input) →
                        { mapKey = y.name
                        , mapValue =
                            json.object
                              ( toMap
                                  { schema = y.schema
                                  , required = json.bool y.required
                                  }
                              )
                        }

                in  json.object (List/map Input Output adapt x)
          }

let example =
      let input =
            object
              [ { name = "foo"
                , required = True
                , schema = string { format = None Text, length = Some 10 }
                }
              , { name = "bar"
                , required = False
                , schema = integer { minimum = Some +0, example = Some +10 }
                }
              ]

      let output =
            ''
            {
              "foo": {
                "required": true,
                "schema": {
                  "format": null,
                  "length": 10
                }
              },
              "bar": {
                "required": false,
                "schema": {
                  "example": 10,
                  "minimum": 0
                }
              }
            }
            ''

      in  assert : JSON/render (toJSON input) ≡ output

in  { Schema, integer, string, object, toJSON }