Miscellaneous JSON🔗

Contributors: Anirudh Gupta

Miscellaneous JSON Operations🔗

While deriving instances is convenient, real-world JSON often requires manual control over serialization, default values, and transformations.

1. Field Renaming (Manual Instances)🔗

If your JSON uses snake_case but your Lean code uses camelCase, you can manually implement ToJson and FromJson instances.

The instance keyword in Lean is used to provide an implementation for a type class. In this case, ToJson and FromJson are type classes that define how a type should be converted to and from Json. By defining these instances manually, you gain full control over the mapping process, allowing you to bridge the gap between different naming conventions or data structures.

structure Person where
  firstName : String
  lastName  : String
deriving Repr

instance : ToJson Person where
  toJson p := json% {
    "first_name": $(p.firstName),
    "last_name": $(p.lastName)
  }

instance : FromJson Person where
  fromJson? j := do
    let first ← j.getObjValAs? String "first_name"
    let last  ← j.getObjValAs? String "last_name"
    return { firstName := first, lastName := last }

{"last_name": "Lovelace", "first_name": "Ada"}#eval toJson 
  ({ firstName := "Ada", lastName := "Lovelace" : Person })
Except.ok { firstName := "Ada", lastName := "Lovelace" }#eval (fromJson? (json% { "first_name": "Ada", 
    "last_name": "Lovelace" }) : Except String Person)

2. Handling Default Values🔗

You can use Json.getObjValAs? to provide a fallback value if a key is missing or not of the expected type.

def getPort (j : Json) (defaultPort : Nat := 8080) : Nat :=
  match j.getObjValAs? Nat "port" with
  | .ok n => n
  | .error _ => defaultPort

3000#eval getPort (json% { "host": "localhost", "port": 3000 })
8080#eval getPort (json% { "host": "localhost" })