Inductive, low universe, TypeVec.Arrow

Stream: general

[William Sørensen]

I have these 3 definitions for TypeVec.Arrow:

def Arrow₁ (α : TypeVec.{u} n) (β : TypeVec.{v} n) : Type max u v :=
  ∀ i : Fin n, α.get i → β.get i

def Arrow₂ : {n : Nat} → TypeVec.{u} n → TypeVec.{v} n → Type max u v
  | 0, .nil, .nil => PUnit
  | _+1, .cons ht₁ tt₁, .cons ht₂ tt₂ => (ht₁ → ht₂) × (Arrow₂ tt₁ tt₂)

inductive Arrow : {n : _} → (α : TypeVec.{u} n) → (β : TypeVec.{v} n) → Type (max u v +1)
  | nil : Arrow .nil .nil
  | cons
      {ht₁ : Type u} {ht₂ : Type v}
      {tt₁ : TypeVec.{u} _} {tt₂ : TypeVec.{v} _}
      (hd : ht₁ → ht₂)
      (tl : Arrow tt₁ tt₂)
      : Arrow (.cons ht₁ tt₁) (.cons ht₂ tt₂)

But for some reason the intuitive definition has a universe bump i cant seem to avoid. Is there:

• A way around this,
• or alternatively a way to define a custom cases definition to be used in a match elimination

[Aaron Liu]

can you provide a #mwe

[William Sørensen]

mwe of general problem:

inductive Holder
  | empty
  | t (x : Type u)

inductive HolderArr : Holder → Type (u+1)
  | empty : HolderArr .empty
  | t {x : Type u} : (x → Bool) → HolderArr (.t x)

Full example here:

inductive Vec (α : Type u) : Nat → Type u
  | nil : Vec α 0
  | cons {n : Nat} (head : α) (tail : Vec α n) : Vec α (n + 1)

abbrev TypeVec (n : Nat) : Type (u+1) := Vec (Type u) n

def Arrow₁ (α : TypeVec.{u} n) (β : TypeVec.{v} n) : Type max u v :=
  ∀ i : Fin n, α.get i → β.get i

def Arrow₂ : {n : Nat} → TypeVec.{u} n → TypeVec.{v} n → Type max u v
  | 0, .nil, .nil => PUnit
  | _+1, .cons ht₁ tt₁, .cons ht₂ tt₂ => (ht₁ → ht₂) × (Arrow₂ tt₁ tt₂)

inductive Arrow : {n : _} → (α : TypeVec.{u} n) → (β : TypeVec.{v} n) → Type (max u v +1)
  | nil : Arrow .nil .nil
  | cons
      {ht₁ : Type u} {ht₂ : Type v}
      {tt₁ : TypeVec.{u} _} {tt₂ : TypeVec.{v} _}
      (hd : ht₁ → ht₂)
      (tl : Arrow tt₁ tt₂)
      : Arrow (.cons ht₁ tt₁) (.cons ht₂ tt₂)

[William Sørensen]

to elaborate on what i mean with the second alternative:
In writing functions like this:

/-- arrow composition in the category of `TypeVec` -/
def comp : {n : Nat} → {α β γ : TypeVec n} → β ⟹ γ → α ⟹ β → α ⟹ γ
  | 0, .nil, .nil, .nil, .nil, .nil => .nil
  | _+1, .cons _ _, .cons _ _, .cons _ _, .cons f t₁, .cons g t₂ =>
    .cons (f ∘ g) (comp t₁ t₂)

I have to be explicit with the constructors of the TypeVec when using the non-inductive defn of Arrows, while using the inductive one it becomes

def comp : {n : Nat} → {α β γ : TypeVec n} → β ⟹ γ → α ⟹ β → α ⟹ γ
  | 0, _, _,_, .nil, .nil => .nil
  | _, _,  _, _, .cons f t₁, .cons g t₂ =>
    .cons (f ∘ g) (comp t₁ t₂)

Is there a way to avoid this?

[Robin Arnez]

Are you working independent of mathlib?
Mathlib defines

/-- n-tuples of types, as a category -/
@[pp_with_univ]
def TypeVec (n : ℕ) :=
  Fin2 n → Type*

/-- arrow in the category of `TypeVec` -/
def Arrow (α β : TypeVec n) :=
  ∀ i : Fin2 n, α i → β i

@[inherit_doc] scoped[MvFunctor] infixl:40 " ⟹ " => TypeVec.Arrow

/-- identity of arrow composition -/
def id {α : TypeVec n} : α ⟹ α := fun _ x => x

/-- arrow composition in the category of `TypeVec` -/
def comp {α β γ : TypeVec n} (g : β ⟹ γ) (f : α ⟹ β) : α ⟹ γ := fun i x => g i (f i x)

