Explain all the arguments to this rec eliminator

Question

I defined this inductive type for representing JSON elements

inductive JSON where
  | null
  | bool (value : Bool)
  | string (value : String)
  | number (value : Float)
  | object (data : AssocList String JSON)
  | array (elements : List JSON)

Which results in the following definition of JSON.rec:

recursor JSON.rec.{u} :
  {motive_1 : JSON → Sort u} →
  {motive_2 : AssocList String JSON → Sort u} →
  {motive_3 : List JSON → Sort u} →
  motive_1 JSON.null →
  ((value : Bool) → motive_1 (JSON.bool value)) →
  ((value : String) → motive_1 (JSON.string value)) →
  ((value : Float) → motive_1 (JSON.number value)) →
  ((data : AssocList String JSON) → motive_2 data → motive_1 (JSON.object data)) →
  ((elements : List JSON) → motive_3 elements → motive_1 (JSON.array elements)) →
  motive_2 AssocList.nil →
  ((key : String) → (value : JSON) → (tail : AssocList String JSON) →
        motive_1 value → motive_2 tail → motive_2 (AssocList.cons key value tail)) →
  motive_3 [] →
  ((head : JSON) → (tail : List JSON) → motive_1 head → motive_3 tail → motive_3 (head :: tail)) →
  (t : JSON) → motive_1 t

Can someone explain the various arguments that go into this? I can see that each constructor gets an argument, like church encoding of the data type, but why are there arguments for nil and cons for AssocList and List? Why 3 motives instead of 1?

Answer 1

I found hints of the answer here

The original definition of JSON "falls outside the strict specification of an inductive type" because List JSON and AssocList String JSON are not positive occurrences. As a workaround, Lean's frontend compiles JSON into 3 mutually recursive types:

mutual
  inductive JSON where
    | object (data : Data)
    | array (elements : Elements)
    | -- other constructors unchanged

  inductive Data where
    | nil : Data
    | cons (key : String) (value : JSON) (tail : Data) : Data

  inductive Elements where
    | nil : Elements
    | cons (head : JSON) (tail : Elements) : Elements
end

Lean automatically defines isomorphisms between Data and AssocList String JSON and between Elements and List JSON. Lean then uses these isomorphisms to keep Data and Elements hidden, but they're there under the hood.

The abstraction works for constructors and pattern-matching, but it leaks into the rec definition, which is essentially three simultaneous eliminations in one. Morally in JSON.rec we are defining 3 mutually recursive functions:

• f1 : (j : JSON) -> motive_1 j
• f2 : (d : Data) -> motive_2 d
• f3 : (e : Elements) -> motive_3 e

The overall return type will come from f1

recursor JSON.rec.{u} :
  -- Return types for each of the three sub-functions
  {motive_1 : JSON → Sort u} →
  {motive_2 : AssocList String JSON → Sort u} →
  {motive_3 : List JSON → Sort u} →

  -- One argument per JSON constructor to handle each case in f1
  motive_1 JSON.null →
  ((value : Bool) → motive_1 (JSON.bool value)) →
  ((value : String) → motive_1 (JSON.string value)) →
  ((value : Float) → motive_1 (JSON.number value)) →
  ((data : AssocList String JSON) → motive_2 data → motive_1 (JSON.object data)) →
  ((elements : List JSON) → motive_3 elements → motive_1 (JSON.array elements)) →

  -- One argument per Data constructor to handle each case in f2
  motive_2 AssocList.nil →
  ((key : String) → (value : JSON) → (tail : AssocList String JSON) →
        motive_1 value → motive_2 tail → motive_2 (AssocList.cons key value tail)) →

  -- One argument per Elements constructor to handle each case in f3
  motive_3 [] →
  ((head : JSON) → (tail : List JSON) → motive_1 head → motive_3 tail → motive_3 (head :: tail)) →

  -- The value to fold over and the overall return value
  (t : JSON) → motive_1 t
```