26.1. JSON🔗

The Json datatype represents JSON values. To use the type and related functionality, import Lean.Data.Json.

inductive type

Lean.Json : Type
Lean.Json : Type

A JSON value.

Constructors

Lean.Json.null : Json

Lean.Json.bool (b : Bool) : Json

Lean.Json.num (n : JsonNumber) : Json

Lean.Json.str (s : String) : Json

Lean.Json.arr (elems : Array Json) : Json

Lean.Json.obj
  (kvPairs : Std.TreeMap.Raw String Json compare) : Json

JSON can express arbitrary precision rational numbers. We store these as JsonNumbers: a mantissa and a negative exponent. Beware that if decoded in JavaScript, these numbers may lose precision.

structure

Lean.JsonNumber : Type
Lean.JsonNumber : Type

A decimal number represented as mantissa * 10^-exponent.

Constructor

Lean.JsonNumber.mk

Fields

mantissa : Int

exponent : Nat

To parse JSON text into a Json value, use Json.parse. Note that Json.parse is not necessarily robust against adversarial inputs. For example, objects with duplicate keys ({ "a": 1, "a": 2 }) have unspecified decodings.

def

Lean.Json.parse (s : String) : Except String Json
Lean.Json.parse (s : String) :
  Except String Json

Parses a JSON value, surrounded by optional whitespace. Objects with duplicate keys are rejected.

In the other direction, there are two ways to render Json values as text. To optimize for compact representation, invoke Json.compress. Alternatively, to produce human-readable output, call Json.render or Json.pretty.

def

Lean.Json.compress (j : Json) : String
Lean.Json.compress (j : Json) : String

opaque

Lean.Json.render : Json → Format
Lean.Json.render : Json → Format

def

Lean.Json.pretty (j : Json) (lineWidth : Nat := 80) : String
Lean.Json.pretty (j : Json)
  (lineWidth : Nat := 80) : String

26.1.1. Literal Syntax🔗

In addition to using the Json constructors directly, JSON values can be written in standard notation following the json% keyword.

syntaxJSON Terms

term ::= ...
    | Allows to use Json syntax in a Lean file.json% json

One may optionally omit quotes on object keys in json% literals (similarly to JavaScript object literals). A $() delimiter can be used to interpolate any value with a FromJson instance (including Json values).

Using a JSON literal

variable (j : Json)

Json.mkObj [("a", Json.num 1), ("b", Json.arr #[Json.num 2, Json.num 3]), ("c", Json.null), ("d", toJson j)] : Json#check json% {
  "a": 1,
  "b": [2, 3],
  c: null,
  d: $(j)
}

Live ↪

The complete grammar of JSON literals is as follows.

syntaxJSON Literals

json ::=
      Json null value syntax.null
    | Json true value syntax.true
    | Json false value syntax.false
    | Json string syntax.str
    | Json number negation syntax for ordinary numbers.-? num
    | Json number negation syntax for scientific numbers.-? scientific
    | Json array syntax.[ json,* ]
    | Json object syntax.{ (Json key/value syntax.Json identifier syntax.jsonIdent : json),* }
    | $(term)

syntaxJSON Field Names

Json identifier syntax.jsonIdent ::=
      Json identifier syntax.ident
    | Json identifier syntax.str

26.1.2. Serialization🔗

Serialization of Lean values to JSON, and deserialization from JSON, is supported through the ToJson and FromJson type classes. Import Lean.Data.Json.FromToJson to use this functionality.

JSON representations of many Lean types can be derived automatically. The default encoding is documented on ToJson (below).

Serializing a structure to JSON

structure Foo where
  x : Bool := true
  y : String := "abc"
  z? : Option Nat := some 1
deriving ToJson, FromJson

{"z": 1, "y": "abc", "x": true}#eval toJson { : Foo }

{"z": 1, "y": "abc", "x": true}

Live ↪

type class

Lean.ToJson.{u} (α : Type u) : Type u
Lean.ToJson.{u} (α : Type u) : Type u

Types that can be encoded as JSON.

Use deriving ToJson to automatically generate an instance. The following encoding strategy is employed by auto-generated instances:

Basic types corresponding to JSON values are encoded as these values.
- Bool is encoded as true/false.
- Strings are encoded as JSON strings.
- Numeric types are encoded as JSON numbers, with the exception of:
  - UInt64 and USize which are encoded as JSON strings. This is because, although JSON numbers proper have unbounded range, in JavaScript they are parsed as Numbers and these can only represent integers up to $2^{53} - 1$ safely; so a roundtrip through JavaScript would result in truncation on these types. (We use these types in the JavaScript-based Lean infoview.)
  - Special Floats which are encoded as JSON strings: "NaN"/"Infinity"/"-Infinity".
Unit is encoded as {} (empty JSON object).
Arrays and Lists are encoded as JSON arrays.
Option.none is encoded as null, whereas some a has the same encoding as a. Note that this implies Option (Option α) does not roundtrip, since none and some none both become null.
General structures are encoded as JSON objects in the obvious way.
- Option fields whose names end with ? have special support: the question mark is omitted from the JSON field name, and such a field is omitted from the JSON object when its value is none (as opposed to being encoded as { "someField": null }).
General inductive types are encoded on a per-constructor basis.
- An argument-free constructor is encoded as its name (a JSON string).
- A constructor with named arguments only is encoded as the JSON object { "ctorName": { "arg1": argVal1, ..., "argN": argValN } }.
- A constructor with one unnamed argument is encoded as the JSON object { "ctorName": argVal }.
- A constructor with more than one unnamed argument is encoded as the JSON object { "ctorName": [argVal1, ..., argValN] }.
Certain other types have special handling: see the instances below.

Instance Constructor

Lean.ToJson.mk.{u}

Methods

toJson : α → Json

type class

Lean.FromJson.{u} (α : Type u) : Type u
Lean.FromJson.{u} (α : Type u) : Type u

Types that can be decoded from JSON.

Use deriving FromJson to automatically generate an instance. See ToJson for details of auto-generated instances.

Instance Constructor

Lean.FromJson.mk.{u}

Methods

fromJson? : Json → Except String α

Many helper functions are available for writing custom JSON encoders and decoders.

For creating JSON values, we have among others Json.mkObj, Json.setObjVal!, and Json.setObjValAs!.

For decoding JSON, the following can be useful: Json.isNull, Json.getStr?, Json.getNat?, Json.getInt?, Json.getBool?, Json.getArr?, Json.getArrVal?, Json.getObjVal?, Json.getObjValD, Json.getObjValAs?.

26.1.	JSON
26.2.	HTML