[William Sørensen]

I am aware. I am just interested to see if with a different definition some of the strangenesses can be avoided like splitFun v appendFun

[William Sørensen]

cuz i have a bunch of code that works with the current definition and its just so painful

[Robin Arnez]

Well for one, the current definition has practical reasons; TypeVec as a function to Type* will be erased at runtime and a Vector of Type* won't.

[Robin Arnez]

Otherwise, what kind of TypeVec are you working with? Couldn't that somehow be fixed using more API on TypeVec?

[William Sørensen]

No i doubt it. I have a few PRs up for making Ws and Ms universe generic but heqs kindof just pop up all the time and i dont feel can be avoided. I am just wondering if having a nice way to patternmatch over then would

[William Sørensen]

And why wouldnt the inductive definitions also be stripped at runtime? Are functions just treated differently at compilation when on a type level?

[Robin Arnez]

A Vector is an Array and an array needs to (at least) store the length

[Robin Arnez]

Well I guess yours isn't an array but you still have to store the structure

[Robin Arnez]

Take this example:

inductive Vec (α : Type u) : Nat → Type u
  | nil : Vec α 0
  | cons {n : Nat} (head : α) (tail : Vec α n) : Vec α (n + 1)

def Vec.size (v : Vec α n) : Nat :=
  match v with
  | .nil => 0
  | .cons _ t => t.size + 1

def test : Vec Prop (Exists.choose (⟨2, rfl⟩ : ∃ a, a = 2)) := by
  have := Exists.choose_spec (⟨2, rfl⟩ : ∃ a, a = 2)
  rw [this]
  exact .cons True (.cons False .nil)

#eval test.size -- 2

(note that this only works on latest nightly though)

[William Sørensen]

Is this to make the vector be erased?

[William Sørensen]

so to erase it i just need a noncomputable value somewhere in the defn?

[William Sørensen]

i still dont understand, doesnt the function still have to be stored in the same way the vec has to be stored?

[Robin Arnez]

In this example you can see that you can't just evaluate the length directly from the type (because of Exists.choose). But you can still compute the length as long as the original expression was computable. Thus the compiler can't erase things of type Vec

[William Sørensen]

But you can do this exact same thing with the mathlib defn of Vec? Is there something I’m missing here?

[Robin Arnez]

Well if you use Fin n -> ... then you don't have the size information anywhere but in the type:

def Vec (α : Type u) : Nat → Type u :=
  fun n => Fin n → α

def Vec.size (_v : Vec α n) : Nat :=
  -- can only use `n`
  n

def test : Vec Prop (Exists.choose (⟨2, rfl⟩ : ∃ a, a = 2)) := by
  have := Exists.choose_spec (⟨2, rfl⟩ : ∃ a, a = 2)
  rw [this]
  exact fun | 0 => True | 1 => False

#eval test.size -- error

whereas the inductive Vec also encodes it in its structure

[William Sørensen]

How does this interact with the second impl Arrow₂

[Robin Arnez]

Well Arrow₂ would still be erased because it is a type; but appending TypeVecs etc. might happen at runtime as well

[William Sørensen]

Ok then I’ll try using those as it solves the main issue which is appendFun and splitFun are then no longer needed. Great. Yeah this api is just a bit painful to work with sometimes

[Robin Arnez]

Is this also acceptable (for matching on TypeVec):

import Mathlib

inductive TypeVecDesc.{u} : ℕ → TypeVec.{u} n → Type (u + 1) where
  | nil : TypeVecDesc 0 v
  | append1 (v : TypeVec.{u} n) (α : Type u) (h : v' = v.append1 α) : TypeVecDesc (n + 1) v'

abbrev TypeVec.dest (vec : TypeVec.{u} n) : TypeVecDesc.{u} n vec :=
  match n with
  | 0 => .nil
  | _ + 1 => .append1 vec.drop vec.last (TypeVec.append1_drop_last _).symm

@[simp] theorem TypeVec.dest_nil (vec : TypeVec.{u} 0) : vec.dest = .nil := rfl
@[simp] theorem TypeVec.dest_append1 (v : TypeVec.{u} n) (α : Type u) : (v.append1 α).dest = .append1 v α rfl := rfl

def Arrow₂ {n : Nat} (v₁ : TypeVec.{u} n) (v₂ : TypeVec.{v} n) : Type max u v :=
  match v₁.dest, v₂.dest with
  | .nil, .nil => PUnit
  | .append1 tt₁ ht₁ rfl, .append1 tt₂ ht₂ rfl => (ht₁ → ht₂) × (Arrow₂ tt₁ tt₂)