An indexed encoding for existentials

existentials.lean

inductive Tag : Type where
| Bool : Tag
| List : Tag -> Tag
| UserCtor : Tag -- struct UserCtor(t : TypeTag, m: TypeFor t -> String, TypeFor t)
| Pi : Tag -> Tag -> Tag
| Tag : Tag



def TypeFor (n : Nat) (tag : Tag) : Type :=
  match h : tag with
  | .Bool => Bool
  | .List t => List (TypeFor n t)
  | .UserCtor => 
    if n == 0 then
      Empty
    else
      (t : Tag) × 
        let R := TypeFor (n - 1) t
        (R -> String × R)
  | .Pi a b => (TypeFor n a) -> (TypeFor n b)
  | .Tag => Tag
termination_by (n, tag)
decreasing_by
  apply Prod.Lex.right
  simp
  apply Prod.Lex.left
  grind
  apply Prod.Lex.right
  grind
  apply Prod.Lex.right
  grind


structure MyThingy (n : Nat) where
  a : Tag
  b : List (TypeFor n a)

-- forall R. (forall x. P x -> R) -> R
-- forall x. P x
-- exists a. 

inductive Tag2 : (n : Nat) -> Type where
| Bool : Tag2 0
| Tag : (n : Nat) -> Tag2 (n + 1)
| List : Tag2 n -> Tag2 n
| UserCtor : Tag2 (n + 1) -- struct UserCtor(t : TypeTag, m: TypeFor t -> String, TypeFor t)
| Pi : Tag2 n -> Tag2 n -> Tag2 n


-- def TagUniv2.inhabitants (n : Nat) (tag : Tag2 n) : Nat :=
--   match tag with
--   | .Bool => 2
--   | .List t => (TagUniv2.inhabitants n t) sizeOf n t
--   | .UserCtor h1 => 
--     if n == 0 then
      
--     TagUniv.sizeOf

def Tag2N := (n : Nat) × Tag2 n

-- the tags that can plausibly be reached "under" an initial one
inductive SmallTag : Tag2N -> Tag2N -> Prop where
| List : SmallTag ⟨n, t⟩ ⟨n, (.List t)⟩
| PiArg : SmallTag ⟨n, a⟩ ⟨n, (.Pi a b)⟩
| PiRet : SmallTag ⟨n, b⟩ ⟨n, (.Pi a b)⟩
| UserCtor {t}  : SmallTag t ⟨t.fst + 1, .UserCtor⟩

    
theorem small_tag_wf : SmallTag smaller ⟨n, t⟩  -> Acc SmallTag smaller  := by 
  intro hSm
  cases t

  case Bool => cases hSm
  case Tag => cases hSm
  case List =>
    cases hSm

    apply Acc.intro
    intro y ev
    exact small_tag_wf ev
  case UserCtor =>
    cases hSm
    
    apply Acc.intro
    intro y ev
    exact small_tag_wf ev
  case Pi => 
    cases hSm <;> {
      apply Acc.intro
      intro y ev
      exact small_tag_wf ev
    }



instance : WellFoundedRelation ((n : Nat) × Tag2 n) := .mk SmallTag (by 
  apply WellFounded.intro
  intro a
  apply Acc.intro
  intro y h
  apply small_tag_wf h)

def TypeFor2 (t : (n : Nat) × Tag2 n) : Type :=
  match h3 : t with 
  | ⟨ n, tag ⟩ =>
    match tag with
    | .Bool => Bool
    | .List t => List (TypeFor2 ⟨ n, t⟩ )
    | .UserCtor => 
        (t : Tag2 (n - 1)) × 
          let R := TypeFor2 ⟨ (n - 1), t⟩ 
          (R -> String × R)
    | .Pi a b => (TypeFor2 ⟨ n, a⟩ ) -> (TypeFor2 ⟨ n,  b ⟩ )
    | .Tag n => Tag2 n
