Heterogenous vectors

Stream: new members

[Nicolas Rolland]

In haskell, or Idris, there are so called "heterogeneous vectors" where one statically tracks the size and the types of elements

I think there are no such data type in Lean (?)
Should I write it my self, which of the following two style is more idiomatic in Lean (or are they equally easy / painful) ?

import Mathlib.Data.Vector

-- Heterogeneous vector style 1
inductive HVect : (n : Nat) -> (Vector (Type v) n) -> Type (v+1)  where
   | Nil  : HVect 0 ⟨ [], simp ⟩
   | Cons : (t : Type v) -> (x : t) -> HVect n ⟨ts, p⟩ -> HVect (n+1) ⟨t::ts, by simp [p]⟩

-- Heterogeneous vector style 2
def HVector (n : ℕ) (ts : Vector Type n)  := (i:Fin (n)) -> ts[i]

def Nil : HVector 0 ⟨[], p ⟩ := fun (⟨n, (p : n < 0)⟩) ↦ by
    exfalso
    have := Nat.le_lt_antisymm (Nat.zero_le n)
    exact this p

def Cons : α → HVector n ⟨ts, tsp⟩ → HVector (Nat.succ n) (⟨α :: ts, by simp; exact tsp⟩ )
  | a, f => fun (⟨i, (ip : i < Nat.succ n)⟩) ↦ by
      rcases i  with (i|i)
      . exact a
      . have : i < n := Nat.succ_lt_succ_iff.mp  ip
        exact f ⟨i, this⟩

[Eric Wieser]

Typically mathlib uses:

-- Heterogeneous vector style 2.5
abbrev HVector (n : ℕ) (ts : Fin n -> Type)  := (i : Fin n) -> ts i

[Kyle Miller]

(Note that this HVector type has different runtime characteristics from HVect, if you care about using these in programs. HVector is a closure and if you're not careful you can have long chains of unforced computations. HVect is eager. On the other hand, HVector is probably more pleasant to prove things about -- HVector is sort of the abstract interface for a heterogenous vector -- and you can generalize Fin n to an arbitrary indexing type.)