Heterogeneous Lists

We define HList as a synonym for List (Σ α : Type u, α), namely a list of types together with a value.

We note some other implementations of HList:

• Soup
• Part of Certified Programming with Dependent Types (it's in Coq, but can be translated to Lean)

Our choice of definition is so that we can directly rely on the existing API for List.

@[reducible, inline]

abbrev HList : Type (u + 1)

Heterogeneous list

def HList.nil : HList

def HList.cons (x : (α : Type u) × α) (xs : HList) : HList

def HList.hlist : Lean.ParserDescr

def HList.«term_::ₕ_» : Lean.TrailingParserDescr

@[simp]

theorem HList.cons_eq_List.cons {x : (α : Type u) × α} {xs : HList} : x ::ₕ xs = x :: xs

@[simp]

theorem HList.length_nil : List.length nil = 0

@[simp]

theorem HList.length_cons (x : (α : Type u) × α) (xs : HList) : List.length (x ::ₕ xs) = List.length xs + 1

def HList.getTypes : HList → List (Type u)

Returns the types of the elements in the HList

@[simp]

theorem HList.getTypes_nil : getTypes [] = []

@[simp]

theorem HList.getTypes_cons (x : (α : Type u) × α) (xs : HList) : getTypes (x :: xs) = x.fst :: xs.getTypes

@[simp]

theorem HList.getTypes_hcons (x : (α : Type u) × α) (xs : HList) : (x ::ₕ xs).getTypes = x.fst :: xs.getTypes

@[simp]

theorem HList.length_getTypes (l : HList) : l.getTypes.length = List.length l

@[simp]

theorem HList.getTypes_eq_get_fst (l : HList) (i : Fin (List.length l)) : l.getTypes[i] = l[i].fst

def HList.getValue (l : HList) (i : Fin (List.length l)) : l[i].fst

Get the value of the element at index i, of type l[i].1

@[simp]

theorem List.get_nil {α : Type u} (i : Fin 0) (a : α) : [].get i = a

def DVec {m : Type v} (α : m → Type u) : Type (max u v)

Dependent vectors

def HList.toDVec (l : HList) : DVec fun (i : Fin (List.length l)) => l[i].fst

Convert a HList to a DVec

def HList.ofDVec {n : ℕ} {α : Fin n → Type u} (l : DVec α) : HList

Create an HList from a DVec

theorem HList.toDVec_eq_getValue (l : HList) (i : Fin (List.length l)) : l.toDVec i = l.getValue i

Equivalent between HList.getValue and HList.toDVec