termination_by t
decreasing_by
  apply SmallTag.List
  · next tdef _ n' => 
    generalize h4 : (Sigma.mk (n' + 1) Tag2.UserCtor) = r
    generalize h5 : (Sigma.mk (n - 1) t) = r2
    suffices h6 : r = ⟨Sigma.fst r2 + 1, Tag2.UserCtor⟩ by
      rw [h6]
      apply SmallTag.UserCtor
    simp [← h4, ← h5]
    grind
  · apply SmallTag.PiArg
  · apply SmallTag.PiRet


structure MyThingy2 (n : Nat) where
  a : Tag2 n
  b : List (TypeFor2 ⟨ n, a⟩)


inductive Tag3 :  Type where
| Bool : Tag3
| Tag : Tag3
| List : Tag3 -> Tag3
| UserCtor : Tag3 -- struct UserCtor(t : TypeTag, m: TypeFor t -> String, TypeFor t)
| Pi : Tag3 -> Tag3 -> Tag3


-- def TagUniv2.inhabitants (n : Nat) (tag : Tag2 n) : Nat :=
--   match tag with
--   | .Bool => 2
--   | .List t => (TagUniv2.inhabitants n t) sizeOf n t
--   | .UserCtor h1 => 
--     if n == 0 then
      
--     TagUniv.sizeOf

def Tag3N := Nat × Tag3

-- the tags that can plausibly be reached "under" an initial one
inductive SmallTag3 : Tag3N -> Tag3N -> Prop where
| List : SmallTag3 ⟨n, t⟩ ⟨n, (.List t)⟩
| PiArg : SmallTag3 ⟨n, a⟩ ⟨n, (.Pi a b)⟩
| PiRet : SmallTag3 ⟨n, b⟩ ⟨n, (.Pi a b)⟩
| UserCtor {t}  : SmallTag3 t ⟨t.fst + 1, .UserCtor⟩

    
theorem small_tag3_wf : SmallTag3 smaller (n, t)  -> Acc SmallTag3 smaller  := by 
  intro hSm
  cases t

  case Bool => cases hSm
  case Tag => cases hSm
  case List =>
    cases hSm

    apply Acc.intro
    intro y ev
    exact small_tag3_wf ev
  case UserCtor =>
    cases hSm
    
    apply Acc.intro
    intro y ev
    exact small_tag3_wf ev
  case Pi => 
    cases hSm <;> {
      apply Acc.intro
      intro y ev
      exact small_tag3_wf ev
    }



instance : WellFoundedRelation Tag3N := .mk SmallTag3 (by 
  apply WellFounded.intro
  intro a
  apply Acc.intro
  intro y h
  apply small_tag3_wf h)

def TypeFor3 (t : Tag3N) : Type :=
  match h3 : t with 
  | ⟨ n, tag ⟩ =>
    match tag with
    | .Bool => Bool
    | .List t => List (TypeFor3 ⟨ n, t⟩ )
    | .UserCtor => 
      if n == 0 then Empty
      else
        (t : Tag3) × 
          let R := TypeFor3 ⟨ (n - 1), t⟩ 
          (R -> String × R)
    | .Pi a b => (TypeFor3 ⟨ n, a⟩ ) -> (TypeFor3 ⟨ n,  b ⟩ )
    | .Tag => Tag3
termination_by t
decreasing_by
  apply SmallTag3.List
  · generalize h1 : n - 1 = n' 
    have h2 := congrArg  (fun n => n + 1) h1
    rw [Nat.sub_add_cancel] at h2
    rw [h2]
    apply SmallTag3.UserCtor
    grind
  · apply SmallTag3.PiArg
  · apply SmallTag3.PiRet


structure MyThingy3 (n : Nat) where
  a : Tag3
  b : List (TypeFor3 ⟨ n, a⟩)

This is 3 variants on the same pattern: a Tag type describing types, and a TypeFor : Tag -> Type function that realizes them. For TypeFor to be well-formed over a set of types that can include existentials, we need to index the depth of the existentials for the proof that its definition is well formed.

This isn't exactly an issue for the purposes of a programming language: This creates a set of 'smaller' universes in a sense that can all live in Set, and if user types are parameterized over n we can provide a meaningful definition of many typical more "impredicative" style definitions by asserting that the lowering of the program is performed at "the lowest necessary n necessary for typing the program", translating to store the values efficiently.

This begs the question of whether we can formalize this pattern to take n "in the limit" and produce a typing rules that have a more native notion of existential types. The delicate interaction is localized to the fully general Pi type formers, where stratification is necessary when a Pi's return type captures the generalized variable of an "existentially bound" (that is, given by a Tag in a product type) type